module Data.Nat where
import Unsafe.Coerce
newtype I x = I { unI :: x }
newtype K x y = K { unK :: x }
data Z
data S n
newtype Nat n = Nat Int
instance Show (Nat n) where
show = show . natToInt
z :: Nat Z
z = Nat 0
s :: Nat n -> Nat (S n)
s (Nat n) = Nat (n + 1)
natToInt :: Nat n -> Int
natToInt (Nat i) = i
data Reifiable n where
Proof :: Reify n => Reifiable n
data Exists = forall n. Ex !(Reifiable n)
reifiable :: Nat n -> Reifiable n
reifiable (Nat i) = case aux i (Ex . proof) of
Ex p -> unsafeCoerce p
where
proof :: Reify n => n -> Reifiable n
proof _ = Proof
aux :: Int -> (forall n. Reify n => n -> r) -> r
aux i k = undefined
class Reify n where
witnessNat :: Nat n
instance Reify Z where
witnessNat = z
instance Reify n => Reify (S n) where
witnessNat = s (witnessNat)
type family (:+:) a b :: *
type instance (:+:) Z n = n
type instance (:+:) (S m) n = S (m :+: n)
type family (:*:) a b :: *
type instance (:*:) Z n = Z
type instance (:*:) (S m) n = n :+: (m :*: n)
addNat :: Nat a -> Nat b -> Nat (a :+: b)
addNat (Nat a) (Nat b) = Nat (a + b)
mulNat :: Nat a -> Nat b -> Nat (a :*: b)
mulNat a b = Nat (natToInt a * natToInt b)
data NatView n where
Zero :: NatView Z
Succ :: Nat n -> NatView (S n)
view :: Nat n -> NatView n
view (Nat 0) = unsafeCoerce Zero
view (Nat (n+1)) = unsafeCoerce (Succ (Nat n))