symantic/Language/Symantic/Typing/Peano.hs

   1 {-# LANGUAGE GADTs #-}
   2 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
   3 -- | Natural numbers inductivey defined at the type-level, and of kind @*@.
   4 module Language.Symantic.Typing.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"
  61
  62 {-
  63 -- | /Type-level natural number/, inductively defined.
  64 data Nat
  65  =   Z
  66  |   S Nat
  67
  68 data SNat n where
  69         SNatZ :: SNat 'Z
  70         SNatS :: SNat n -> SNat ('S n)
  71 instance Show (SNat n) where
  72         showsPrec _p = showsPrec 10 . intNat
  73
  74 intNat :: SNat n -> Int
  75 intNat = go 0
  76         where
  77         go :: Int -> SNat n -> Int
  78         go i SNatZ     = i
  79         go i (SNatS n) = go (1 + i) n
  80
  81 type family (+) (a::Nat) (b::Nat) :: Nat where
  82         'Z   + b = b
  83         'S a + b = 'S (a + b)
  84 -}