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