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