[Haskell-cafe] Type arithmetic with ATs/TFs

[Andrew Coppin]

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...