[Haskell-cafe] Type arithmetic with ATs

[Robert Greayer]

On Wed, Feb 10, 2010 at 2:29 PM, Andrew Coppin
<andrewcoppin at btinternet.com> 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?
>
> (I know for a fact that other people have done this - rule 34 requires it.)
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

With type families, something like:

type family Add m n
type instance Add (Succ n) (Succ m) = Succ (Succ (Add n m))
type instance Add Zero (Succ m) = (Succ m)
type instance Add (Succ m) Zero = (Succ m)
type instance Add Zero Zero = Zero

is this what you are after?

There's also the tfp library on hackage which has much more type level
arithmetic, using type families.