@@ -1,5 +1,6 @@
1module TypeFun.Data.Peano
1module TypeFun.Data.Peano
@@ -7,14 +8,24 @@ module TypeFun.Data.Peano
10−import Data.Typeable
11+import Data.Typeable
11−import GHC.Generics (Generic)
12+import GHC.Generics (Generic)
12−import GHC.TypeLits
13+import GHC.TypeLits
14data N = Z | S N
15data N = Z | S N
15 deriving ( Eq, Ord, Read, Show
16 deriving ( Eq, Ord, Read, Show
16 , Generic, Typeable )
17 , Generic, Typeable )
20+class KnownPeano (p :: N) where
21+ peanoVal :: proxy p -> Integer
23+instance KnownPeano Z where
26+instance (KnownPeano n) => KnownPeano (S n) where
27+ peanoVal _ = succ $ peanoVal (Proxy :: Proxy n)
18type family ToNat (a :: N) :: Nat where
29type family ToNat (a :: N) :: Nat where
19 ToNat Z = 0
30 ToNat Z = 0
20 ToNat (S a) = 1 + (ToNat a)
31 ToNat (S a) = 1 + (ToNat a)