The Coq mailing list

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

>> We should justify principles like this (i.e. all type constructors are 
>> injective) by a semantic explanation or by a translation into a well 
>> understood core language e.g. (extensional) Marttin-Loef Type Theory with 
>> W-types and universes. I don't know any such explanation which would 
>> justify this principle. Moreover, Chung's example shows that this is not 
>> possible (without giving up something else) since pure type theory is 
>> consistent with EM.
> 
> Agreed that there should be a convincing explanation, but again, I do
> think there is a strong intuition behind the principle (what Dan Doel
> and I were getting at), and the fact that it plays an important role
> in typechecking suggests that we shouldn't jump to conclusions.

I am not sure about this. *Most* datatype constructors are injective on type 
names, hence in functional programming one overgeneralizes this to *all*. 
Indeed this is one of the reasons that it is not clear how to add lambda 
abstractions on type level to Haskell, because Haskell assumes that all 
functions on the type level are injective. 

>  I am
> not sure that Agda should be conservative over classical mathematics:
> it seems there is a fundamental tension between exploiting the full
> power of a constructive type theory and upholding the fictions of
> classical mathematics.  Chung-Kil's paradox shows that you can't
> reason classically in Agda just by adding the law of excluded middle
> -- okay, so don't do it that way.

I don't think this is an instance of a constructive principle which is not 
valid classically (such as continuity). It seems rather an instance of 
something being wrong but not wrong enough to make the theory inconsistent. 
Another example is the propositional axiom of choice which is wrong but it 
doesn't make the theory inconsistent but only entails EM (by the Diaconescu 
construction). I mean being able to derive either EM or ~ EM are indications 
that something is wrong in these cases,

> Could you explain what you meant by: "Also while we may accept that
> extensions of Type Theory may be anticlassical, we should expect that
> core Type Theory is consistent with EM."?

In Martin-Loef Type Theory you cannot refute EM and I would expect that the 
same holds for Agda. Thinking about this, I wouldn't insist on this too 
strongly, but I'd need a better reason than "injectivity of type 
constructors". E.g. the observation that a function of type (Nat -> Nat) -> 
Nat can only use a finite amount of information of its input (i.e. 
continuity) we may want to built into our type theory (but how ?).

Cheers,
Thorsten