Bug in GADT Implementation?

Dominic Steinitz

26 May 2007 26 May '07

5:10 p.m.

I would expect foo r@(Range BITSTRING _ _) x = [] to give an error but it doesn't. Writing t = Range BITSTRING gives one so why not the pattern match? Dom. data BitString = BitString [Bool] deriving Show data ConstrainedType :: * -> * where INTEGER :: ConstrainedType Int BITSTRING :: ConstrainedType BitString Seq :: ConstrainedType a -> ConstrainedType b -> ConstrainedType (a,b) Range :: Ord a => ConstrainedType a -> a -> a -> ConstrainedType a foo :: ConstrainedType a -> a -> [Int] foo BITSTRING (BitString x) = map fromEnum x foo INTEGER x = [x] foo r@(Range INTEGER _ _) x = [upperInt r,x] foo r@(Range BITSTRING _ _) x = [] r1 = Range INTEGER 20 40 r2 = Range r1 25 45 upperInt :: ConstrainedType Int -> Int upperInt INTEGER = 256 upperInt (Range t l u) = min u (upperInt t)

Show replies by date

Roberto Zunino

26 May 26 May

8 p.m.

Dominic Steinitz wrote:

...

I would expect

foo r@(Range BITSTRING _ _) x = []

to give an error but it doesn't. Writing

t = Range BITSTRING

gives one so why not the pattern match?

AFAICS, this is because when you construct a value, as in t, you have to provide the required context (Ord in this case) or face an error. OTOH, when you destruct a value, you simply get the context back and you are not required to provide anything, so no type error is generated. This works in HEAD: data A data Foo where F :: Num A => Foo bar :: Foo -> A bar F = 42 Regards, Zun.

Dominic Steinitz

7:51 p.m.

Roberto Zunino wrote:

...

Dominic Steinitz wrote:

...
I would expect

foo r@(Range BITSTRING _ _) x = []

to give an error but it doesn't. Writing

t = Range BITSTRING

gives one so why not the pattern match?

AFAICS, this is because when you construct a value, as in t, you have to provide the required context (Ord in this case) or face an error. OTOH, when you destruct a value, you simply get the context back and you are not required to provide anything, so no type error is generated.

This works in HEAD:

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

bar :: Foo -> A bar F = 42

Regards, Zun.

Zun, This seems even worse to me. A is not inhabited so how can 42 be of type A? BTW this doesn't compile in 6.6. I suppose I could read my example as "if there is anything that matches Range BITSTRING _ _ then do the following" and since nothing can ever match it then it's a redundant case. But I would expect the compiler to at least warn me that nothing can ever match this. Dom.

David House

8:48 p.m.

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. 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@gmail.com

Dominic Steinitz

9:52 p.m.

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

Isaac Dupree

11:20 p.m.

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 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.

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

Arie Peterson

11:27 p.m.

Dominic Steinitz wrote:

...

I suppose I could read my example as "if there is anything that matches Range BITSTRING _ _ then do the following" and since nothing can ever match it then it's a redundant case. But I would expect the compiler to at least warn me that nothing can ever match this.

Why is there nothing that can match 'Range BITSTRING _ _'? Some other module may define an instance 'Ord BitString'. Kind regards, Arie -- making someone not survive must surely count as non-verbal communication - bring

Simon Peyton-Jones

28 May 28 May

4:16 p.m.

| > I suppose I could read my example as "if there is anything that matches | > Range BITSTRING _ _ then do the following" and since nothing can ever | > match it then it's a redundant case. But I would expect the compiler to | > at least warn me that nothing can ever match this. | | Why is there nothing that can match 'Range BITSTRING _ _'? | | Some other module may define an instance 'Ord BitString'. Arie's right -- that's the reason. In general, rejecting code because it can't possibly be executed is nice when GHC can be absolutely definitely sure that it can't be executed. But if there's any doubt at all, it has to accept the program. After all, if the function can't be called, there's no harm to soundness. But if it's certain that the code is dead, its better to report it sooner. Simon

6615

Age (days ago)

6617

Last active (days ago)

List overview

Download

7 comments

6 participants

participants (6)

Arie Peterson
David House
Dominic Steinitz
Isaac Dupree
Roberto Zunino
Simon Peyton-Jones

Bug in GADT Implementation?

tags

participants (6)