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