symantic/Language/Symantic/Typing/Peano.hs

   1 {-# LANGUAGE GADTs #-}
   2 -- | Natural numbers inductivey defined at the type-level, and of kind @*@.
   3 module Language.Symantic.Typing.Peano where
   4
   5 import Data.Type.Equality
   6
   7 -- * Types 'Zero' and 'Succ'
   8 data Zero
   9 data Succ p
  10
  11 -- ** Type synonyms for a few numbers
  12 type P0 = Zero
  13 type P1 = Succ P0
  14 type P2 = Succ P1
  15 type P3 = Succ P2
  16 -- ...
  17
  18 -- * Type 'SPeano'
  19 -- | Singleton for 'Zero' and 'Succ'.
  20 data SPeano p where
  21  SZero :: SPeano Zero
  22  SSucc :: SPeano p -> SPeano (Succ p)
  23 instance TestEquality SPeano where
  24         testEquality SZero SZero = Just Refl
  25         testEquality (SSucc x) (SSucc y)
  26          | Just Refl <- testEquality x y
  27          = Just Refl
  28         testEquality _ _ = Nothing
  29
  30 -- * Type 'IPeano'
  31 -- | Implicit construction of 'SPeano'.
  32 class IPeano p where
  33         ipeano :: SPeano p
  34 instance IPeano Zero where
  35         ipeano = SZero
  36 instance IPeano p => IPeano (Succ p) where
  37         ipeano = SSucc ipeano
  38
  39 -- * Type 'EPeano'
  40 data EPeano where
  41         EPeano :: SPeano p -> EPeano
  42 instance Eq EPeano where
  43         EPeano x == EPeano y =
  44                 case testEquality x y of
  45                  Just _ -> True
  46                  _ -> False
  47 instance Show EPeano where
  48         show (EPeano x) = show (integral_from_peano x::Integer)
  49
  50 -- * Interface with 'Integral'
  51 integral_from_peano :: Integral i => SPeano p -> i
  52 integral_from_peano SZero = 0
  53 integral_from_peano (SSucc x) = 1 + integral_from_peano x
  54
  55 peano_from_integral :: Integral i => i -> (forall p. SPeano p -> ret) -> ret
  56 peano_from_integral 0 k = k SZero
  57 peano_from_integral i k | i > 0 =
  58         peano_from_integral (i - 1) $ \p -> k (SSucc p)
  59 peano_from_integral _ _ = error "peano_from_integral"
  60
  61 {-
  62 -- | /Type-level natural number/, inductively defined.
  63 data Nat
  64  =   Z
  65  |   S Nat
  66
  67 data SNat n where
  68         SNatZ :: SNat 'Z
  69         SNatS :: SNat n -> SNat ('S n)
  70 instance Show (SNat n) where
  71         showsPrec _p = showsPrec 10 . intNat
  72
  73 intNat :: SNat n -> Int
  74 intNat = go 0
  75         where
  76         go :: Int -> SNat n -> Int
  77         go i SNatZ     = i
  78         go i (SNatS n) = go (1 + i) n
  79
  80 type family (+) (a::Nat) (b::Nat) :: Nat where
  81         'Z   + b = b
  82         'S a + b = 'S (a + b)
  83 -}