]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/Data/Peano.hs
Simplify the Constraint projection
[haskell/symantic.git] / Language / Symantic / Lib / Data / Peano.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE Rank2Types #-}
4 {-# LANGUAGE TypeOperators #-}
5 {-# LANGUAGE TypeFamilies #-}
6 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
7 -- | Natural numbers at the type-level, and of kind @*@.
8 module Language.Symantic.Lib.Data.Peano where
9
10 import Data.Type.Equality
11
12 -- * Types 'Zero' and 'Succ'
13 data Zero
14 data Succ p
15
16 -- ** Type synonyms for a few numbers
17 type P0 = Zero
18 type P1 = Succ P0
19 type P2 = Succ P1
20 type P3 = Succ P2
21 -- ...
22
23 -- * Type 'SPeano'
24 -- | Singleton for 'Zero' and 'Succ'.
25 data SPeano p where
26 SZero :: SPeano Zero
27 SSucc :: SPeano p -> SPeano (Succ p)
28 instance TestEquality SPeano where
29 testEquality SZero SZero = Just Refl
30 testEquality (SSucc x) (SSucc y)
31 | Just Refl <- testEquality x y
32 = Just Refl
33 testEquality _ _ = Nothing
34
35 -- * Type 'IPeano'
36 -- | Implicit construction of 'SPeano'.
37 class IPeano p where
38 ipeano :: SPeano p
39 instance IPeano Zero where
40 ipeano = SZero
41 instance IPeano p => IPeano (Succ p) where
42 ipeano = SSucc ipeano
43
44 -- * Type 'EPeano'
45 data EPeano where
46 EPeano :: SPeano p -> EPeano
47 instance Eq EPeano where
48 EPeano x == EPeano y =
49 case testEquality x y of
50 Just _ -> True
51 _ -> False
52 instance Show EPeano where
53 show (EPeano x) = show (integral_from_peano x::Integer)
54
55 -- * Interface with 'Integral'
56 integral_from_peano :: Integral i => SPeano p -> i
57 integral_from_peano SZero = 0
58 integral_from_peano (SSucc x) = 1 + integral_from_peano x
59
60 peano_from_integral :: Integral i => i -> (forall p. SPeano p -> ret) -> ret
61 peano_from_integral 0 k = k SZero
62 peano_from_integral i k | i > 0 =
63 peano_from_integral (i - 1) $ \p -> k (SSucc p)
64 peano_from_integral _ _ = error "peano_from_integral"