naturals

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

Prim.hs (1998B)

      1 module Naturals.Speano.Prim (
      2     SpeanoSig (..),
      3     Speano (..),
      4     speanoShow,
      5     speano,
      6     speanoInd,
      7     speanoRec,
      8     speanoFold,
      9     speanoPred,
     10     speanoAdd,
     11 ) where
     12 
     13 import Data.Coerce
     14 import Data.Functor.Const
     15 
     16 import Naturals.Natural
     17 import Naturals.Peano
     18 
     19 -- | The "signature" of singleton (@Peano@-indexed) natural numbers:
     20 -- @SpeanoSig@ is to @Speano@ as @Maybe@ is to @Peano@.
     21 data SpeanoSig f n where
     22     ZeroOp :: SpeanoSig f Z
     23     SuccOp :: f n -> SpeanoSig f (S n)
     24 
     25 -- | Singleton (@Peano@-indexed) unary natural numbers.
     26 --
     27 -- @Speano@ is implemented as a GADT, and hence is inefficient.
     28 -- See @Snat@ and @Snatural@ for efficient alternatives.
     29 data Speano n where
     30     Zero :: Speano Z
     31     Succ :: Speano n -> Speano (S n)
     32 
     33 deriving instance Eq (Speano n)
     34 
     35 instance Show (Speano n) where
     36     show = show . toNatural
     37 
     38 -- | A variant of @show \@(Speano n)@ that uses unary notation instead of decimal.
     39 speanoShow :: Speano n -> String
     40 speanoShow Zero = "Z"
     41 speanoShow (Succ n) = 'S' : speanoShow n
     42 
     43 instance ToNatural (Speano n) where
     44     toNatural Zero = 0
     45     toNatural (Succ n) = succ (toNatural n)
     46 
     47 -- | The (nonrecursive) eliminator for @Speano@ (equivalent to a case
     48 -- expression).
     49 speano :: ((n ~ Z) => a) -> (forall m. (n ~ S m) => Speano m -> a) -> Speano n -> a
     50 speano z _ Zero = z
     51 speano _ s (Succ m) = s m
     52 
     53 -- | Induction for @Speano@.
     54 speanoInd :: f Z -> (forall m. Speano m -> f m -> f (S m)) -> Speano n -> f n
     55 speanoInd z _ Zero = z
     56 speanoInd z s (Succ m) = s m (speanoInd z s m)
     57 
     58 -- | The (nondependent) recursor for @Speano@.
     59 speanoRec :: forall a n. a -> (forall m. Speano m -> a -> a) -> Speano n -> a
     60 speanoRec = coerce $ speanoInd @(Const a) @n
     61 
     62 -- | The catamorphism for @Speano@.
     63 speanoFold :: a -> (a -> a) -> Speano n -> a
     64 speanoFold z s = speanoRec z (const s)
     65 
     66 speanoPred :: Speano (S n) -> Speano n
     67 speanoPred (Succ n) = n
     68 
     69 speanoAdd :: Speano m -> Speano n -> Speano (Add m n)
     70 speanoAdd Zero n = n
     71 speanoAdd (Succ m) n = Succ (speanoAdd m n)