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