Re: [Haskell-cafe] Type arithmetic with ATs/TFs

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