[Haskell-cafe] Type-level naturals & multiplication
Reid Barton
rwbarton at math.harvard.edu
Mon Oct 12 03:38:20 EDT 2009
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
More information about the Haskell-Cafe
mailing list