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? Sincerely, Brad _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
