<html><head><base href="x-msg://283/"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Dear Chung,<div><br></div><div>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?</div><div><br></div><div>Surely, type constructors should not be injective in general. A definition of the form</div><div><br></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>data I : (Set -> Set) -> Set where </div><div><br></div><div>should be expandable by an annonymous declaration </div><div><br></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>I : (Set -> Set) -> Set</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>I F = data {}</div><div><br></div><div>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).</div><div><br></div><div>Clearly I is just a constant function and hence not injective. </div><div><br></div><div>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.</div><div><br></div><div>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. </div><div><br></div><div>First of all, clearly it is not essential that I is empty, your proof goes through with</div><div><br></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>data I : (Set -> Set) -> Set where </div><div><span class="Apple-tab-span" style="white-space:pre"> </span> inI : I (¥ë x ¡æ x)</div><div><br></div> without any problems. Interestingly, the proof still goes through if we turn the first argument into a parameter<div><br></div><div><span class="Apple-tab-span" style="white-space:pre"> </span> data I (F : Set -> Set) : Set where </div><div><span class="Apple-tab-span" style="white-space:pre"> </span> inI : I F</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>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. </div><div><br></div><div>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.</div><div><br></div><div>Cheers,</div><div>Thorsten</div><div><div><br></div><div><span class="Apple-tab-span" style="white-space:pre"> </span><br><div><div><br><div><br></div><div><br><div><div>On 6 Jan 2010, at 23:44, Chung Kil Hur wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div bgcolor="#ffffff"><div><font size="2" face="Arial">Hi everyone,</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">I proved the absurdity in Agda assuming the excluded middle.</font></div><div><font size="2" face="Arial">Is it a well-known fact ?</font></div><div><font size="2" face="Arial">It seems that Agda's set theory is weird.</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">This comes from the injectivity of inductive type constructors.</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">The proof sketch is as follows.</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">Define a family of inductive type</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">data I : (Set -> Set) -> Set where</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">with no constructors.</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">By injectivity of type constructors, I can show that I : (Set -> Set) -> Set is injective.</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">As you may see, there is a size problem with this injectivity.</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">So, I just used the cantor's diagonalization to derive absurdity in a classical way.</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">Does anyone know whether cantor's diagonalization essentially needs the classical axiom, or can be done intuitionistically ?</font></div><div><font size="2" face="Arial">If the latter is true, then Agda system is inconsistent.</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">Please have a look at the Agda code below.</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">Any comments are wellcome.</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">Best regards,</font></div><div><font size="2" face="Arial">Chung-Kil Hur</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">============== Agda code ===============</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">module cantor where</font></div><div><font size="2"></font> </div><div><font size="2" face="Arial"> data Empty : Set where</font></div><div> </div><div><font size="2" face="Arial"> data One : Set where<br> one : One</font></div><div> </div><div><font size="2" face="Arial"> data coprod (A : Set1) (B : Set1) : Set1 where<br> inl : ¢£ (a : A) -> coprod A B<br> inr : ¢£ (b : B) -> coprod A B</font></div><div> </div><div><font size="2" face="Arial"> postulate exmid : ¢£ (A : Set1) -> coprod A (A -> Empty)</font></div><div> </div><div><font size="2" face="Arial"> data Eq1 {A : Set1} (x : A) : A -> Set1 where<br> refleq1 : Eq1 x x</font></div><div> </div><div><font size="2" face="Arial"> cast : ¢£ { A B } -> Eq1 A B -> A -> B<br> cast refleq1 a = a</font></div><div> </div><div><font size="2" face="Arial"> Eq1cong : ¢£ {f g : Set -> Set} a -> Eq1 f g -> Eq1 (f a) (g a)<br> Eq1cong a refleq1 = refleq1</font></div><div> </div><div><font size="2" face="Arial"> Eq1sym : ¢£ {A : Set1} { x y : A } -> Eq1 x y -> Eq1 y x<br> Eq1sym refleq1 = refleq1</font></div><div> </div><div><font size="2" face="Arial"> Eq1trans : ¢£ {A : Set1} { x y z : A } -> Eq1 x y -> Eq1 y z -> Eq1 x z<br> Eq1trans refleq1 refleq1 = refleq1</font></div><div> </div><div><font size="2" face="Arial"> data I : (Set -> Set) -> Set where</font></div><div> </div><div><font size="2" face="Arial"> Iinj : ¢£ { x y : Set -> Set } -> Eq1 (I x) (I y) -> Eq1 x y<span class="Apple-converted-space"> </span><br> Iinj refleq1 = refleq1</font></div><div> </div><div><font size="2" face="Arial"> data invimageI (a : Set) : Set1 where<br> invelmtI : forall x -> (Eq1 (I x) a) -> invimageI a</font></div><div> </div><div><font size="2" face="Arial"> J : Set -> (Set -> Set)<br> J a with exmid (invimageI a)<br> J a | inl (invelmtI x y) = x<br> J a | inr b = ¥ë x ¡æ Empty</font></div><div> </div><div><font size="2" face="Arial"> data invimageJ (x : Set -> Set) : Set1 where<br> invelmtJ : forall a -> (Eq1 (J a) x) -> invimageJ x</font></div><div> </div><div><font size="2" face="Arial"> IJIeqI : ¢£ x -> Eq1 (I (J (I x))) (I x)<br> IJIeqI x with exmid (invimageI (I x))<br> IJIeqI x | inl (invelmtI x' y) = y<br> IJIeqI x | inr b with b (invelmtI x refleq1)<br> IJIeqI x | inr b | ()</font></div><div> </div><div><font size="2" face="Arial"> J_srj : ¢£ (x : Set -> Set) -> invimageJ x<br> J_srj x = invelmtJ (I x) (Iinj (IJIeqI x))</font></div><div> </div><div><font size="2" face="Arial"> cantor : Set -> Set<br> cantor a with exmid (Eq1 (J a a) Empty)<br> cantor a | inl a' = One<br> cantor a | inr b = Empty</font></div><div> </div><div><font size="2" face="Arial"> OneNeqEmpty : Eq1 One Empty -> Empty<br> OneNeqEmpty p = cast p one</font></div><div> </div><div><font size="2" face="Arial"> cantorone : ¢£ a -> Eq1 (J a a) Empty -> Eq1 (cantor a) One<span class="Apple-converted-space"> </span><br> cantorone a p with exmid (Eq1 (J a a) Empty)<br> cantorone a p | inl a' = refleq1<br> cantorone a p | inr b with b p<br> cantorone a p | inr b | ()</font></div><div> </div><div><font size="2" face="Arial"> cantorempty : ¢£ a -> (Eq1 (J a a) Empty -> Empty) -> Eq1 (cantor a) Empty<br> cantorempty a p with exmid (Eq1 (J a a) Empty)<br> cantorempty a p | inl a' with p a'<br> cantorempty a p | inl a' | ()<br> cantorempty a p | inr b = refleq1</font></div><div> </div><div><font size="2" face="Arial"> cantorcase : ¢£ a -> Eq1 cantor (J a) -> Empty<br> cantorcase a pf with exmid (Eq1 (J a a) Empty)<br> cantorcase a pf | inl a' = OneNeqEmpty (Eq1trans (Eq1trans (Eq1sym (cantorone a a')) (Eq1cong a pf)) a')<br> cantorcase a pf | inr b = b (Eq1trans (Eq1sym (Eq1cong a pf)) (cantorempty a b))</font></div><div> </div><div><font size="2" face="Arial"> absurd : Empty<br> absurd with (J_srj cantor)<br> absurd | invelmtJ a y = cantorcase a (Eq1sym y)</font></div><div><font size="2" face="Arial"></font> </div><div><font size="2" face="Arial">=====================================</font></div><div> </div><div><font size="2" face="Arial"></font> </div>_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br></div></blockquote></div><br></div></div></div></div></div></body></html>