]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Typing/Peano.hs
Update to lastest symantic-document
[haskell/symantic.git] / symantic / Language / Symantic / Typing / Peano.hs
1 {-# LANGUAGE GADTs #-}
2 -- | Natural numbers inductivey defined at the type-level, and of kind @*@.
3 module Language.Symantic.Typing.Peano where
4
5 import Data.Type.Equality
6
7 -- * Types 'Zero' and 'Succ'
8 data Zero
9 data Succ p
10
11 -- ** Type synonyms for a few numbers
12 type P0 = Zero
13 type P1 = Succ P0
14 type P2 = Succ P1
15 type P3 = Succ P2
16 -- ...
17
18 -- * Type 'SPeano'
19 -- | Singleton for 'Zero' and 'Succ'.
20 data SPeano p where
21 SZero :: SPeano Zero
22 SSucc :: SPeano p -> SPeano (Succ p)
23 instance TestEquality SPeano where
24 testEquality SZero SZero = Just Refl
25 testEquality (SSucc x) (SSucc y)
26 | Just Refl <- testEquality x y
27 = Just Refl
28 testEquality _ _ = Nothing
29
30 -- * Type 'IPeano'
31 -- | Implicit construction of 'SPeano'.
32 class IPeano p where
33 ipeano :: SPeano p
34 instance IPeano Zero where
35 ipeano = SZero
36 instance IPeano p => IPeano (Succ p) where
37 ipeano = SSucc ipeano
38
39 -- * Type 'EPeano'
40 data EPeano where
41 EPeano :: SPeano p -> EPeano
42 instance Eq EPeano where
43 EPeano x == EPeano y =
44 case testEquality x y of
45 Just _ -> True
46 _ -> False
47 instance Show EPeano where
48 show (EPeano x) = show (integral_from_peano x::Integer)
49
50 -- * Interface with 'Integral'
51 integral_from_peano :: Integral i => SPeano p -> i
52 integral_from_peano SZero = 0
53 integral_from_peano (SSucc x) = 1 + integral_from_peano x
54
55 peano_from_integral :: Integral i => i -> (forall p. SPeano p -> ret) -> ret
56 peano_from_integral 0 k = k SZero
57 peano_from_integral i k | i > 0 =
58 peano_from_integral (i - 1) $ \p -> k (SSucc p)
59 peano_from_integral _ _ = error "peano_from_integral"
60
61 {-
62 -- | /Type-level natural number/, inductively defined.
63 data Nat
64 = Z
65 | S Nat
66
67 data SNat n where
68 SNatZ :: SNat 'Z
69 SNatS :: SNat n -> SNat ('S n)
70 instance Show (SNat n) where
71 showsPrec _p = showsPrec 10 . intNat
72
73 intNat :: SNat n -> Int
74 intNat = go 0
75 where
76 go :: Int -> SNat n -> Int
77 go i SNatZ = i
78 go i (SNatS n) = go (1 + i) n
79
80 type family (+) (a::Nat) (b::Nat) :: Nat where
81 'Z + b = b
82 'S a + b = 'S (a + b)
83 -}