[Haskell-cafe] Type-level naturals & multiplication

[Reid Barton]

On Sat, Oct 10, 2009 at 02:59:37PM -0400, Brad Larsen wrote:
> Suppose we implement type-level naturals as so:
> 
> data Zero
> data Succ a
> 
> Then, we can reflect the type-level naturals into a GADT as so (not
> sure if ``reflect'' is the right terminology here):
> 
> data Nat :: * -> * where
>   Zero :: Nat Zero
>   Succ :: Nat a -> Nat (Succ a)
> 
> Using type families, we can then proceed to define type-level addition:
> 
> type family Add a b :: *
> type instance Add Zero b = b
> type instance Add (Succ a) b = Succ (Add a b)
> 
> Is there any way to define type-level multiplication without requiring
> undecidable instances?

I hesitate to contradict Manuel Chakravarty on this subject... but I
posted a type-level multiplication program without undecidable
instances on this list in June:

http://www.haskell.org/pipermail/haskell-cafe/2009-June/062452.html

If you prefer to use EmptyDataDecls, you can replace the first four
lines by

data Z
data S n

data Id :: * -> *
data (:.) :: (* -> *) -> (* -> *) -> (* -> *)

And I still don't understand why that definition works while
the obvious one doesn't :)

Regards,
Reid Barton