]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/Data/Peano.hs
polish names
[haskell/symantic.git] / Language / Symantic / Lib / Data / Peano.hs
1 {-# LANGUAGE GADTs #-}
2 {-# LANGUAGE Rank2Types #-}
3 {-# LANGUAGE TypeOperators #-}
4 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
5 -- | Natural numbers at the type-level, and of kind @*@.
6 module Language.Symantic.Lib.Data.Peano where
7
8 import Data.Type.Equality ((:~:)(Refl))
9
10 -- * Types 'Zero' and 'Succ'
11 -- | Type-level peano numbers of kind '*'.
12 data Zero
13 data Succ p
14
15 -- * Type 'SPeano'
16 -- | Singleton for 'Zero' and 'Succ'.
17 data SPeano p where
18 SZero :: SPeano Zero
19 SSucc :: SPeano p -> SPeano (Succ p)
20
21 -- * Type 'IPeano'
22 -- | Implicit construction of 'SPeano'.
23 class IPeano p where
24 ipeano :: SPeano p
25 instance IPeano Zero where
26 ipeano = SZero
27 instance IPeano p => IPeano (Succ p) where
28 ipeano = SSucc ipeano
29
30 -- * Type 'EPeano'
31 data EPeano where
32 EPeano :: SPeano p -> EPeano
33 instance Eq EPeano where
34 EPeano x == EPeano y =
35 (integral_from_peano x::Integer) ==
36 integral_from_peano y
37
38 integral_from_peano :: Integral i => SPeano p -> i
39 integral_from_peano SZero = 0
40 integral_from_peano (SSucc x) = 1 + integral_from_peano x
41
42 peano_from_integral :: Integral i => i -> (forall p. SPeano p -> ret) -> ret
43 peano_from_integral 0 k = k SZero
44 peano_from_integral i k | i > 0 =
45 peano_from_integral (i - 1) $ \p -> k (SSucc p)
46 peano_from_integral _ _ = error "peano_from_integral"
47
48 peano_eq :: forall x y. SPeano x -> SPeano y -> Maybe (x :~: y)
49 peano_eq SZero SZero = Just Refl
50 peano_eq (SSucc x) (SSucc y)
51 | Just Refl <- x `peano_eq` y
52 = Just Refl
53 peano_eq _ _ = Nothing