naturals

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

Prim.hs (1502B)

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