naturals

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

Prim.hs (1691B)

      1 module Naturals.Peano.Prim (
      2     Peano (..),
      3     peanoShow,
      4     peano,
      5     peanoRec,
      6     peanoFold,
      7     Add,
      8 ) where
      9 
     10 import Control.Exception
     11 
     12 import Naturals.Natural
     13 
     14 -- | Unary natural numbers.
     15 -- Intended mainly for use at the type-level via DataKinds.
     16 data Peano = Z | S Peano deriving (Eq)
     17 
     18 instance Show Peano where
     19     show = show . toNatural
     20 
     21 -- | A variant of @show \@Peano@ that uses unary notation instead of decimal.
     22 peanoShow :: Peano -> String
     23 peanoShow Z = "Z"
     24 peanoShow (S n) = 'S' : peanoShow n
     25 
     26 instance Ord Peano where
     27     Z `compare` Z = EQ
     28     S _ `compare` Z = GT
     29     Z `compare` S _ = LT
     30     S m `compare` S n = m `compare` n
     31 
     32 instance Num Peano where
     33     Z + n = n
     34     S m + n = S (m + n)
     35 
     36     n - Z = n
     37     _ - S _ = throw Underflow
     38 
     39     Z * _ = Z
     40     S m * n = m * n + n
     41 
     42     abs n = n
     43 
     44     signum Z = Z
     45     signum (S _) = S Z
     46 
     47     fromInteger 0 = Z
     48     fromInteger n
     49         | n > 0 = S (fromInteger (n - 1))
     50         | otherwise = throw Underflow
     51 
     52 instance ToNatural Peano where
     53     toNatural Z = 0
     54     toNatural (S n) = succ (toNatural n)
     55 
     56 instance FromNatural Peano where
     57     fromNatural 0 = Z
     58     fromNatural n = S (fromNatural (pred n))
     59 
     60 -- | The (nonrecursive) eliminator for @Peano@ (equivalent to a case expression).
     61 peano :: a -> (Peano -> a) -> Peano -> a
     62 peano z _ Z = z
     63 peano _ s (S m) = s m
     64 
     65 -- | The recursor for @Peano@.
     66 peanoRec :: a -> (Peano -> a -> a) -> Peano -> a
     67 peanoRec z _ Z = z
     68 peanoRec z s (S m) = s m (peanoRec z s m)
     69 
     70 -- | The catamorphism for @Peano@.
     71 peanoFold :: a -> (a -> a) -> Peano -> a
     72 peanoFold z s = peanoRec z (const s)
     73 
     74 type family Add (x :: Peano) (y :: Peano) :: Peano where
     75     Add Z n = n
     76     Add (S m) n = S (Add m n)