naturals

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

IsFin.hs (3668B)

      1 module Naturals.IsFin (
      2     FinSig (..),
      3     IsFin (..),
      4     pattern FZero,
      5     pattern FSucc,
      6     pattern Fin0,
      7     pattern Fin1,
      8     pattern Fin2,
      9     pattern Fin3,
     10     pattern Fin4,
     11     pattern Fin5,
     12     pattern Fin6,
     13     pattern Fin7,
     14     pattern Fin8,
     15     pattern Fin9,
     16     finFromSpeano,
     17     finShow,
     18     fin,
     19     finAbsurd,
     20     finRec,
     21     finFold,
     22     finMirror,
     23 ) where
     24 
     25 import Naturals.IsSpeano
     26 import Naturals.Natural
     27 import Naturals.Peano
     28 
     29 -- | The "signature" of finite (@Peano@-indexed) prefixes of the natural
     30 -- numbers.
     31 data FinSig f n where
     32     FZeroOp :: FinSig f (S n)
     33     FSuccOp :: f n -> FinSig f (S n)
     34 
     35 -- | Types that behave like finite (@Peano@-indexed) prefixes of the natural
     36 -- numbers.
     37 --
     38 -- Laws:
     39 --   - @finPeel finZero = FZeroOp@
     40 --   - @finPeel (finSucc n) = FSuccOp n@
     41 --   - @toNatural finZero = 0@
     42 --   - @toNatural (finSucc n) = succ (toNatural n)@
     43 class (forall n. ToNatural (f n)) => IsFin f where
     44     {-# MINIMAL finZero, finSucc, finPeel #-}
     45 
     46     finZero :: f (S n)
     47     finSucc :: f n -> f (S n)
     48 
     49     -- | Peel off the outermost operation (@FZeroOp@ or @FSuccOp@) from the
     50     -- argument, obtaining a result suitable for shallow pattern matching.
     51     finPeel :: f n -> FinSig f n
     52 
     53     finWeaken :: (IsFin f) => f n -> f (S n)
     54     finWeaken FZero = FZero
     55     finWeaken (FSucc n) = FSucc (finWeaken n)
     56 
     57 pattern FZero :: (IsFin f) => (n ~ S m) => f n
     58 pattern FZero <- (finPeel -> FZeroOp) where FZero = finZero
     59 pattern FSucc :: (IsFin f) => (n ~ S m) => f m -> f n
     60 pattern FSucc p <- (finPeel -> FSuccOp p) where FSucc = finSucc
     61 {-# COMPLETE FZero, FSucc #-}
     62 
     63 pattern Fin0 :: (IsFin f) => f (Add Peano0 (S n))
     64 pattern Fin0 = FZero
     65 
     66 pattern Fin1 :: (IsFin f) => f (Add Peano1 (S n))
     67 pattern Fin1 = FSucc Fin0
     68 
     69 pattern Fin2 :: (IsFin f) => f (Add Peano2 (S n))
     70 pattern Fin2 = FSucc Fin1
     71 
     72 pattern Fin3 :: (IsFin f) => f (Add Peano3 (S n))
     73 pattern Fin3 = FSucc Fin2
     74 
     75 pattern Fin4 :: (IsFin f) => f (Add Peano4 (S n))
     76 pattern Fin4 = FSucc Fin3
     77 
     78 pattern Fin5 :: (IsFin f) => f (Add Peano5 (S n))
     79 pattern Fin5 = FSucc Fin4
     80 
     81 pattern Fin6 :: (IsFin f) => f (Add Peano6 (S n))
     82 pattern Fin6 = FSucc Fin5
     83 
     84 pattern Fin7 :: (IsFin f) => f (Add Peano7 (S n))
     85 pattern Fin7 = FSucc Fin6
     86 
     87 pattern Fin8 :: (IsFin f) => f (Add Peano8 (S n))
     88 pattern Fin8 = FSucc Fin7
     89 
     90 pattern Fin9 :: (IsFin f) => f (Add Peano9 (S n))
     91 pattern Fin9 = FSucc Fin8
     92 
     93 finFromSpeano :: (IsSpeano s, IsFin f) => s n -> f (S n)
     94 finFromSpeano Zero = FZero
     95 finFromSpeano (Succ n) = FSucc (finFromSpeano n)
     96 
     97 -- | Show with unary notation.
     98 finShow :: (IsFin f) => f n -> String
     99 finShow FZero = "Z"
    100 finShow (FSucc n) = 'S' : finShow n
    101 
    102 -- | The (nonrecursive) eliminator for types implementing @IsFin@.
    103 fin :: (IsFin f) => (forall m. (n ~ S m) => a) -> (forall m. (n ~ S m) => f m -> a) -> f n -> a
    104 fin z _ FZero = z
    105 fin _ s (FSucc m) = s m
    106 
    107 finAbsurd :: (IsFin f) => f Z -> a
    108 finAbsurd = \case {}
    109 
    110 -- | The recursor for types implementing @IsFin@.
    111 finRec :: (IsFin f) => a -> (forall m. f m -> a -> a) -> f n -> a
    112 finRec z _ FZero = z
    113 finRec z s (FSucc m) = s m (finRec z s m)
    114 
    115 -- | The "catamorphism" for types implementing @IsFin@.
    116 finFold :: (IsFin f) => a -> (a -> a) -> f n -> a
    117 finFold z s = finRec z (const s)
    118 
    119 newtype FinMirror f n = FinMirror {unFinMirror :: f n -> f n}
    120 
    121 -- | Informally, @finMirror n i = n - i - 1@.
    122 finMirror :: forall s f n. (IsSpeano s, IsFin f) => s n -> f n -> f n
    123 finMirror =
    124     let z :: FinMirror f Z
    125         z = FinMirror finAbsurd
    126         s :: s m -> FinMirror f m -> FinMirror f (S m)
    127         s m (FinMirror f) = FinMirror \case
    128             FZero -> finFromSpeano m
    129             FSucc i -> finWeaken (f i)
    130     in unFinMirror . speanoInd z s