[Agda] Agda with excluded middle is inconsistent
Andreas Abel
andreas.abel at ifi.lmu.de
Thu Jan 7 18:23:17 CET 2010
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
More information about the Agda
mailing list