かたれべるのやつ

typelevel.hs

{-# LANGUAGE FunctionalDependencies, FlexibleInstances, UndecidableInstances,
             ScopedTypeVariables #-}

data Z
data S a
data P a

class ToNum a where
    num :: Num b => a -> b
instance ToNum Z where
    num _ = 0
instance ToNum a => ToNum (S a) where
    num _ = 1  + num (undefined :: a)
instance ToNum a => ToNum (P a) where
    num _ = -1 + num (undefined :: a)

zero = undefined :: Z
one  = undefined :: S Z
mone = undefined :: P Z

class Neg a b | a -> b
instance Neg Z Z
instance Neg a b => Neg (S a) (P b)
instance Neg a b => Neg (P a) (S b)

class Add a b c | a b -> c
instance Add Z Z Z
instance Add (S a) Z (S a)
instance Add (P a) Z (P a)
instance Add Z (S b) (S b)
instance Add Z (P b) (P b)
instance Add a b c => Add (S a) (P b) c
instance Add a b c => Add (P a) (S b) c
instance Add a b c => Add (S a) (S b) (S (S c))
instance Add a b c => Add (P a) (P b) (P (P c))

add :: Add a b c => a -> b -> c
add = undefined

two  = add one one

class Sub a b c | a b -> c
instance (Neg b b', Add a b' c) => Sub a b c

sub :: Sub a b c => a -> b -> c
sub = undefined