module TypeFun.Data.Peano
( N(..)
, KnownPeano(..)
, ToNat
, FromNat
, (:+:)
, (:-:)
, (:*:)
) where
import Data.Typeable
import GHC.Generics (Generic)
import GHC.TypeLits
data N = Z | S N
deriving ( N -> N -> Bool
(N -> N -> Bool) -> (N -> N -> Bool) -> Eq N
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: N -> N -> Bool
$c/= :: N -> N -> Bool
== :: N -> N -> Bool
$c== :: N -> N -> Bool
Eq, Eq N
Eq N
-> (N -> N -> Ordering)
-> (N -> N -> Bool)
-> (N -> N -> Bool)
-> (N -> N -> Bool)
-> (N -> N -> Bool)
-> (N -> N -> N)
-> (N -> N -> N)
-> Ord N
N -> N -> Bool
N -> N -> Ordering
N -> N -> N
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: N -> N -> N
$cmin :: N -> N -> N
max :: N -> N -> N
$cmax :: N -> N -> N
>= :: N -> N -> Bool
$c>= :: N -> N -> Bool
> :: N -> N -> Bool
$c> :: N -> N -> Bool
<= :: N -> N -> Bool
$c<= :: N -> N -> Bool
< :: N -> N -> Bool
$c< :: N -> N -> Bool
compare :: N -> N -> Ordering
$ccompare :: N -> N -> Ordering
$cp1Ord :: Eq N
Ord, ReadPrec [N]
ReadPrec N
Int -> ReadS N
ReadS [N]
(Int -> ReadS N)
-> ReadS [N] -> ReadPrec N -> ReadPrec [N] -> Read N
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [N]
$creadListPrec :: ReadPrec [N]
readPrec :: ReadPrec N
$creadPrec :: ReadPrec N
readList :: ReadS [N]
$creadList :: ReadS [N]
readsPrec :: Int -> ReadS N
$creadsPrec :: Int -> ReadS N
Read, Int -> N -> ShowS
[N] -> ShowS
N -> String
(Int -> N -> ShowS) -> (N -> String) -> ([N] -> ShowS) -> Show N
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [N] -> ShowS
$cshowList :: [N] -> ShowS
show :: N -> String
$cshow :: N -> String
showsPrec :: Int -> N -> ShowS
$cshowsPrec :: Int -> N -> ShowS
Show
, (forall x. N -> Rep N x) -> (forall x. Rep N x -> N) -> Generic N
forall x. Rep N x -> N
forall x. N -> Rep N x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep N x -> N
$cfrom :: forall x. N -> Rep N x
Generic, Typeable )
class KnownPeano (p :: N) where
peanoVal :: proxy p -> Integer
instance KnownPeano Z where
peanoVal :: proxy 'Z -> Integer
peanoVal proxy 'Z
_ = Integer
0
instance (KnownPeano n) => KnownPeano (S n) where
peanoVal :: proxy ('S n) -> Integer
peanoVal proxy ('S n)
_ = Integer -> Integer
forall a. Enum a => a -> a
succ (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (p :: N) (proxy :: N -> *).
KnownPeano p =>
proxy p -> Integer
peanoVal (Proxy n
forall k (t :: k). Proxy t
Proxy :: Proxy n)
type family ToNat (a :: N) :: Nat where
ToNat Z = 0
ToNat (S a) = 1 + (ToNat a)
type family FromNat (a :: Nat) :: N where
FromNat 0 = Z
FromNat a = S (FromNat (a - 1))
type family (:+:) (a :: N) (b :: N) :: N where
Z :+: b = b
(S a) :+: b = a :+: (S b)
type family (:-:) (a :: N) (b :: N) :: N where
a :-: Z = a
(S a) :-: (S b) = a :-: b
type family (:*:) (a :: N) (b :: N) :: N where
Z :*: b = Z
a :*: Z = Z
(S a) :*: b = b :+: (a :*: b)