[Haskell-cafe] More experiments with ATs

[wren ng thornton]

Andrew Coppin wrote:
> Brent Yorgey wrote:
>> On Sun, Jul 04, 2010 at 10:31:34AM +0100, Andrew Coppin wrote:   
>>> I have literally no idea what a type family is. I understand ATs (I 
>>> think!), but TFs make no sense to me.
>>>     
>>
>> ATs are just TFs which happen to be associated with a particular
>> class.  So if you understand ATs then you understand TFs too, you just
>> didn't know it. =)
>>   
> 
> How would that make sense though? I'm having trouble forming a mental 
> image of how / why you'd use that...

Type families ---in the traditional dependent-types sense, not 
necessarily the GHC sense--- are a collection of related types which are 
"the same" in some sense, but which are distinguished from one another 
by indices.

There are two ways of interpreting this. The first approach is to think 
about type families where the index gives you some type-level 
information about the term-level value; this is the same thing as GADTs. 
That is, if we take the standard whipping boy:

     data List :: * -> * -> * where
         nil   :: forall a. List a Z
         cons  :: forall a. a -> List a n -> List a (S n)

then we'll want some way of talking about "all Lists", irrespective of 
their lengths. Thus, "List A" (for some A) is a type family, but not a 
type. There's a fundamental difference here between parametric 
polymorphism and type indices. In Coq it's made more explicit (though 
it's still rendered subtle), but in Haskell it can be a bit harder to see.


The other perspective is to think of type families as a function from 
indices to types, where the particular function constitutes the type 
family. This is the approach taken by associated types and type families 
in GHC. TFs, as separate from ATs, are useful for implementing 
type-level functions. For example, we could define addition on Z and S, 
which would allow us to give the type

     (++) :: List a n -> List a m -> List a (Plus n m)

The type family Plus takes two indices and returns a type, but it does 
so in a way that it is allowed to perform case analysis on the input 
arguments--- and therefore is not parametric.

-- 
Live well,
~wren