Re: [Haskell-cafe] Bug in GADT Implementation?

David House wrote:

On 26/05/07, Dominic Steinitz 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).