[Haskell-cafe] Bug in GADT Implementation?

[Isaac Dupree]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

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.

Which I can in haskell...


data A
data Foo where F :: Num A => Foo

bar :: Foo -> A
bar F = 42

instance Num A where --i.e, methods = undefined
instance Show A where show _ = "A"
instance Eq A where _ == _ = True


main = print (bar F)


Program result: 'A' is printed (using ghc HEAD that is).

> 
> 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.)

although the conclusions are mathematically sound intuitionistically in
any case, and maybe the reasoning is too (I didn't consider closely).
In haskell you can get a poor rendition of pigs flying to demonstrate
how the logic works, is all :-)

Isaac
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFGWMDJHgcxvIWYTTURArOGAJ9BNXjw9dpN3nsqLsb1dc+GzoIhTwCeKGu4
kmh6jirgmam9Z6sHCKqFjdw=
=5szC
-----END PGP SIGNATURE-----