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

   1 {-# LANGUAGE GADTs #-}
   2 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
   3 -- | Natural numbers at the type-level, and of kind @*@.
   4 module Language.Symantic.Lib.Data.Type.Peano where
   5
   6 import Data.Type.Equality
   7
   8 -- * Types 'Zero' and 'Succ'
   9 data Zero
  10 data Succ p
  11
  12 -- ** Type synonyms for a few numbers
  13 type P0 = Zero
  14 type P1 = Succ P0
  15 type P2 = Succ P1
  16 type P3 = Succ P2
  17 -- ...
  18
  19 -- * Type 'SPeano'
  20 -- | Singleton for 'Zero' and 'Succ'.
  21 data SPeano p where
  22  SZero :: SPeano Zero
  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
  28          = Just Refl
  29         testEquality _ _ = Nothing
  30
  31 -- * Type 'IPeano'
  32 -- | Implicit construction of 'SPeano'.
  33 class IPeano p where
  34         ipeano :: SPeano p
  35 instance IPeano Zero where
  36         ipeano = SZero
  37 instance IPeano p => IPeano (Succ p) where
  38         ipeano = SSucc ipeano
  39
  40 -- * Type 'EPeano'
  41 data EPeano where
  42         EPeano :: SPeano p -> EPeano
  43 instance Eq EPeano where
  44         EPeano x == EPeano y =
  45                 case testEquality x y of
  46                  Just _ -> True
  47                  _ -> False
  48 instance Show EPeano where
  49         show (EPeano x) = show (integral_from_peano x::Integer)
  50
  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
  55
  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"