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 ((:~:)(Refl))
  11
  12 -- * Types 'Zero' and 'Succ'
  13 -- | Type-level peano numbers of kind '*'.
  14 data Zero
  15 data Succ p
  16
  17 -- ** Type synonyms for a few numbers
  18 type P0 = Zero
  19 type P1 = Succ P0
  20 type P2 = Succ P1
  21 type P3 = Succ P2
  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
  29 -- * Type 'IPeano'
  30 -- | Implicit construction of 'SPeano'.
  31 class IPeano p where
  32         ipeano :: SPeano p
  33 instance IPeano Zero where
  34         ipeano = SZero
  35 instance IPeano p => IPeano (Succ p) where
  36         ipeano = SSucc ipeano
  37
  38 -- * Type 'EPeano'
  39 data EPeano where
  40         EPeano :: SPeano p -> EPeano
  41 instance Eq EPeano where
  42         EPeano x == EPeano y =
  43                 (integral_from_peano x::Integer) ==
  44                  integral_from_peano y
  45
  46 integral_from_peano :: Integral i => SPeano p -> i
  47 integral_from_peano SZero = 0
  48 integral_from_peano (SSucc x) = 1 + integral_from_peano x
  49
  50 peano_from_integral :: Integral i => i -> (forall p. SPeano p -> ret) -> ret
  51 peano_from_integral 0 k = k SZero
  52 peano_from_integral i k | i > 0 =
  53         peano_from_integral (i - 1) $ \p -> k (SSucc p)
  54 peano_from_integral _ _ = error "peano_from_integral"
  55
  56 peano_eq :: forall x y. SPeano x -> SPeano y -> Maybe (x :~: y)
  57 peano_eq SZero SZero = Just Refl
  58 peano_eq (SSucc x) (SSucc y)
  59  | Just Refl <- x `peano_eq` y
  60  = Just Refl
  61 peano_eq _ _ = Nothing
  62
  63 {-
  64 -- * Type family '<='
  65 type family n <= m :: Bool where
  66         Zero   <= m      = 'True
  67         n      <= Zero   = 'False
  68         Succ n <= Succ m = n <= m
  69
  70 -- * Type 'VList'
  71 -- | Vector list.
  72 data VList :: * -> * -> * where
  73         VNil  :: VList Zero a
  74         (:::) :: a -> VList p a -> VList (Succ p) a
  75 infixr 5 :::
  76 -}