[Haskell-cafe] Is it possible to do type-level arithmetic
without UndeciableInstances?
Reid Barton
rwbarton at math.harvard.edu
Fri Jun 5 17:39:49 EDT 2009
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
More information about the Haskell-Cafe
mailing list