module Data.TypeNat.Nat (
Nat(..)
, IsNat(..)
, LTE(..)
, Zero
, One
, Two
, Three
, Four
, Five
, Six
, Seven
, Eight
, Nine
, Ten
) where
data Nat = Z | S Nat
type Zero = Z
type One = S Z
type Two = S One
type Three = S Two
type Four = S Three
type Five = S Four
type Six = S Five
type Seven = S Six
type Eight = S Seven
type Nine = S Eight
type Ten = S Nine
class IsNat (n :: Nat) where
natRecursion :: (forall m . b -> a m -> a (S m)) -> (b -> a Z) -> (b -> b) -> b -> a n
instance IsNat Z where
natRecursion _ ifZ _ = ifZ
instance IsNat n => IsNat (S n) where
natRecursion ifS ifZ reduce x = ifS x (natRecursion ifS ifZ reduce (reduce x))
class LTE (n :: Nat) (m :: Nat) where
lteInduction :: (forall k . LTE (S k) m => d k -> d (S k)) -> d n -> d m
lteRecursion :: (forall k . LTE n k => d (S k) -> d k) -> d m -> d n
instance LTE n n where
lteInduction f x = x
lteRecursion f x = x
instance LTE n m => LTE n (S m) where
lteInduction
:: forall (d :: Nat -> *) .
(forall (k :: Nat) . LTE (S k) (S m) => d k -> d (S k))
-> d n
-> d (S m)
lteInduction f x =
let sub :: d m
sub = lteInduction f x
in f sub
lteRecursion f x = lteRecursion f (f x)