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