naturals

natural numbers in Haskell
git clone git://git.rr3.xyz/naturals
Log | Files | Refs

Prim.hs (1306B)

      1 module Naturals.Snat.Prim (
      2     Snat,
      3     pattern Zero,
      4     pattern Succ,
      5     snat,
      6     snatInd,
      7     snatRec,
      8     snatFold,
      9     snatPred,
     10     snatAdd,
     11 ) where
     12 
     13 import Data.Coerce
     14 import Data.Functor.Const
     15 
     16 import Naturals.Peano
     17 import Naturals.Snat.Unsafe (Snat, snatAdd, snatPeel, snatSucc, snatZero)
     18 import Naturals.Speano hiding (Succ, Zero)
     19 
     20 pattern Zero :: () => (n ~ Z) => Snat n
     21 pattern Zero <- (snatPeel -> ZeroOp) where Zero = snatZero
     22 pattern Succ :: () => (n ~ S m) => Snat m -> Snat n
     23 pattern Succ p <- (snatPeel -> SuccOp p) where Succ = snatSucc
     24 {-# COMPLETE Zero, Succ #-}
     25 
     26 -- | The (nonrecursive) eliminator for @Snat@ (equivalent to a case expression
     27 -- with @Zero@ and @Succ@).
     28 snat :: ((n ~ Z) => a) -> (forall m. (n ~ S m) => Snat m -> a) -> Snat n -> a
     29 snat z _ Zero = z
     30 snat _ s (Succ m) = s m
     31 
     32 -- | Induction for @Snat@.
     33 snatInd :: f Z -> (forall m. Snat m -> f m -> f (S m)) -> Snat n -> f n
     34 snatInd z _ Zero = z
     35 snatInd z s (Succ m) = s m (snatInd z s m)
     36 
     37 -- | The (nondependent) recursor for @Snat@.
     38 snatRec :: forall a n. a -> (forall m. Snat m -> a -> a) -> Snat n -> a
     39 snatRec = coerce $ snatInd @(Const a) @n
     40 
     41 -- | The catamorphism for @Snat@.
     42 snatFold :: a -> (a -> a) -> Snat n -> a
     43 snatFold z s = snatRec z (const s)
     44 
     45 snatPred :: Snat (S n) -> Snat n
     46 snatPred (Succ n) = n