]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/Data/Peano.hs
init
[haskell/symantic.git] / Language / Symantic / Lib / Data / Peano.hs
1 {-# LANGUAGE GADTs #-}
2 {-# LANGUAGE Rank2Types #-}
3 {-# LANGUAGE TypeOperators #-}
4 -- | Type variable.
5 module Language.Symantic.Lib.Data.Peano where
6
7 import Data.Type.Equality ((:~:)(Refl))
8
9 -- * Types 'Zero' and 'Succ'
10 -- | Type-level peano numbers of kind '*'.
11 data Zero
12 data Succ p
13
14 -- * Type 'SPeano'
15 -- | Singleton for peano numbers.
16 data SPeano p where
17 SZero :: SPeano Zero
18 SSucc :: SPeano p -> SPeano (Succ p)
19
20 integral_from_peano :: Integral i => SPeano p -> i
21 integral_from_peano SZero = 0
22 integral_from_peano (SSucc x) = 1 + integral_from_peano x
23
24 peano_from_integral :: Integral i => i -> (forall p. SPeano p -> ret) -> ret
25 peano_from_integral 0 k = k SZero
26 peano_from_integral i k | i > 0 =
27 peano_from_integral (i - 1) $ \p -> k (SSucc p)
28 peano_from_integral _ _ = error "peano_from_integral"
29
30 peano_eq :: forall x y. SPeano x -> SPeano y -> Maybe (x :~: y)
31 peano_eq SZero SZero = Just Refl
32 peano_eq (SSucc x) (SSucc y)
33 | Just Refl <- x `peano_eq` y
34 = Just Refl
35 peano_eq _ _ = Nothing