naturals

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

IsSpeano.hs (3416B)

      1 module Naturals.IsSpeano (
      2     SpeanoSig (..),
      3     IsSpeano (..),
      4     pattern Zero,
      5     pattern Succ,
      6     pattern Speano0,
      7     pattern Speano1,
      8     pattern Speano2,
      9     pattern Speano3,
     10     pattern Speano4,
     11     pattern Speano5,
     12     pattern Speano6,
     13     pattern Speano7,
     14     pattern Speano8,
     15     pattern Speano9,
     16     speanoShow,
     17     speano,
     18     speanoInd,
     19     speanoRec,
     20     speanoFold,
     21     speanoPred,
     22 ) where
     23 
     24 import Data.Coerce
     25 import Data.Functor.Const
     26 
     27 import Naturals.Natural
     28 import Naturals.Peano
     29 
     30 -- | The signature of singleton (@Peano@-indexed) natural numbers.
     31 data SpeanoSig f n where
     32     ZeroOp :: SpeanoSig f Z
     33     SuccOp :: f n -> SpeanoSig f (S n)
     34 
     35 -- | Types that behave like singleton (@Peano@-indexed) natural numbers.
     36 --
     37 -- Laws:
     38 --   - @speanoPeel speanoZero = ZeroOp@
     39 --   - @speanoPeel (speanoSucc n) = SuccOp n@
     40 --   - @toNatural speanoZero = 0@
     41 --   - @toNatural (speanoSucc n) = succ (toNatural n)@
     42 class (forall n. ToNatural (f n)) => IsSpeano f where
     43     {-# MINIMAL speanoZero, speanoSucc, speanoPeel #-}
     44 
     45     speanoZero :: f Z
     46     speanoSucc :: f n -> f (S n)
     47 
     48     -- | Peel off the outermost operation (@ZeroOp@ or @SuccOp@) from the
     49     -- argument, obtaining a result suitable for shallow pattern matching.
     50     speanoPeel :: f n -> SpeanoSig f n
     51 
     52     speanoAdd :: (IsSpeano f) => f m -> f n -> f (Add m n)
     53     speanoAdd Zero n = n
     54     speanoAdd (Succ m) n = Succ (speanoAdd m n)
     55 
     56 pattern Zero :: (IsSpeano f) => (n ~ Z) => f n
     57 pattern Zero <- (speanoPeel -> ZeroOp) where Zero = speanoZero
     58 pattern Succ :: (IsSpeano f) => (n ~ S m) => f m -> f n
     59 pattern Succ p <- (speanoPeel -> SuccOp p) where Succ = speanoSucc
     60 {-# COMPLETE Zero, Succ #-}
     61 
     62 pattern Speano0 :: (IsSpeano f) => f Peano0
     63 pattern Speano0 = Zero
     64 
     65 pattern Speano1 :: (IsSpeano f) => f Peano1
     66 pattern Speano1 = Succ Speano0
     67 
     68 pattern Speano2 :: (IsSpeano f) => f Peano2
     69 pattern Speano2 = Succ Speano1
     70 
     71 pattern Speano3 :: (IsSpeano f) => f Peano3
     72 pattern Speano3 = Succ Speano2
     73 
     74 pattern Speano4 :: (IsSpeano f) => f Peano4
     75 pattern Speano4 = Succ Speano3
     76 
     77 pattern Speano5 :: (IsSpeano f) => f Peano5
     78 pattern Speano5 = Succ Speano4
     79 
     80 pattern Speano6 :: (IsSpeano f) => f Peano6
     81 pattern Speano6 = Succ Speano5
     82 
     83 pattern Speano7 :: (IsSpeano f) => f Peano7
     84 pattern Speano7 = Succ Speano6
     85 
     86 pattern Speano8 :: (IsSpeano f) => f Peano8
     87 pattern Speano8 = Succ Speano7
     88 
     89 pattern Speano9 :: (IsSpeano f) => f Peano9
     90 pattern Speano9 = Succ Speano8
     91 
     92 -- | Show with unary notation.
     93 speanoShow :: (IsSpeano f) => f n -> String
     94 speanoShow Zero = "Z"
     95 speanoShow (Succ n) = 'S' : speanoShow n
     96 
     97 -- | The (nonrecursive) eliminator for types implementing @IsSpeano@.
     98 speano :: (IsSpeano f) => ((n ~ Z) => a) -> (forall m. (n ~ S m) => f m -> a) -> f n -> a
     99 speano z _ Zero = z
    100 speano _ s (Succ m) = s m
    101 
    102 -- | Induction for types implementing @IsSpeano@.
    103 speanoInd :: forall f n p. (IsSpeano f) => p Z -> (forall m. f m -> p m -> p (S m)) -> f n -> p n
    104 speanoInd z _ Zero = z
    105 speanoInd z s (Succ m) = s m (speanoInd z s m)
    106 
    107 -- | The (nondependent) recursor for types implementing @IsSpeano@.
    108 speanoRec :: forall f n a. (IsSpeano f) => a -> (forall m. f m -> a -> a) -> f n -> a
    109 speanoRec = coerce $ speanoInd @f @n @(Const a)
    110 
    111 -- | The catamorphism for types implementing @IsSpeano@.
    112 speanoFold :: (IsSpeano f) => a -> (a -> a) -> f n -> a
    113 speanoFold z s = speanoRec z (const s)
    114 
    115 speanoPred :: (IsSpeano f) => f (S n) -> f n
    116 speanoPred (Succ m) = m