On Fri, Jun 05, 2009 at 01:58:33PM -0700, Ryan Ingram wrote:
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?
Here is a solution. I don't understand exactly why this works while various simpler things don't. {-# LANGUAGE TypeFamilies, TypeOperators, KindSignatures #-} data Z = Z data S n = S n newtype Id a = Id a newtype (a :. b) c = O (a (b c)) type family Expand x type instance Expand Z = Z type instance Expand (S a) = S (Expand a) type instance Expand (Id a) = Expand a type instance Expand ((a :. b) c) = Expand (a (b c)) type family (f :: * -> *) :^ n :: * -> * type instance f :^ Z = Id type instance f :^ (S a) = f :. (f :^ a) type Plus a = S :^ a type Times a b = Expand ((Plus a :^ b) Z) {- *Main> undefined :: Times (S (S Z)) (S (S (S Z))) <interactive>:1:0: No instance for (Show (S (S (S (S (S (S Z))))))) arising from a use of `print' at <interactive>:1:0-41 Possible fix: add an instance declaration for (Show (S (S (S (S (S (S Z))))))) In a stmt of a 'do' expression: print it -} Regards, Reid