[Haskell-cafe] Is it possible to do type-level arithmetic without UndeciableInstances?

[Reid Barton]

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