@@ -0,0 +1,30 @@
1+module TypeFun.Data.Peano where
2+
3+import Data.Typeable
4+import GHC.Generics (Generic)
5+import GHC.TypeLits
6+
7+data N = Z | S N
8+ deriving ( Eq, Ord, Read, Show
9+ , Generic, Typeable )
10+
11+type family ToNat (a :: N) :: Nat where
12+ ToNat Z = 0
13+ ToNat (S a) = 1 + (ToNat a)
14+
15+type family FromNat (a :: Nat) :: N where
16+ FromNat 0 = Z
17+ FromNat a = S (FromNat (a - 1))
18+
19+type family (:+:) (a :: N) (b :: N) :: N where
20+ Z :+: b = b
21+ (S a) :+: b = a :+: (S b)
22+
23+type family (:-:) (a :: N) (b :: N) :: N where
24+ a :-: Z = a
25+ (S a) :-: (S b) = a :-: b
26+
27+type family (:*:) (a :: N) (b :: N) :: N where
28+ Z :*: b = Z
29+ a :*: Z = Z
30+ (S a) :*: b = b :+: (a :*: b)