The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

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).

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.

-- Dan