[Agda] Agda with excluded middle is inconsistent
Dan Doel
dan.doel at gmail.com
Thu Jan 7 18:09:28 CET 2010
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
More information about the Agda
mailing list