Re: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
On Sun, Dec 11, 2005 at 07:41:43PM +, 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⑈ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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. John -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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. -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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 [EMAIL PROTECTED] wrote: 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. -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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 [EMAIL PROTECTED] wrote:
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/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re[2]: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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 -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[4]: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] 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/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
On Wed, Dec 07, 2005 at 10:12:07PM +, 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⑈ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existentially-quantified constructors, Eq and Show
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, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
