[Haskell-cafe] Bug in GADT Implementation?

[Dominic Steinitz]

David House wrote:
> On 26/05/07, Dominic Steinitz <dominic.steinitz at blueyonder.co.uk> wrote:
>> This seems even worse to me. A is not inhabited so how can 42 be of
>> type A?
> 
> I think it should work. The context on the F constructor says that A
> is an instance of Num, so you could only have an F value if you could
> prove that A was an instance of Num. Therefore, when deconstructing in
> bar's pattern, if you match an F, then A must be an instance of Num,
> so to say 42 :: A is valid. F is a proof, or witness, of A's
> instantiation of Num. As A isn't, in actuality, an instance of Num,
> you can never have an F value, but that doesn't matter: all that bar
> does is express the fact that _if_ you have a value F, then it's valid
> to say 42 :: A.
> 

You are echoing my supposition as to why my example compiles. I think
I'd like to see a proof. I'm assuming the deduction rules are written
down somewhere.

> In a way, it's a bit like saying the following is a true statement:
>  If there are 8 days in the week, then pigs can fly.
> Neither of the substatements ("there are 8 days in the week" and "pigs
> can fly"), when taken by themselves, are true. However, the statement
> as a whole is true. Here are a couple of ways of explaining this:
> 
> * If you can prove that there are in fact 8 days in the week, then you
> must have a faulty logic system, so you could prove anything
> (including "pigs can fly").
> * In order to disprove the statement, you'd have to prove that "there
> are 8 days in the week" is true and simultaneously that "pigs can fly
> is false". However, you can't do this, because you could never prove
> that "there are 8 days in the week" is true. Hence, the statement
> can't be false, so it must be true.

Yes you can prove anything from an empty hypothesis.

> 
> (I'm ignoring the difference between truth and provability; think of
> my arguments as classical rather than intuitionistic.)
> 

You've lost me here. I thought classical logic assumed the law of the
excluded middle or alternatively the rule of double negation. I can't
see either of those here (and I suppose they would need to be part of
the deduction rules if they were).