Type-level Naturals

Number.hs

{-# OPTIONS_GHC -fglasgow-exts #-}
{-# LANGUAGE UndecidableInstances #-}

data S a
data Z

newtype Number s = Num ()

class AsInt n where
    asInt :: Number n -> Int

anyNum :: Number s
anyNum = Num ()

instance AsInt Z where
    asInt _ = 0
instance AsInt n => AsInt (S n) where
    asInt _ = asInt (anyNum :: Number n) + 1

instance (AsInt n) => Show (Number n) where
    show = show . asInt

zero :: Number Z
zero = anyNum
suck :: Number s -> Number (S s)
suck _ = anyNum

type family a :+: b
type instance Z :+: b = b
type instance (S a) :+: b = S (a :+: b)

add :: Number a -> Number b -> Number (a:+:b)
add _ _ = anyNum

type family a :*: b
type instance Z :*: b = Z
type instance (S a) :*: b = b :+: (a :*: b) -- needs -XUndecidableInstances

mult :: Number a -> Number b -> Number (a:*:b)
mult _ _ = anyNum