Type Families

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Type Families

Alexander Solla-2
(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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type Families

Dan Doel
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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type Families

Felipe Lessa
In reply to this post by Alexander Solla-2
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.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe