RE: GADT + Newtype deriving = Erroneous errors
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#newtype-deriving Simon | -Original Message- | From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] 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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GADT + Newtype deriving = Erroneous errors
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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GADT + Newtype deriving = Erroneous errors
On Mon, Mar 26, 2007 at 09:18:34PM -0700, Stefan O'Rear wrote:
[EMAIL PROTECTED]:/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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GADT + Newtype deriving = Erroneous errors
Tomasz Zielonka wrote:
On Mon, Mar 26, 2007 at 09:18:34PM -0700, Stefan O'Rear wrote:
[EMAIL PROTECTED]:/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.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GADT + Newtype deriving = Erroneous errors
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
Re: GADT + Newtype deriving = Erroneous errors
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.)
[EMAIL PROTECTED]:/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.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GADT + Newtype deriving = Erroneous errors
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.)
[EMAIL PROTECTED]:/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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GADT + Newtype deriving = Erroneous errors
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. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
