The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Hi Dan,

On Jan 7, 2010, at 6:09 PM, Dan Doel wrote:

> On Thursday 07 January 2010 11:24:30 am Noam Zeilberger wrote:
> > 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.
>
> Yes, I hadn't been thinking of this particular example before, but  
> one can ask
> the question: when is
>
>  I F -> I G
>
> a valid type for
>
>  foo x = x
>
> ? If the data declaration turns into something like
>
>  I : (Set -> Set) -> Set
>  I _ = data {}
>
> Then the answer is, "always." The signature evaluates to
>
>  data {} -> data {}
>
> irrespective of what F and G are. However, this isn't true in Agda  
> now, where
> the answer to the question is, I believe, only when F = G. Which  
> means that
> type checking considers datatype constructors to be injective. And I  
> expect
> things will stay that way, because having to know how a source  
> language
> desugars into a core language to figure out what source terms are  
> well-typed
> strikes me as inelegant. For instance, is
>
>  data Nat1 = zero1 | suc1 Nat1
>  data Nat2 = zero2 | suc2 Nat2
>
>  foo : Nat1 -> Nat2
>  foo n = n
>
> valid? If the core language is an OTT-style 0, 1, 2, Pi, Sigma, W,  
> then the
> answer in the core language is probably "yes". But a core language  
> like Pi-
> Sigma might disagree (I think).

The answer is no, since there is a semantics which refutes this.

Also, we do not strive for completeness of Agda type checking wrt. to  
some semantics.  Soundness is enough, and we want decidability.

> So type constructors in the source language might retain the  
> appearance of
> injectivity regardless of whether their representation in the core  
> language
> is, or whether such a principle is given as it currently is in Agda,  
> due to
> that making typing sensible.

Exactly.

Cheers,

Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41