Language/LOL/Symantic/Lib/Data/Peano.hs

   1 {-# LANGUAGE GADTs #-}
   2 {-# LANGUAGE Rank2Types #-}
   3 {-# LANGUAGE TypeOperators #-}
   4 -- | Type variable.
   5 module Language.LOL.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