2 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
3 -- | Natural numbers at the type-level, and of kind @*@.
4 module Language.Symantic.Helper.Data.Type.Peano where
6 import Data.Type.Equality
8 -- * Types 'Zero' and 'Succ'
12 -- ** Type synonyms for a few numbers
20 -- | Singleton for 'Zero' and 'Succ'.
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
29 testEquality _ _ = Nothing
32 -- | Implicit construction of 'SPeano'.
35 instance IPeano Zero where
37 instance IPeano p => IPeano (Succ p) where
42 EPeano :: SPeano p -> EPeano
43 instance Eq EPeano where
44 EPeano x == EPeano y =
45 case testEquality x y of
48 instance Show EPeano where
49 show (EPeano x) = show (integral_from_peano x::Integer)
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
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"