[Haskell-cafe] Type-level naturals & multiplication
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Tue Oct 13 01:23:04 EDT 2009
Reid Barton:
> 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 :)
Ok, I should have been more precise. It's not that anything about
multiplication as such is a problem. However, when you look at the
standard definitions for addition
> type family Add a b :: *
> type instance Add Zero b = b
> type instance Add (Succ a) b = Succ (Add a b)
and multiplication
> type family Mul a b :: *
> type instance Mul Zero b = Zero
> type instance Mul (Succ a) b = Add (Mul a b) b
then the difference is that multiplication uses nested applications of
type families (namely, Add (Mul a b) b). It is this nested
application of type families that can be abused to construct programs
that lead to non-termination of type checking (by exploiting the
openness of type families in combination with local equalities
introduced either by equality constraints in type signatures or GADT
pattern matches). Unfortunately, there doesn't seem to be a simple
syntactic criterion that would let GHC decide between harmless and
problematic uses of nested *open* family applications in family
instances. Hence, we need to rule them all out.
You circumvent that problem cleverly by the use of higher-kinded types.
Manuel
More information about the Haskell-Cafe
mailing list