module Data.PeanoNat where
import GHC.TypeNats
import Import
data PeanoNat
= Zero
| Succ PeanoNat
addPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat
addPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat
addPeanoNat PeanoNat
Zero PeanoNat
b = PeanoNat
b
addPeanoNat (Succ PeanoNat
a) PeanoNat
b = PeanoNat -> PeanoNat
Succ forall a b. (a -> b) -> a -> b
$ PeanoNat -> PeanoNat -> PeanoNat
addPeanoNat PeanoNat
a PeanoNat
b
type Add :: PeanoNat -> PeanoNat -> PeanoNat
type family Add a b where
Add 'Zero b = b
Add ('Succ a) b = 'Succ (Add a b)
subtractFromPeanoNat :: PeanoNat -> PeanoNat -> Maybe PeanoNat
subtractFromPeanoNat :: PeanoNat -> PeanoNat -> Maybe PeanoNat
subtractFromPeanoNat PeanoNat
Zero PeanoNat
b = forall a. a -> Maybe a
Just PeanoNat
b
subtractFromPeanoNat (Succ PeanoNat
a) (Succ PeanoNat
b) = PeanoNat -> PeanoNat -> Maybe PeanoNat
subtractFromPeanoNat PeanoNat
a PeanoNat
b
subtractFromPeanoNat (Succ PeanoNat
_) PeanoNat
Zero = forall a. Maybe a
Nothing
multiplyPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat
multiplyPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat
multiplyPeanoNat PeanoNat
Zero PeanoNat
_ = PeanoNat
Zero
multiplyPeanoNat (Succ PeanoNat
a) PeanoNat
b = PeanoNat -> PeanoNat -> PeanoNat
addPeanoNat (PeanoNat -> PeanoNat -> PeanoNat
multiplyPeanoNat PeanoNat
a PeanoNat
b) PeanoNat
b
peanoToNatural :: PeanoNat -> Natural
peanoToNatural :: PeanoNat -> Natural
peanoToNatural PeanoNat
Zero = Natural
0
peanoToNatural (Succ PeanoNat
n) = forall a. Enum a => a -> a
succ forall a b. (a -> b) -> a -> b
$ PeanoNat -> Natural
peanoToNatural PeanoNat
n
naturalToPeano :: Natural -> PeanoNat
naturalToPeano :: Natural -> PeanoNat
naturalToPeano Natural
0 = PeanoNat
Zero
naturalToPeano Natural
n = PeanoNat -> PeanoNat
Succ forall a b. (a -> b) -> a -> b
$ Natural -> PeanoNat
naturalToPeano forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a
pred Natural
n
type PeanoToNatural :: PeanoNat -> Nat
type family PeanoToNatural pn where
PeanoToNatural 'Zero = 0
PeanoToNatural ('Succ pn) = PeanoToNatural pn + 1
type ListLength :: forall k. [k] -> PeanoNat
type family ListLength l where
ListLength '[] = 'Zero
ListLength (a ': aa) = 'Succ (ListLength aa)