[Haskell-cafe] More experiments with ATs
wren ng thornton
wren at freegeek.org
Tue Jul 6 01:55:02 EDT 2010
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
More information about the Haskell-Cafe
mailing list