coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>
- To: Chung Kil Hur <Chung-Kil.Hur AT pps.jussieu.fr>
- Cc: Agda mailing list <agda AT lists.chalmers.se>, coq-club AT inria.fr
- Subject: [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent
- Date: Thu, 7 Jan 2010 10:30:41 +0000
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) 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:
|
- [Coq-Club] [Agda] Agda with excluded middle is inconsistent, Chung Kil Hur
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Dan Doel
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
David Wahlstedt
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
Archive powered by MhonArc 2.6.16.