[Haskell-cafe] Bug in GADT Implementation?

[David House]

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.

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.

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

-- 
-David House, dmhouse at gmail.com