Existentially-quantified constructors, Eq and Show
Folks, Is there a less verbose way of doing this: data State a = Start | Stop | (Show a, Eq a) => State a instance Eq a => Eq (State a) where (State a) == (State b) = a == b Start == Start = True Stop == Stop = True instance Show a => Show (State a) where show (State a) = show a show Start = "Start" show Stop = "Stop" Thanks, Joel -- http://wagerlabs.com/
Hello Joel, Thursday, December 08, 2005, 1:12:07 AM, you wrote: JR> Is there a less verbose way of doing this: data (Show a, Eq a) => State a = Start | Stop | State a deriving (Show, Eq) -- Best regards, Bulat mailto:bulatz@HotPOP.com
I was also hoping that something like this would let me avoid quantifying a in functions downstream but alas, it does not happen. I have to use (Eq a, Show a) => a ... everywhere else. On Dec 7, 2005, at 11:14 PM, Bulat Ziganshin wrote:
data (Show a, Eq a) => State a = Start | Stop | State a deriving (Show, Eq)
Hello Joel, Thursday, December 08, 2005, 12:26:52 PM, you wrote: JR> I was also hoping that something like this would let me avoid JR> quantifying a in functions downstream but alas, it does not happen. I JR> have to use (Eq a, Show a) => a ... everywhere else. to avoid context declarations you can (need?) completely avoid function types declarations, as i do -- Best regards, Bulat mailto:bulatz@HotPOP.com
Doesn't this have an effect on performance? Is GHC still able to optimize things properly? On Dec 8, 2005, at 10:20 AM, Bulat Ziganshin wrote:
Hello Joel,
Thursday, December 08, 2005, 12:26:52 PM, you wrote:
JR> I was also hoping that something like this would let me avoid JR> quantifying a in functions downstream but alas, it does not happen. I JR> have to use (Eq a, Show a) => a ... everywhere else.
to avoid context declarations you can (need?) completely avoid function types declarations, as i do
Hello Joel, better to ask Simon. if automatically determined type is more generic than you really need, this can something slow program. but i think that generally this have no big impact, because many functions are just inlined and, theoretically, can be specialized just at inlining place Thursday, December 08, 2005, 3:43:56 PM, you wrote: JR> Doesn't this have an effect on performance? JR> Is GHC still able to optimize things properly? JR> On Dec 8, 2005, at 10:20 AM, Bulat Ziganshin wrote:
Hello Joel,
Thursday, December 08, 2005, 12:26:52 PM, you wrote:
JR> I was also hoping that something like this would let me avoid JR> quantifying a in functions downstream but alas, it does not happen. I JR> have to use (Eq a, Show a) => a ... everywhere else.
to avoid context declarations you can (need?) completely avoid function types declarations, as i do
JR> -- JR> http://wagerlabs.com/ -- Best regards, Bulat mailto:bulatz@HotPOP.com
Here is something else that I don't quite understand... Original version compiles: push :: Show b => State b -> Dispatcher b a -> (ScriptState a b) () push state dispatcher = do w <- get trace 95 $ "push: Pushing " ++ show state ++ " onto the stack" let s = stack w putStrict $ w { stack = (state, dispatcher):s } data State a = Start | Stop | (Show a, Eq a) => State a instance Eq a => Eq (State a) where (State a) == (State b) = a == b Start == Start = True Stop == Stop = True _ == _ = False instance Show a => Show (State a) where show (State a) = show a show Start = "Start" show Stop = "Stop" This version does not. Why does it require Eq in the ++ context? And why doesn't the other version? data (Show a, Eq a) => State a = Start | Stop | State a deriving (Eq, Show) Could not deduce (Eq b) from the context (Show b) arising from use of `show' at ./Script/Engine.hs:86:38-41 Probable fix: add (Eq b) to the type signature(s) for `push' In the first argument of `(++)', namely `show state' In the second argument of `(++)', namely `(show state) ++ " onto the stack"' -- http://wagerlabs.com/
Okay, so here you *did* get something from the existential typing :)
The type of show, restricted to State in the original version is:
show :: Show a => State a -> String
Now, in the new version, you get the type:
show :: (Eq a, Show a) => State a -> String
because what happens is that pattern matches against data constructors
of the new State type result in that class context being added to the
type of a function. The derived instance of show pattern matches
against values of the state type, and there you have it. Here's an
excerpt from: http://www.haskell.org/onlinereport/decls.html#user-defined-datatypes
================
For example, the declaration
data Eq a => Set a = NilSet | ConsSet a (Set a)
introduces a type constructor Set of kind *->*, and constructors
NilSet and ConsSet with types
NilSet :: forall a. Set a
ConsSet :: forall a. Eq a =>a ->Set a ->Set a
In the example given, the overloaded type for ConsSet ensures that
ConsSet can only be applied to values whose type is an instance of the
class Eq. Pattern matching against ConsSet also gives rise to an Eq a
constraint. For example:
f (ConsSet a s) = a
the function f has inferred type Eq a => Set a -> a. The context in
the data declaration has no other effect whatsoever.
================
This doesn't happen in the strangely existential version (which isn't
really making full use of the existential quantification) since such a
pattern matching rule doesn't apply there.
It's actually probably best to just leave the context off the type
altogether. Though this makes the type of the data constructors more
general, it probably won't cause any further trouble.
- Cale
On 08/12/05, Joel Reymont
Here is something else that I don't quite understand...
Original version compiles:
push :: Show b => State b -> Dispatcher b a -> (ScriptState a b) () push state dispatcher = do w <- get trace 95 $ "push: Pushing " ++ show state ++ " onto the stack" let s = stack w putStrict $ w { stack = (state, dispatcher):s }
data State a = Start | Stop | (Show a, Eq a) => State a
instance Eq a => Eq (State a) where (State a) == (State b) = a == b Start == Start = True Stop == Stop = True _ == _ = False
instance Show a => Show (State a) where show (State a) = show a show Start = "Start" show Stop = "Stop"
This version does not. Why does it require Eq in the ++ context? And why doesn't the other version?
data (Show a, Eq a) => State a = Start | Stop | State a deriving (Eq, Show)
Could not deduce (Eq b) from the context (Show b) arising from use of `show' at ./Script/Engine.hs:86:38-41 Probable fix: add (Eq b) to the type signature(s) for `push' In the first argument of `(++)', namely `show state' In the second argument of `(++)', namely `(show state) ++ " onto the stack"'
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Joel Reymont wrote:
Folks,
Is there a less verbose way of doing this:
data State a = Start | Stop | (Show a, Eq a) => State a
I'm curious, what is the difference between the above and... data State a = Start | Stop | State a deriving (Show, Eq) ...Does it give better error messages at compile time or something? Thanks, Greg Buchholz
On Wed, Dec 07, 2005 at 10:12:07PM +0000, Joel Reymont wrote:
data State a = Start | Stop | (Show a, Eq a) => State a
you arn't using existential types here. an example with an existential type would be (in ghc syntax)
data forall a . State = Start | Stop | (Show a, Eq a) => State a
note that what makes it existential is that 'a' does not appear as an argument to State, but rather is bound by the 'forall'. so if the above is what you want, then I believe you have the shortest way but you can add some rules to DrIFT if you want to do so automatically. if you are okay with a being an argument then
data State a = Start | Stop | State a deriving(Show,Eq)
will do what you want I believe. John PS. many, including me, feel 'forall' is a misnomer there and should be the keyword 'exists' instead. so just read 'foralls' that come _before_ the type name as 'exists' in your head and it will make more sense. John -- John Meacham - ⑆repetae.net⑆john⑈
On Wed, Dec 07, 2005 at 04:09:31PM -0800, John Meacham wrote:
you arn't using existential types here. an example with an existential type would be (in ghc syntax)
data forall a . State = Start | Stop | (Show a, Eq a) => State a
Shouldn't it be:
data State = Start | Stop | forall a . (Show a, Eq a) => State a
? Best regards Tomasz -- I am searching for a programmer who is good at least in some of [Haskell, ML, C++, Linux, FreeBSD, math] for work in Warsaw, Poland
Did someone actually try compiling this? Here are the results: data State a = Start | Stop | (Show a, Eq a) => State a deriving Show foo.hs:1:5: Can't make a derived instance of `Show (State a)' (`State' has existentially-quantified constructor(s)) When deriving instances for type `State' I do not want to do it the way Tomasz and John are suggesting below. I need the user of my library to supply their own a and be able to pattern match on it. In the library itself I just need Show and Eq a. The following does the trick (compiles, works) but sucks in its verbosity: data State a = Start | Stop | (Show a, Eq a) => State a instance Eq a => Eq (State a) where (State a) == (State b) = a == b Start == Start = True Stop == Stop = True _ == _ = False instance Show a => Show (State a) where show (State a) = show a show Start = "Start" show Stop = "Stop" On Dec 8, 2005, at 8:36 AM, John Meacham wrote:
On Thu, Dec 08, 2005 at 09:13:10AM +0100, Tomasz Zielonka wrote:
Shouldn't it be:
data State = Start | Stop | forall a . (Show a, Eq a) => State a
ah. you are right. my bad.
data (Eq a, Show a) => State a = Start | Stop | State a deriving Show
Putting the class context on the data constructor like that wasn't
doing you any more good than this way, and was causing ghc to think
that the constructor was existentially quantified.
- Cale
On 08/12/05, Joel Reymont
Did someone actually try compiling this? Here are the results:
data State a = Start | Stop | (Show a, Eq a) => State a deriving Show
foo.hs:1:5: Can't make a derived instance of `Show (State a)' (`State' has existentially-quantified constructor(s)) When deriving instances for type `State'
I do not want to do it the way Tomasz and John are suggesting below. I need the user of my library to supply their own a and be able to pattern match on it. In the library itself I just need Show and Eq a.
The following does the trick (compiles, works) but sucks in its verbosity:
data State a = Start | Stop | (Show a, Eq a) => State a
instance Eq a => Eq (State a) where (State a) == (State b) = a == b Start == Start = True Stop == Stop = True _ == _ = False
instance Show a => Show (State a) where show (State a) = show a show Start = "Start" show Stop = "Stop"
On Dec 8, 2005, at 8:36 AM, John Meacham wrote:
On Thu, Dec 08, 2005 at 09:13:10AM +0100, Tomasz Zielonka wrote:
Shouldn't it be:
data State = Start | Stop | forall a . (Show a, Eq a) => State a
ah. you are right. my bad.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Thursday 08 December 2005 09:36, John Meacham wrote:
On Thu, Dec 08, 2005 at 09:13:10AM +0100, Tomasz Zielonka wrote:
Shouldn't it be:
data State = Start
| Stop | forall a . (Show a, Eq a) => State a
ah. you are right. my bad.
But this is a rank-2 type, not an existentially quantified type? Ben
Ben,
data State = Start
| Stop | forall a . (Show a, Eq a) => State a
But this is a rank-2 type, not an existentially quantified type?
No, this one really is an existentially quantified type. An example of a data constructor with a rank-2 type would be, f.i.: data State = ... | State (forall a . (Show a, Eq a) => a) Here we have State :: (forall a . (Show a, Eq a) => a) -> State while in the existentially quantified case we had State :: forall a . (Show a, Eq a) => a -> State which has rank 1. (The rank-2 example does not make much sense, however, for the only value that can be passed to State is bottom. But, hey, it's just an example.) Regards, Stefan
On Dec 8, 2005, at 12:09 AM, John Meacham wrote:
if you are okay with a being an argument then
data State a = Start | Stop | State a deriving(Show,Eq)
will do what you want I believe.
This does the trick! Thank you! -- http://wagerlabs.com/
John Meacham wrote:
PS. many, including me, feel 'forall' is a misnomer there and should be the keyword 'exists' instead. so just read 'foralls' that come _before_ the type name as 'exists' in your head and it will make more sense.
I disagree. When you write forall a. D (P a) (Q a) it means that there's a variant of D for all types a. It's as though you had D (P Bool) (Q Bool) | D (P String) (Q String) | ... Writing exists instead would mean that there's only one version of D for some a, and you don't know what that a is; in that case you could only safely apply D to arguments of type (forall b. P b) and (forall b. Q b). I think the problem is not with the use of forall, but with the use of the term "existential type". The fact that existential quantification shows up in discussions of this language extension is a red herring. Even Haskell 98 has existential types in this sense, since (forall a. ([a] -> Int)) and ((exists a. [a]) -> Int) are isomorphic. -- Ben
On Sun, Dec 11, 2005 at 07:41:43PM +0000, Ben Rudiak-Gould wrote:
I think the problem is not with the use of forall, but with the use of the term "existential type". The fact that existential quantification shows up in discussions of this language extension is a red herring. Even Haskell 98 has existential types in this sense, since (forall a. ([a] -> Int)) and ((exists a. [a]) -> Int) are isomorphic.
this is why exists makes more sense to me :) data Foo = exists a . Foo (a -> a) now if we simply deforest the following call, f :: Foo -> Int we get f :: (exists a . a -> a) -> Int which is the same as f :: forall a . a -> a -> Int which is the type we want. however, perhaps it is an argument for data Foo = Foo (exists a . a -> a) as the syntax. John -- John Meacham - ⑆repetae.net⑆john⑈
participants (9)
-
Ben Rudiak-Gould -
Benjamin Franksen -
Bulat Ziganshin -
Cale Gibbard -
Greg Buchholz -
Joel Reymont -
John Meacham -
Stefan Holdermans -
Tomasz Zielonka