{-# LANGUAGE TypeFamilies #-} module PeanoArith

data Z = Z data S n = S n

So, this type family works just fine:

type family Plus a b type instance Plus Z b = b type instance Plus (S a) b = S (Plus a b)

As does this one:

type family Minus a b type instance Minus a Z = Z type instance Minus Z (S b) = Z type instance Minus (S a) (S b) = Minus a b

But this one doesn't work without UndecidableInstances:

type family Times a b type instance Times Z b = Z type instance Times (S a) b = Plus b (Times a b)

I tried several different implementations for Times but I was unable to come up with one that passed the type family termination checker. Is there a way to do so? Some examples of attempts:

-- (a+1)*(b+1) = ab + a + b + 1 type family Times1 a b type instance Times1 Z Z = Z type instance Times1 (S n) Z = Z type instance Times1 Z (S n) = Z type instance Times1 (S a) (S b) = S (Plus (Times1 a b) (Plus a b))

-- inline Plus type family Times2_H a b acc type Times2 a b = Times2_H a b Z type instance Times2_H a b (S acc) = S (Times2_H a b acc) type instance Times2_H Z b Z = Z type instance Times2_H (S a) b Z = Times2_H a b b

Do you have any other ideas? Is (a*b) too big for the termination checker to ever accept? -- ryan