Actually, at least in GHC, associated types are just syntax sugar for type families. That is, this code: class Container c where type Element c :: * view :: c -> Maybe (Element c,c) instance Container [a] where type Element [a] = a view [] = Nothing view (x:xs) = Just (x,xs) is the same as this code: type family Element c :: * class Container c where view :: c -> Maybe (Element c, c) type instance Container [a] = a instance Container [a] where view [] = Nothing view (x:xs) = Just (x,xs) -- ryan On Thu, Feb 11, 2010 at 1:10 PM, Andrew Coppin wrote:

Andrew Coppin wrote:

...

OK, so I sat down today and tried this, but I can't figure out how.

There are various examples of type-level arithmetic around the place. For example,

http://www.haskell.org/haskellwiki/Type_arithmetic

(This is THE first hit on Google, by the way. Haskell is apparently THAT popular!) But this does type arithmetic using functional dependencies; what I'm trying to figure out is how to do that with associated types.

Any hints?

Several people have now replied to this, both on and off-list. But all the replies use type families, not associated types.

Now type families are something I don't yet comprehend. (Perhaps the replies will help... I haven't studied them yet.) What I understand is that ATs allow you to write things like

 class Container c where   type Element c :: *   ...

And now you can explicitly talk about the kind of element a container can hold, rather than relying on the type constructor having a particular kind or something. So the above works for containers that can hold *anything* (such as lists), containers which can only hold *one* thing (e.g., ByteString), and containers which can hold only certain things (e.g., Set).

...which is great. But I can't see a way to use this for type arithmetic. Possibly because I don't have a dramatically solid mental model of exactly how it works. You'd *think* that something like

 class Add x y where   type Sum x y :: *

 instance Add x y => Add (Succ x) y where   type Sum (Succ x) y = Succ (Sum x y)

ought to work, but apparently not.

As to what type families - type declarations outside of a class - end up meaning, I haven't the vaguest idea. The Wiki page makes it sound increadibly complicated...

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Fri, Feb 12, 2010 at 2:11 PM, Andrew Coppin wrote:

OK, well in that case, I'm utterly puzzled as to why both forms exist in the first place. If TFs don't allow you to do anything that can't be done with ATs, why have them?

My head hurts...

I think the question is the reverse -- why do ATs exist when you can do everything with the more general Type Families? This is the answer from the GHC documentation: "Type families appear in two flavours: (1) they can be defined on the toplevel or (2) they can appear inside type classes (in which case they are known as associated type synonyms). The former is the more general variant, as it lacks the requirement for the type-indices to coincide with the class parameters. However, the latter can lead to more clearly structured code and compiler warnings if some type instances were - possibly accidentally - omitted." http://www.haskell.org/haskellwiki/GHC/Indexed_types#Detailed_definition_of_...

On Fri, Feb 12, 2010 at 2:10 PM, Edward Kmett wrote:

On Fri, Feb 12, 2010 at 2:11 PM, Andrew Coppin wrote:

...

OK, well in that case, I'm utterly puzzled as to why both forms exist in the first place. If TFs don't allow you to do anything that can't be done with ATs, why have them?

My head hurts...

s/GADT/Fundep/g ?

You can say anything you might say with type families using GADTs, but you'll often be talking about stuff you don't care about. =)

sometimes you don't care what the Element type of a container is, just that it is a container. Yet using GADTs you must always reference the content type.

size :: Container' c e => c -> Int -- using Container' defined with GADTs

as opposed to

size :: Container c => c -> Int

That doesn't seem like a huge sacrifice at first, until you start considering things like:

http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/...

Instead of just being able to talk about a CCC based on the type used for its homomorphisms, now I must constantly talk about the type used for its product, and exponentials, and the identity of the product, even when I don't care about those properties!

This ability to not talk about those extra types becomes useful when you start defining data types.

Say you define a simple imperative growable hash data type, parameterized over the monad type. You could do so with TFs fairly easily:

newtype Hash m k v = Hash (Ref m (Array Int (Ref m [(k,v)]))) empty :: MonadRef m => m (Hash m k v) insert :: (Hashable k, MonadRef m) => k -> v -> Hash m k v -> m ()

But the GADT version leaks implementation-dependent details out to the data type:

newtype Hash r k v = Hash (r (Array Int (r [(k,v)]))) empty :: MonadRef m r => m (Hash r k v) insert :: (Hashable k, MonadRef m r) => k -> v -> Hash r k v -> m ()

This gets worse as you need more and more typeclass machinery.

On the other hand, GADTs are useful when you want to define multidirectional mutual dependencies without repeating yourself. Each is a win in terms of the amount of boilerplate you have to write in different circumstances.

class Foo a b c | a b -> c, b c -> a, c a -> b where     foo :: a -> b -> c

would require 3 different class associate types, one for each fundep.

-Edward Kmett _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Robert Greayer wrote:

What Ryan said, and here's an example of addition with ATs, specifically (not thoroughly tested, but tested a little). The translation to TFs sans ATs is straightforward.

class Add a b where type SumType a b

instance Add Zero Zero where type SumType Zero Zero = Zero

instance Add (Succ a) Zero where type SumType (Succ a) Zero = Succ a

instance Add Zero (Succ a) where type SumType Zero (Succ a) = Succ a

instance Add (Succ a) (Succ b) where type SumType (Succ a) (Succ b) = Succ (Succ (SumType a b))

I'm pretty sure this is almost exactly what I wrote in the first place, and it didn't work. I'll try again and see if I get anywhere...