(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