The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

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