GADT + Newtype deriving = Erroneous errors
This code causes GHC to incorrectly fail - the case *is* reachable. (I invented this technique in an attempt to directly access the internal System FC newtype coercion; it promised until a few minutes ago to solve all the EnumMap performance concerns.) stefan@stefans:/tmp$ cat A.lhs
{-# OPTIONS_GHC -fglasgow-exts #-}
data IsIntT x where IsIntT :: IsIntT Int
class IsIntC a where isInt :: IsIntT a instance IsIntC Int where isInt = IsIntT
newtype Foo = Foo Int deriving(IsIntC)
x :: IsIntT Foo -> Int x IsIntT = (Foo 2) + 2
y = x (isInt :: IsIntT Foo) stefan@stefans:/tmp$ ghci -v0 A.lhs
A.lhs:11:4: Inaccessible case alternative: Can't match types `Foo' and `Int' In the pattern: IsIntT In the definition of `x': x IsIntT = (Foo 2) + 2 Stefan
Stefan O'Rear wrote:
This code causes GHC to incorrectly fail - the case *is* reachable. (I invented this technique in an attempt to directly access the internal System FC newtype coercion; it promised until a few minutes ago to solve all the EnumMap performance concerns.)
stefan@stefans:/tmp$ cat A.lhs
{-# OPTIONS_GHC -fglasgow-exts #-}
data IsIntT x where IsIntT :: IsIntT Int
class IsIntC a where isInt :: IsIntT a instance IsIntC Int where isInt = IsIntT
newtype Foo = Foo Int deriving(IsIntC)
x :: IsIntT Foo -> Int x IsIntT = (Foo 2) + 2
IsIntT Foo is a concrete type. IsIntT has concrete type IsInt Int. These types cannot possibly match. This may be what you want:
{-# OPTIONS_GHC -fglasgow-exts #-} data IsIntT :: * -> * where IsIntT :: IsIntT Int
class IsIntC a where isInt :: IsIntT a instance IsIntC Int where isInt = IsIntT
newtype Foo = Foo Int deriving(IsIntC)
x :: IsIntT free -> Int x IsIntT = 2
y = x (isInt :: IsIntT Foo)
Note that (Foo 2) + 2 is an attempt to add a Foo and an Int, which cannot possibly compile. So I replaced it with just a 2.
On Tue, Mar 27, 2007 at 11:32:29AM +0100, Chris Kuklewicz wrote:
Stefan O'Rear wrote:
This code causes GHC to incorrectly fail - the case *is* reachable. (I invented this technique in an attempt to directly access the internal System FC newtype coercion; it promised until a few minutes ago to solve all the EnumMap performance concerns.)
stefan@stefans:/tmp$ cat A.lhs
{-# OPTIONS_GHC -fglasgow-exts #-}
data IsIntT x where IsIntT :: IsIntT Int
class IsIntC a where isInt :: IsIntT a instance IsIntC Int where isInt = IsIntT
newtype Foo = Foo Int deriving(IsIntC)
x :: IsIntT Foo -> Int x IsIntT = (Foo 2) + 2
IsIntT Foo is a concrete type. IsIntT has concrete type IsInt Int. These types cannot possibly match.
Sure they can. This is an attempt to torture-test GHC. Using newtype deriving, I have constructed a non-bottom value of type IsIntT Foo. Thus, the value is evidence of the fact that the newtype is isomorphic to the base type. In the language of GHC HEAD, it is a value-level reification of the coercion used to implement the newtype in System FC (although the same bogus error occurs with 6.4.2, 6.6, 6.7.20070213, 6.7.20070223, and 6.7.20070323). GHC seems to be making the (unwaranted!) assumption that distinct concrete types can never be unified - but they CAN, and the compiler is failing my torture test. (BTW, why is the inaccessible alternative an error rather than a warning?)
Note that (Foo 2) + 2 is an attempt to add a Foo and an Int, which cannot possibly compile. So I replaced it with just a 2.
Why not? They are the same type, and I have Curry-Howard proof of this fact. Stefan
Stefan O'Rear:
They are the same type, and I have Curry-Howard proof of this fact.
If that's the case, then it begs the question why you'd bother defining Foo in the first place. How would this solve EnumMap performance concerns? I am under the impression that newtypes are *defined* to be distinct types which don't unify. You haven't shown us your proof, but if it contradicts the definition, then it probably says more about the definition (or some other construct you've used) than any implementation derived from it.
Stefan O'Rear wrote:
On Tue, Mar 27, 2007 at 11:32:29AM +0100, Chris Kuklewicz wrote:
Stefan O'Rear wrote:
newtype Foo = Foo Int deriving(IsIntC)
Note that (Foo 2) + 2 is an attempt to add a Foo and an Int, which cannot possibly compile. So I replaced it with just a 2.
Why not? They are the same type, and I have Curry-Howard proof of this fact.
Stefan
Foo is isomorphic to Int in structure. But it is not the same type. Foo is a new type that is distinct from Int. That means I get type safety -- you cannot pass an Int to a function that expects a Foo and vice versa. Since (+) is defined as (Num a => a->a->a) it cannot add type different types and thus you *cannot* add a Foo and an Int. This (+) is allowed, since "type" is just shorthand:
type Bar = Int
x :: Bar x = 2 y :: Int y = 3 z = x+y
This (+) is not allowed, since "data" declares a new type:
data Bar = Bar Int deriving (Num)
x :: Bar x = Bar 2 y :: Int y = 3 z = x+y
This (+) is not allowed, since "newtype" declares a new type:
newtype Bar = Bar Int deriving (Num)
x :: Bar x = Bar 2 y :: Int y = 3 z = x+y
On Wed, Mar 28, 2007 at 12:03:41PM +0100, Chris Kuklewicz wrote:
Stefan O'Rear wrote:
On Tue, Mar 27, 2007 at 11:32:29AM +0100, Chris Kuklewicz wrote:
Stefan O'Rear wrote:
newtype Foo = Foo Int deriving(IsIntC)
Note that (Foo 2) + 2 is an attempt to add a Foo and an Int, which cannot possibly compile. So I replaced it with just a 2.
Why not? They are the same type, and I have Curry-Howard proof of this fact.
Stefan
Foo is isomorphic to Int in structure. But it is not the same type. Foo is a new type that is distinct from Int. That means I get type safety -- you cannot pass an Int to a function that expects a Foo and vice versa. Since (+) is defined as (Num a => a->a->a) it cannot add type different types and thus you *cannot* add a Foo and an Int.
Well, I thought I had a non-bottom value of type IsIntT Foo, but when I tried to seq it ghc crashed: http://hackage.haskell.org/trac/ghc/ticket/1251 Let's postpone this discussion until the people who maintain the typechecker have a chance to rule :) Stefan
We don't have to wait for the type checkers to rule. The semantics of GADTs is pretty clear (if it's implemented correctly is another matter). If you write data IsIntT x where IsIntT :: IsIntT Int then there is only one (non-bottom) value in the IsIntT families of types and that is IsIntT::IsInt Int And since Haskell uses nominal type equality there is no type equal to Int that is not Int. The fact that you can derive IsIntC looks like a good ole' bug to me. -- Lennart On Mar 28, 2007, at 23:22 , Stefan O'Rear wrote:
On Wed, Mar 28, 2007 at 12:03:41PM +0100, Chris Kuklewicz wrote:
Stefan O'Rear wrote:
On Tue, Mar 27, 2007 at 11:32:29AM +0100, Chris Kuklewicz wrote:
Stefan O'Rear wrote:
newtype Foo = Foo Int deriving(IsIntC)
Note that (Foo 2) + 2 is an attempt to add a Foo and an Int, which cannot possibly compile. So I replaced it with just a 2.
Why not? They are the same type, and I have Curry-Howard proof of this fact.
Stefan
Foo is isomorphic to Int in structure. But it is not the same type. Foo is a new type that is distinct from Int. That means I get type safety -- you cannot pass an Int to a function that expects a Foo and vice versa. Since (+) is defined as (Num a => a->a->a) it cannot add type different types and thus you *cannot* add a Foo and an Int.
Well, I thought I had a non-bottom value of type IsIntT Foo, but when I tried to seq it ghc crashed: http://hackage.haskell.org/trac/ghc/ ticket/1251
Let's postpone this discussion until the people who maintain the typechecker have a chance to rule :)
Stefan _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Right. There are two things going on in this thread. First, when you say newtype T = MkT Int then T and Int are distinct types. Adding a deriving( whatever ) doesn't change that fact. Earlier messages make this point. The second is that GHC's current "newtype deriving" mechanism is plain wrong. It's one of those feature-interaction things. Something that used to work fine (newtype deriving) breaks when you elaborate an apparently unrelated feature (GADTs). Stefan has helpfully boiled out a bug report http://hackage.haskell.org/trac/ghc/ticket/1251. Thank you Stefan. I'm nose-down in ICFP mode at the moment, but I'll look at it after that deadline. Meanwhile, it's clear that the rules for "newtype deriving" need to be refined. Would anyone like to have a go at refining them? http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html... Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On | Behalf Of Lennart Augustsson | Sent: 29 March 2007 00:29 | To: Stefan O'Rear | Cc: glasgow-haskell-users@haskell.org | Subject: Re: GADT + Newtype deriving = Erroneous errors | | We don't have to wait for the type checkers to rule. The semantics | of GADTs is pretty clear (if it's implemented correctly is another | matter). If you write | data IsIntT x where | IsIntT :: IsIntT Int | then there is only one (non-bottom) value in the IsIntT families of | types and that is IsIntT::IsInt Int | | And since Haskell uses nominal type equality there is no type equal | to Int that is not Int. | | The fact that you can derive IsIntC looks like a good ole' bug to me. | | -- Lennart | | | On Mar 28, 2007, at 23:22 , Stefan O'Rear wrote: | | > On Wed, Mar 28, 2007 at 12:03:41PM +0100, Chris Kuklewicz wrote: | >> Stefan O'Rear wrote: | >>> On Tue, Mar 27, 2007 at 11:32:29AM +0100, Chris Kuklewicz wrote: | >>>> Stefan O'Rear wrote: | >> | >>>>>> newtype Foo = Foo Int deriving(IsIntC) | >>>>>> | >> | >>> | >>>> Note that (Foo 2) + 2 is an attempt to add a Foo and an Int, | >>>> which cannot | >>>> possibly compile. So I replaced it with just a 2. | >>> | >>> Why not? They are the same type, and I have Curry-Howard proof | >>> of this fact. | >>> | >>> Stefan | >> | >> Foo is isomorphic to Int in structure. But it is not the same | >> type. Foo is a | >> new type that is distinct from Int. That means I get type safety | >> -- you cannot | >> pass an Int to a function that expects a Foo and vice versa. | >> Since (+) is | >> defined as (Num a => a->a->a) it cannot add type different types | >> and thus you | >> *cannot* add a Foo and an Int. | > | > Well, I thought I had a non-bottom value of type IsIntT Foo, but when | > I tried to seq it ghc crashed: http://hackage.haskell.org/trac/ghc/ | > ticket/1251 | > | > Let's postpone this discussion until the people who maintain the | > typechecker have a chance to rule :) | > | > Stefan | > _______________________________________________ | > Glasgow-haskell-users mailing list | > Glasgow-haskell-users@haskell.org | > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones wrote:
Generally speaking GHC will inline *across* modules just as much as it does *within* modules, with a single large exception.
If GHC sees that a function 'f' is called just once, it inlines it regardless of how big 'f' is. But once 'f' is exported, GHC can never see that it's called exactly once, even if that later turns out to be the case. This inline-once optimisation is pretty important in practice.
So: do not export functions that are not used outside the module (i.e. use an explicit export list, and keep it as small as possible).
This is very interesting to know, as it explains a strange effect that I was seeing: I had an algorithm and I began to add variants of it as separate functions in the same module. Then I saw the original function (which I had not touched) get slower and slower. I even wondered if the compiler was not maybe taking common parts of my functions out of them to reduce the evaluations making my original function slower, but then it was that it wasn't inlining anymore some functions. This means the with haskell (with ghc) cleaning up old code and keeping the modules as clean as possible pays off even more than in other languages... good to know, and very important when benchmarking various algorithms: commenting out a variant is better as having it as separate function.... Fawzi
woops sorry for the previous post, the subject was wrong... this one is correct. Simon Peyton-Jones wrote:
Generally speaking GHC will inline *across* modules just as much as it does *within* modules, with a single large exception.
If GHC sees that a function 'f' is called just once, it inlines it regardless of how big 'f' is. But once 'f' is exported, GHC can never see that it's called exactly once, even if that later turns out to be the case. This inline-once optimisation is pretty important in practice.
So: do not export functions that are not used outside the module (i.e. use an explicit export list, and keep it as small as possible).
This is very interesting to know, as it explains a strange effect that I was seeing: I had an algorithm and I began to add variants of it as separate functions in the same module. Then I saw the original function (which I had not touched) get slower and slower. I even wondered if the compiler was not maybe taking common parts of my functions out of them to reduce the evaluations making my original function slower, but then it was that it wasn't inlining anymore some functions. This means the with haskell (with ghc) cleaning up old code and keeping the modules as clean as possible pays off even more than in other languages... good to know, and very important when benchmarking various algorithms: commenting out a variant is better as having it as separate function.... Fawzi
On Mon, Mar 26, 2007 at 09:18:34PM -0700, Stefan O'Rear wrote:
stefan@stefans:/tmp$ cat A.lhs
{-# OPTIONS_GHC -fglasgow-exts #-}
data IsIntT x where IsIntT :: IsIntT Int
class IsIntC a where isInt :: IsIntT a instance IsIntC Int where isInt = IsIntT
newtype Foo = Foo Int deriving(IsIntC)
I think newtype deriving should be rejected in this case. Maybe this is the real problem here? Best regards Tomek
Tomasz Zielonka wrote:
On Mon, Mar 26, 2007 at 09:18:34PM -0700, Stefan O'Rear wrote:
stefan@stefans:/tmp$ cat A.lhs
{-# OPTIONS_GHC -fglasgow-exts #-}
data IsIntT x where IsIntT :: IsIntT Int
class IsIntC a where isInt :: IsIntT a instance IsIntC Int where isInt = IsIntT
newtype Foo = Foo Int deriving(IsIntC)
I think newtype deriving should be rejected in this case. Maybe this is the real problem here?
Best regards Tomek
On reflection, I agree. The derived instance would have to be
instance IsIntC Foo where isInt :: IsIntT Foo isInt = isIntT
which cannot type check. Only
instance IsIntC Foo where isInt :: IsIntT Foo isInt = undefined
is possible.
participants (7)
-
Chris Kuklewicz -
Fawzi Mohamed -
Lennart Augustsson -
Matthew Brecknell -
Simon Peyton-Jones -
Stefan O'Rear -
Tomasz Zielonka