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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
