(I'm using a fixed width font, so if you don't see nice formatting, you need to use a fixed width font. This is literate Haskell, but I copied and pasted the code. YMMV) Hi Everybody! (Hi Dr. Nick) I've been looking for a good way to use some richer notions of polymorphism than Haskell98 allows. First, I tried to define a monad "of" the things I want to quantify over (so each "type of view" or "type of evaluable thing" would be a constructor in a monadic type.) But that didn't seem to offer the kind of extensibility I wanted, since I basically want to join several types together. I tried FunDeps next, and that worked okay, but it was a bit difficult to keep track of what was "meant" to do what. I guess I could have plowed through the work, but it wasn't any fun. I finally heard about TypeFamilies, and they seem to give me the kind of extensibility I want, while keeping the theoretical foundations relatively clean. But I am not so sure I understand them. Let us consider the code:
type AbstractValue = Int class Evaluate asset where data Value asset :: * value :: (Value asset) -> AbstractValue
That's easy enough. "Value asset" is an indexed type. That is reflected in the instance declaration:
instance Evaluate Abstract where data Value Abstract = AbstractValue Abstract value (AbstractValue int) = int
Okay, easy enough. But what happens when we want to "add" Evaluate instances?
data Add a b = Add a b instance ( Evaluate a , Evaluate b ) => Evaluate (Add a b) where data Value (Sum a b) = SumValue (Sum a b)
Even this much is straightforward. We require a and b to be Evaluate'able before we can find the sum of a and b as "values". Now I want to write my definition for the "value" function. But... how is that supposed to work? My first guess is value (SumValue (Sum a b)) = (value a) + (value b) But I more-or-less expected that to fail. I realize I need some more typing information. What am I supposed to fill in? My next guess was
value (SumValue (Sum a b)) = (value $ Value a) + (value $ Value
b) But Value doesn't exist as a type constructor. So now that I am starting to "get" what's going on, I wonder why I don't get what's going on. Since I need to use a type constructor for the (Value a) and (Value b) "things", it kind of defeats the point. (I hesitate to say "value", since I have been using "value" to mean the result/blah of an Evaluate instance) Speaking of which, I am still not sure what the difference between associate data type families and associated type constructor families are. The former use the data keyword in class declarations, and the latter use type keywords. What can I do with one and not the other? I would really appreciate some guidance. Thanks! Alex
On Sunday 20 September 2009 9:43:53 pm Alexander Solla wrote:
But I more-or-less expected that to fail. I realize I need some more typing information. What am I supposed to fill in? My next guess was
value (SumValue (Sum a b)) = (value $ Value a) + (value $ Value
b)
But Value doesn't exist as a type constructor. So now that I am starting to "get" what's going on, I wonder why I don't get what's going on. Since I need to use a type constructor for the (Value a) and (Value b) "things", it kind of defeats the point. (I hesitate to say "value", since I have been using "value" to mean the result/blah of an Evaluate instance)
Well, the obvious answer is that you should instead write data Value (Add a b) = SumValue (Sum (Value a) (Value b)) So that they are already Values, and value can be called on them. I don't really understand what you're using the data families for, though. Value looks like sort of an identity wrapper around its argument.
Speaking of which, I am still not sure what the difference between associate data type families and associated type constructor families are. The former use the data keyword in class declarations, and the latter use type keywords. What can I do with one and not the other?
Type families (as far as their use in classes goes) are for when the associated type already exists. For instance, in a collection class: class Collection c where type Elem c :: * ... You'll have instances: instance Collection [a] where type Elem [a] = a ... By contrast, data families are for when you want to define new data types indexed by the type. For instance, if you're doing generalized tries: class Key k where data Trie k :: * -> * ... Then: instance (Key k) => Key [k] where data Trie [k] a = ListTrie (Maybe a) (Trie k (Trie [k] a)) ... You can, of course, approximate one with the other. If you use a data family, you can use newtypes so there's no additional overhead (but you'll have to sprinkle constructors in your code). And data families can be simulated like (using the Trie example): class Key k where type Trie k :: * -> * ... data ListTrie k a = ListTrie (Maybe a) (Trie k (ListTrie k a)) instance Key k => Key [k] where type Trie [k] = ListTrie k ... But in cases where you're writing lots of new data/newtype declarations, just to refer to them with an associated type, you may was well use associated data instead and remove the middle man. Of course, sometimes you may not be clearly in either situation, so it may be a judgment call. Type families are also useful if you want to do computation at the type level. In that sense, type families are like (value-level) functions, and data families are like (value-level) constructors (I think that's accurate). Hope that helped a bit, -- Dan
On Sun, Sep 20, 2009 at 06:43:53PM -0700, Alexander Solla wrote:
data Add a b = Add a b instance ( Evaluate a , Evaluate b ) => Evaluate (Add a b) where
Okay.
data Value (Sum a b) = SumValue (Sum a b)
Hmmm, have you tried
data Value (Add a b) = AddValue (Value a) (Value b)
Now your 'value' function would be
value (AddValue va vb) = value va + value vb
because you're holding 'Value a' and 'Value b', not 'a' and 'b'. It may help to think as if this class represented a container. For value, do you need the whole container or just one of its elements? I know other will give a better explanation, but maybe this is enough to get you in the right track :). HTH, -- Felipe.
participants (3)
-
Alexander Solla -
Dan Doel -
Felipe Lessa