Language/Symantic/Lib/Data/Peano.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE Rank2Types #-}
   4 {-# LANGUAGE TypeOperators #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
   7 -- | Natural numbers at the type-level, and of kind @*@.
   8 module Language.Symantic.Lib.Data.Peano where
   9
  10 import Data.Type.Equality
  11
  12 -- * Types 'Zero' and 'Succ'
  13 data Zero
  14 data Succ p
  15
  16 -- ** Type synonyms for a few numbers
  17 type P0 = Zero
  18 type P1 = Succ P0
  19 type P2 = Succ P1
  20 type P3 = Succ P2
  21 -- ...
  22
  23 -- * Type 'SPeano'
  24 -- | Singleton for 'Zero' and 'Succ'.
  25 data SPeano p where
  26  SZero :: SPeano Zero
  27  SSucc :: SPeano p -> SPeano (Succ p)
  28 instance TestEquality SPeano where
  29         testEquality SZero SZero = Just Refl
  30         testEquality (SSucc x) (SSucc y)
  31          | Just Refl <- testEquality x y
  32          = Just Refl
  33         testEquality _ _ = Nothing
  34
  35 -- * Type 'IPeano'
  36 -- | Implicit construction of 'SPeano'.
  37 class IPeano p where
  38         ipeano :: SPeano p
  39 instance IPeano Zero where
  40         ipeano = SZero
  41 instance IPeano p => IPeano (Succ p) where
  42         ipeano = SSucc ipeano
  43
  44 -- * Type 'EPeano'
  45 data EPeano where
  46         EPeano :: SPeano p -> EPeano
  47 instance Eq EPeano where
  48         EPeano x == EPeano y =
  49                 case testEquality x y of
  50                  Just _ -> True
  51                  _ -> False
  52 instance Show EPeano where
  53         show (EPeano x) = show (integral_from_peano x::Integer)
  54
  55 -- * Interface with 'Integral'
  56 integral_from_peano :: Integral i => SPeano p -> i
  57 integral_from_peano SZero = 0
  58 integral_from_peano (SSucc x) = 1 + integral_from_peano x
  59
  60 peano_from_integral :: Integral i => i -> (forall p. SPeano p -> ret) -> ret
  61 peano_from_integral 0 k = k SZero
  62 peano_from_integral i k | i > 0 =
  63         peano_from_integral (i - 1) $ \p -> k (SSucc p)
  64 peano_from_integral _ _ = error "peano_from_integral"