naturals

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

Fin.hs (743B)

      1 module Naturals.Fin (
      2     Fin (..),
      3 ) where
      4 
      5 import Naturals.IsFin hiding (FSucc, FZero)
      6 import Naturals.Natural
      7 import Naturals.Peano
      8 
      9 -- | Finite (@Peano@-indexed) prefixes of the unary natural numbers.
     10 --
     11 -- @Fin@ is implemented as a "correct-by-construction" GADT, making it
     12 -- inefficient. See @Finat@ and @Finatural@ for efficient alternatives.
     13 data Fin n where
     14     FZero :: Fin (S n)
     15     FSucc :: Fin n -> Fin (S n)
     16 
     17 deriving instance Eq (Fin n)
     18 
     19 instance Show (Fin n) where
     20     show = show . toNatural
     21 
     22 instance ToNatural (Fin n) where
     23     toNatural FZero = 0
     24     toNatural (FSucc n) = succ (toNatural n)
     25 
     26 instance IsFin Fin where
     27     finZero = FZero
     28 
     29     finSucc = FSucc
     30 
     31     finPeel FZero = FZeroOp
     32     finPeel (FSucc m) = FSuccOp m