[Haskell-cafe] Type-level naturals & multiplication

[Manuel M T Chakravarty]

Brad Larsen:
> 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?

No, not at the moment.  The reasons are explained in the paper "Type  
Checking with Open Type Functions" (ICFP'08):

   http://www.cse.unsw.edu.au/~chak/papers/tc-tfs.pdf

We want to eventually add closed *type families* to the system (ie,  
families where you can't add new instances in other modules).  For  
such closed families, we should be able to admit more complex  
instances without requiring undecidable instances.

Manuel