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