[Agda] Agda with excluded middle is inconsistent

[Thorsten Altenkirch]

Dear Chung,

congratulations! I didn't know about this problem and I think it is a serious issue indeed. Maybe it is a known issue? Nisse? Ulf?

Surely, type constructors should not be injective in general. A definition of the form

	data I : (Set -> Set) -> Set where 

should be expandable by an annonymous declaration 

	I : (Set -> Set) -> Set
	I F = data {}

in an analogous way a named function definition can be expanded by definition and a lambda abstraction (e.g. this is the approach in PiSigma a proposed core language for dependently typed programming).

Clearly I is just a constant function and hence not injective. 

I suspect that the idea that type constructors should be injective arises from the goal to imitate polymorphic programming ala Haskell where the type checker exploits the "fact" that all type formers are injective. This is reflected in a rule in Haskell's core language Fc which I find semantically unacceptable but which seems to be pragmatically necessary.

How can we fix this? I suspect that it would be pragmatically unacceptable to give up in general that type constructors are injective because this would make type inference much less powerful. 

First of all, clearly it is not essential that I is empty, your proof goes through with

	data I : (Set -> Set) -> Set where 
	   inI : I (λ x → x)

 without any problems. Interestingly, the proof still goes through if we turn the first argument into a parameter

	 data I (F : Set -> Set) : Set where 
	   inI : I F

I find this interesting because now I seems to be injective because F is now an implicit parameter of inI.  However, if we try to translate this into an anonymous definition we end up destroying injectivity. Hence the mistaken assumption that all type constructors are injective seems to be the root of the problem.

The only fix I can see is that Agda should check wether a type constructor is actually injective and only then use this fact during unification. We may want to go further and allow the user to prove that a function is injective (I suggested this before) which would enable us to make type inference stronger in many situations. For most type constructors Agda could infer this automatically but certainly not for I and its variants.

Btw, I think it is correct that your proof needs EM even though I can't think of a simple argument just now. This is related to what Dan has been saying: I conjectured if we assume some sort of continuity we can actually construct a non-trivial solution of a D = D -> D in Type Theory. But since continuity is consistent with core Type Theory we should not be able to refute this. 

Continuity is also inconsistent with EM but it seems a reasonable assumption, while I cannot see any reason to believe that all type constructors should be injective. Also while we may accept that extensions of Type Theory may be anticlassical, we should expect that core Type Theory is consistent with EM. Hence, this is a real issue and it should be fixed.

Cheers,
Thorsten

	



On 6 Jan 2010, at 23:44, Chung Kil Hur wrote:

> Hi everyone,
>  
> I proved the absurdity in Agda assuming the excluded middle.
> Is it a well-known fact ?
> It seems that Agda's set theory is weird.
>  
> This comes from the injectivity of inductive type constructors.
>  
> The proof sketch is as follows.
>  
> Define a family of inductive type
>  
> data I : (Set -> Set) -> Set where
>  
> with no constructors.
>  
> By injectivity of type constructors, I can show that I : (Set -> Set) -> Set is injective.
>  
> As you may see, there is a size problem with this injectivity.
>  
> So, I just used the cantor's diagonalization to derive absurdity in a classical way.
>  
> Does anyone know whether cantor's diagonalization essentially needs the classical axiom, or can be done intuitionistically ?
> If the latter is true, then Agda system is inconsistent.
>  
> Please have a look at the Agda code below.
>  
> Any comments are wellcome.
>  
> Best regards,
> Chung-Kil Hur
>  
>  
> ============== Agda code ===============
>  
> module cantor where
>  
>   data Empty : Set where
>  
>   data One : Set where
>     one : One
>  
>   data coprod (A : Set1) (B : Set1) : Set1 where
>     inl : ∀ (a : A) -> coprod A B
>     inr : ∀ (b : B) -> coprod A B
>  
>   postulate exmid : ∀ (A : Set1) -> coprod A (A -> Empty)
>  
>   data Eq1 {A : Set1} (x : A) : A -> Set1 where
>     refleq1 : Eq1 x x
>  
>   cast : ∀ { A B } -> Eq1 A B -> A -> B
>   cast refleq1 a = a
>  
>   Eq1cong : ∀ {f g : Set -> Set} a -> Eq1 f g -> Eq1 (f a) (g a)
>   Eq1cong a refleq1 = refleq1
>  
>   Eq1sym : ∀ {A : Set1} { x y : A } -> Eq1 x y -> Eq1 y x
>   Eq1sym refleq1 = refleq1
>  
>   Eq1trans : ∀ {A : Set1} { x y z : A } -> Eq1 x y -> Eq1 y z -> Eq1 x z
>   Eq1trans refleq1 refleq1 = refleq1
>  
>   data I : (Set -> Set) -> Set where
>  
>   Iinj : ∀ { x y : Set -> Set } -> Eq1 (I x) (I y) -> Eq1 x y 
>   Iinj refleq1 = refleq1
>  
>   data invimageI (a : Set) : Set1 where
>     invelmtI : forall x -> (Eq1 (I x) a) -> invimageI a
>  
>   J : Set -> (Set -> Set)
>   J a with exmid (invimageI a)
>   J a | inl (invelmtI x y) = x
>   J a | inr b = λ x → Empty
>  
>   data invimageJ (x : Set -> Set) : Set1 where
>     invelmtJ : forall a -> (Eq1 (J a) x) -> invimageJ x
>  
>   IJIeqI : ∀ x -> Eq1 (I (J (I x))) (I x)
>   IJIeqI x with exmid (invimageI (I x))
>   IJIeqI x | inl (invelmtI x' y) = y
>   IJIeqI x | inr b with b (invelmtI x refleq1)
>   IJIeqI x | inr b | ()
>  
>   J_srj : ∀ (x : Set -> Set) -> invimageJ x
>   J_srj x = invelmtJ (I x) (Iinj (IJIeqI x))
>  
>   cantor : Set -> Set
>   cantor a with exmid (Eq1 (J a a) Empty)
>   cantor a | inl a' = One
>   cantor a | inr b = Empty
>  
>   OneNeqEmpty : Eq1 One Empty -> Empty
>   OneNeqEmpty p = cast p one
>  
>   cantorone : ∀ a -> Eq1 (J a a) Empty -> Eq1 (cantor a) One 
>   cantorone a p with exmid (Eq1 (J a a) Empty)
>   cantorone a p | inl a' = refleq1
>   cantorone a p | inr b with b p
>   cantorone a p | inr b | ()
>  
>   cantorempty : ∀ a -> (Eq1 (J a a) Empty -> Empty) -> Eq1 (cantor a) Empty
>   cantorempty a p with exmid (Eq1 (J a a) Empty)
>   cantorempty a p | inl a' with p a'
>   cantorempty a p | inl a' | ()
>   cantorempty a p | inr b = refleq1
>  
>   cantorcase : ∀ a -> Eq1 cantor (J a) -> Empty
>   cantorcase a pf with exmid (Eq1 (J a a) Empty)
>   cantorcase a pf | inl a' = OneNeqEmpty (Eq1trans (Eq1trans (Eq1sym (cantorone a a')) (Eq1cong a pf)) a')
>   cantorcase a pf | inr b = b (Eq1trans (Eq1sym (Eq1cong a pf)) (cantorempty a b))
>  
>   absurd : Empty
>   absurd with (J_srj cantor)
>   absurd | invelmtJ a y = cantorcase a (Eq1sym y)
>  
> =====================================
>  
>  
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100107/da02565c/attachment-0001.html