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