how would this be done? type classes? existential types?
hi, this is one of those situations that always make scheme and perl hackers laugh at me: i have written a piece of code that is intuitively clear, and now i am trying to turn it into something that compiles. and here it goes. i have a type class that looks something like this: class Resource a where resourceName :: a -> String resourceAdvance :: a -> a resourceStarved :: a -> Bool resourceSpend :: a -> Int -> a resourceEarn :: a -> Int -> a resource types are rice, crude oil, pizza, software code, and so on. they all have a different internal structure and the same abstract interface, that's why i have defined this type class. now i want to create a list of a type similar to [r1, r2, r3] :: (Resource a) => [a] but with r1 being pizza, r2 being crude oil, and so on. my first idea was this: data Rs = forall a . (Resource a) => Rs a unRs (Rs a) = a rsName :: Rs -> String rsName = resourceName . unRs ... and then export Rs as an abstract data type. this would allow for lists of type [Rs], which is exactly what i want. but what is the type of unRs? or better: can i make it type at all? and isn't this solution a little redundant and verbose? should i do it like in the example for existentially quantified types in the ghc manual? http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html but wouldnt't the code become really messy? or should i do the type class and instances, and then do Rs the existentially quantified way, with all class methods arguments to the Rs constructor? or is there a completely different way to do this (besides using scheme or perl :-)? thanks, matthias
You can't give unRs a type. What I usually do in this situation is to make the Rs type a Resource too. instance Resource Rs where resourceName (Rs a) = resourceName a resourceAdvance (Rs a) = Rs (resourceAdvance a) resourceStarved (Rs a) = resourceStarved a resourceSpend (Rs a) i = Rs (resourceSpend a i) resourceEarn (Rs a) i = Rs (resourceEarn a i) And then you export Rs (with some mkRs=Rs if you export it abstractly) and the Resource class. Then you can use Rs to make your heterogeneous lists and class ops to manipulate them. -- Lennart Matthias Fischmann wrote:
hi,
this is one of those situations that always make scheme and perl hackers laugh at me: i have written a piece of code that is intuitively clear, and now i am trying to turn it into something that compiles. and here it goes.
i have a type class that looks something like this:
class Resource a where resourceName :: a -> String resourceAdvance :: a -> a resourceStarved :: a -> Bool resourceSpend :: a -> Int -> a resourceEarn :: a -> Int -> a
resource types are rice, crude oil, pizza, software code, and so on. they all have a different internal structure and the same abstract interface, that's why i have defined this type class.
now i want to create a list of a type similar to
[r1, r2, r3] :: (Resource a) => [a]
but with r1 being pizza, r2 being crude oil, and so on. my first idea was this:
data Rs = forall a . (Resource a) => Rs a unRs (Rs a) = a rsName :: Rs -> String rsName = resourceName . unRs ...
and then export Rs as an abstract data type. this would allow for lists of type [Rs], which is exactly what i want.
but what is the type of unRs? or better: can i make it type at all? and isn't this solution a little redundant and verbose? should i do it like in the example for existentially quantified types in the ghc manual?
http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html
but wouldnt't the code become really messy? or should i do the type class and instances, and then do Rs the existentially quantified way, with all class methods arguments to the Rs constructor? or is there a completely different way to do this (besides using scheme or perl :-)?
thanks, matthias
------------------------------------------------------------------------
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Matthias Fischmann wrote:
hi,
this is one of those situations that always make scheme and perl hackers laugh at me: i have written a piece of code that is intuitively clear, and now i am trying to turn it into something that compiles. and here it goes.
i have a type class that looks something like this:
class Resource a where resourceName :: a -> String resourceAdvance :: a -> a resourceStarved :: a -> Bool resourceSpend :: a -> Int -> a resourceEarn :: a -> Int -> a
resource types are rice, crude oil, pizza, software code, and so on.
If there is a known list of resources, then they could all be a single data type.
they all have a different internal structure and the same abstract interface, that's why i have defined this type class.
now i want to create a list of a type similar to
[r1, r2, r3] :: (Resource a) => [a]
The above only works if r1 :: a, r2 :: a, and r3 :: a But this is not what you want, since pizza and crude oil are different types.
but with r1 being pizza, r2 being crude oil, and so on. my first idea was this:
data Rs = forall a . (Resource a) => Rs a unRs (Rs a) = a rsName :: Rs -> String rsName = resourceName . unRs ...
and then export Rs as an abstract data type. this would allow for lists of type [Rs], which is exactly what i want.
but what is the type of unRs? or better: can i make it type at all?
No. You cannot make unRs like that.
and isn't this solution a little redundant and verbose? should i do it like in the example for existentially quantified types in the ghc manual?
http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html
but wouldnt't the code become really messy? or should i do the type class and instances, and then do Rs the existentially quantified way, with all class methods arguments to the Rs constructor? or is there a completely different way to do this (besides using scheme or perl :-)?
thanks, matthias
But you can make a list of such things: (Why isn't it "resourceName :: String" ?) class Resource a where resourceName :: a -> String resourceAdvance :: a -> a resourceStarved :: a -> Bool resourceSpend :: a -> Int -> a resourceEarn :: a -> Int -> a data R where { R :: Resource a => a -> R } instance Resource R where resourceName (R a) = resourceName a resourceAdvance (R a) = R (resourceAdvance a) resourceStarved (R a) = resourceStarved a resourceSpend (R a) i = R (resourceSpend a i) resourceEarn (R a) i = R (resourceEarn a i) data Pizza=Pizza data Oil=Oil instance Resource Pizza where resourceName _ = "pizza" instance Resource Oil where resourceName _ = "oil" list = [R Pizza, R Oil] names = map resourceName list -- Chris
On Thu, Mar 16, 2006 at 12:40:00PM +0000, Chris Kuklewicz wrote:
(Why isn't it "resourceName :: String" ?)
because i am too clumsy. (-: when i am trying this, ghc complains that the type of resourceName doesn't have any occurrance of 'a', and i feel that it must be harder for the type engine to figure things out if there isn't, so resourceName is still a mapping from resources to their names. did i miss anything? m.
Matthias Fischmann wrote:
On Thu, Mar 16, 2006 at 12:40:00PM +0000, Chris Kuklewicz wrote:
(Why isn't it "resourceName :: String" ?)
when i am trying this, ghc complains that the type of resourceName doesn't have any occurrance of 'a', and i feel that it must be harder for the type engine to figure things out if there isn't, so resourceName is still a mapping from resources to their names.
Yes, if you had resourceName :: forall a. Resource a => String then there'd be nothing to prevent the expression (resourceName :: String) from evaluating to any resource name in any context. A trick you can pull is to define data Proxy a = Proxy and give resourceName's parameter the type Proxy a instead of a. This makes it clear that it's only the type you care about, not the value. The downside is that it tends to be less convenient to use, which is presumably why standard library functions with this problem (like floatRadix and sizeOf) don't use this solution. -- Ben
On Thu, Mar 16, 2006 at 12:57:54PM +0100, Matthias Fischmann wrote:
i have a type class that looks something like this:
class Resource a where resourceName :: a -> String resourceAdvance :: a -> a resourceStarved :: a -> Bool resourceSpend :: a -> Int -> a resourceEarn :: a -> Int -> a
resource types are rice, crude oil, pizza, software code, and so on. they all have a different internal structure and the same abstract interface, that's why i have defined this type class.
now i want to create a list of a type similar to
[r1, r2, r3] :: (Resource a) => [a]
but with r1 being pizza, r2 being crude oil, and so on.
The existential is equivalent to a recursive type, as in this solution (in Haskell 98): data ResourceProperties a = ResourceProperties { resourceName :: String, resourceAdvance :: a, resourceStarved :: Bool, resourceSpend :: Int -> a, resourceEarn :: Int -> a } instance Functor ResourceProperties where fmap f p = ResourceProperties { resourceName = resourceName p, resourceAdvance = f (resourceAdvance p), resourceStarved = resourceStarved p, resourceSpend = f . resourceSpend p, resourceEarn = f . resourceEarn p } class Resource a where resourceProperties :: a -> ResourceProperties a newtype Rs = Rs (ResourceProperties Rs) instance Resource Rs where resourceProperties (Rs r) = r mkRs :: Resource a => a -> Rs mkRs = Rs . fmap mkRs . resourceProperties There won't be an unRs.
Matthias Fischmann wrote:
now i want to create a list of a type similar to
[r1, r2, r3] :: (Resource a) => [a]
but with r1 being pizza, r2 being crude oil, and so on.
The type you actually want here is [exists a. (Resource a) && a], but no Haskell implementation supports that.
data Rs = forall a . (Resource a) => Rs a unRs (Rs a) = a rsName :: Rs -> String rsName = resourceName . unRs ...
[...]
but what is the type of unRs?
Its type is (Rs -> (exists a. (Resource a) && a)), but again no Haskell implementation supports that. -- Ben
Ben Rudiak-Gould wrote:
Matthias Fischmann wrote:
now i want to create a list of a type similar to
[r1, r2, r3] :: (Resource a) => [a]
but with r1 being pizza, r2 being crude oil, and so on.
The type you actually want here is [exists a. (Resource a) && a], but no Haskell implementation supports that.
Is there a reason for using && instead of [exists a. Resource a=>a] ? Also, am I right in thinking that the reason why no implementation supports this is as follows: a) A value 'v' of type 'exists a. Resource a=>a 'would have to be internally represented as something like (dictResource_t, value_t) and b) Given such a value, there is no syntactic way to distinguish the pair from the value_t stored inside it, unlike the use of 'forall' where the syntax for the constructor conveniently "represents" any dictionaries that have been glued onto the value (ie pattern matching against R x gives us back the dictionaries "R" and the plain value x)? Hope I'm not making this more confusing but I'm still trying to get my head around all these invisible happenings regarding dictionaries so I can visualise what's happening in terms of bytes and pointers in the runtime.... Thanks, Brian.
Brian Hulley wrote:
Is there a reason for using && instead of
[exists a. Resource a=>a]
?
Only that => looks like a function arrow, && looks like a tuple. I stole this notation from an unpublished paper by SimonPJ et al on adding existential quantification to Haskell. I'm not especially attached to it. Actually I rather like forall a | Resource a. a exists a | Resource a. a
a) A value 'v' of type 'exists a. Resource a=>a 'would have to be internally represented as something like (dictResource_t, value_t)
Yes.
b) Given such a value, there is no syntactic way to distinguish the pair from the value_t stored inside it, unlike the use of 'forall' where the syntax for the constructor conveniently "represents" any dictionaries that have been glued onto the value (ie pattern matching against R x gives us back the dictionaries "R" and the plain value x)?
Yes, but that doesn't necessarily mean you can't work out when to construct and deconstruct these implicit tuples. That's exactly what the type inference process does with implicit type arguments, and implicit type returns are dual to that, so the process should be similar. It is tricky, though. E.g. given (f (g "z")) where f :: forall a. [a] -> Int g :: String -> (exists b. [b]) in principle you should be able to call g first, getting a type b and a list [b], then instantiate f with the type b, then pass the list to it, ultimately getting an Int. But I don't know how to design a type inference algorithm that will find this typing. If on the other hand f :: (exists a. [a]) -> Int then it's easy to do the right thing---which is a little odd since these two types for f are otherwise indistinguishable.
Hope I'm not making this more confusing but I'm still trying to get my head around all these invisible happenings regarding dictionaries so I can visualise what's happening in terms of bytes and pointers in the runtime....
Once you understand where the types go in System F, the dictionaries are easy: they always follow the types around. Any time you have forall a b c. (C1 a b, C2 b c) => ... in the source, you have five corresponding parameters/arguments in GHC Core, one for each type variable and constraint. These are always passed around as a unit (at least prior to optimization). In principle you could box them in a 5-tuple. The dictionary values are nothing more or less than proofs that the corresponding constraints hold. -- Ben
Ben Rudiak-Gould wrote:
Brian Hulley wrote:
Is there a reason for using && instead of
[exists a. Resource a=>a]
?
Only that => looks like a function arrow, && looks like a tuple. I stole this notation from an unpublished paper by SimonPJ et al on adding existential quantification to Haskell. I'm not especially attached to it. Actually I rather like
forall a | Resource a. a exists a | Resource a. a
The bar is certainly consistent with the use in guards etc, but would lead to: exists a | (Show a, Eq a) . a which looks a bit clunky because of the need for () as well because of the comma (to limit the scope of the comma). Also, it might be confusing to have to use a different notation to qualify type variables just because these type variables are being existentially qualified, when => is used everywhere else. Personally I'd get rid of => altogether, and enclose constraints in {} eg foo :: forall a {Resource a} a -- dot is optional after } bar :: {Show a, Eq a} a->Bool [exists a {Resource a} a] class {Monad m} MonadIO m where ... This would fit into the rest of the syntax for Haskell as it stands at the moment. [snip]
It is tricky, though. E.g. given (f (g "z")) where
f :: forall a. [a] -> Int g :: String -> (exists b. [b])
in principle you should be able to call g first, getting a type b and a list [b], then instantiate f with the type b, then pass the list to it, ultimately getting an Int. But I don't know how to design a type inference algorithm that will find this typing. If on the other hand
f :: (exists a. [a]) -> Int
then it's easy to do the right thing---which is a little odd since these two types for f are otherwise indistinguishable.
If the two types for f are indistinguishable, perhaps the forall in f's type could be converted into an existential as a kind of normal form before doing type inference?
Hope I'm not making this more confusing but I'm still trying to get my head around all these invisible happenings regarding dictionaries so I can visualise what's happening in terms of bytes and pointers in the runtime....
Once you understand where the types go in System F, the dictionaries are easy: they always follow the types around. Any time you have
forall a b c. (C1 a b, C2 b c) => ...
in the source, you have five corresponding parameters/arguments in GHC Core, one for each type variable and constraint. These are always passed around as a unit (at least prior to optimization). In principle you could box them in a 5-tuple. The dictionary values are nothing more or less than proofs that the corresponding constraints hold.
Thanks, this helps a lot, Brian.
participants (6)
-
Ben Rudiak-Gould -
Brian Hulley -
Chris Kuklewicz -
Lennart Augustsson -
Matthias Fischmann -
Ross Paterson