module Data.Type.Nat where
import Data.Type.Equality
import Data.Type.Product
import Type.Class.Known
import Type.Class.Witness
import Type.Family.Constraint
import Type.Family.List
import Type.Family.Nat
data Nat :: N -> * where
Z_ :: Nat Z
S_ :: !(Nat n) -> Nat (S n)
deriving instance Eq (Nat n)
deriving instance Ord (Nat n)
deriving instance Show (Nat n)
instance Known Nat Z where
known = Z_
instance Known Nat n => Known Nat (S n) where
type KnownC Nat (S n) = Known Nat n
known = S_ known
instance Witness ØC (Known Nat n) (Nat n) where
(\\) r = \case
Z_ -> r
S_ x -> r \\ x
instance TestEquality Nat where
testEquality = \case
Z_ -> \case
Z_ -> Just Refl
S_ _ -> Nothing
S_ x -> \case
Z_ -> Nothing
S_ y -> testEquality x y /? qed
instance DecEquality Nat where
decideEquality = \case
Z_ -> \case
Z_ -> Proven _Z
S_ _ -> Refuted _ZneS
S_ x -> \case
Z_ -> Refuted $ _ZneS . sym
S_ y -> (_S <-> _s) <?> decideEquality x y
_Z :: Z :~: Z
_Z = Refl
_S :: x :~: y -> S x :~: S y
_S Refl = Refl
_s :: S x :~: S y -> x :~: y
_s Refl = Refl
_ZneS :: Z :~: S x -> Void
_ZneS = impossible
addZ :: Nat x -> (x + Z) :~: x
addZ = \case
Z_ -> Refl
S_ x -> _S $ addZ x
addS :: Nat x -> Nat y -> S (x + y) :~: (x + S y)
addS = \case
Z_ -> pure Refl
S_ x -> _S . addS x
(.+) :: Nat x -> Nat y -> Nat (x + y)
(.+) = \case
Z_ -> id
S_ x -> S_ . (x .+)
infixr 6 .+
(.*) :: Nat x -> Nat y -> Nat (x * y)
(.*) = \case
Z_ -> const Z_
S_ x -> (.+) <$> (x .*) <*> id
infixr 7 .*
(.^) :: Nat x -> Nat y -> Nat (x ^ y)
(.^) x = \case
Z_ -> S_ Z_
S_ y -> (x .^ y) .* x
infixl 8 .^
nat :: Nat n -> Int
nat = \case
Z_ -> 0
S_ x -> succ $ nat x
n0 :: Nat N0
n1 :: Nat N1
n2 :: Nat N2
n3 :: Nat N3
n4 :: Nat N4
n5 :: Nat N5
n6 :: Nat N6
n7 :: Nat N7
n8 :: Nat N8
n9 :: Nat N9
n10 :: Nat N10
n0 = Z_
n1 = S_ n0
n2 = S_ n1
n3 = S_ n2
n4 = S_ n3
n5 = S_ n4
n6 = S_ n5
n7 = S_ n6
n8 = S_ n7
n9 = S_ n8
n10 = S_ n9