Numeric.Peano

Peano numerals. Effort is made to make them as efficient as possible, and as lazy as possible, but they are many orders of magnitude less efficient than machine integers. They are primarily used for type-level programming, and occasionally for calculations which can be short-circuited.

For instance, to check if two lists are the same length, you could write:

length xs == length ys

But this unnecessarily traverses both lists. The more efficient version, on the other hand, is less clear:

sameLength [] [] = True
sameLength (_:xs) (_:ys) = sameLength xs ys
sameLength _ _ = False

Using genericLength, on the other hand, the laziness of Nat will indeed short-circuit:

>>> genericLength [1,2,3] == genericLength [1..]
False

Documentation

>>> import Test.QuickCheck
>>> import Data.List (genericLength)
>>> default (Nat)
>>> :{
instance Arbitrary Nat where
    arbitrary = fmap (fromInteger . getNonNegative) arbitrary
:}

data Nat

Peano numbers. Care is taken to make operations as lazy as possible:

>>> 1 > S (S undefined)
False
>>> Z > undefined
False
>>> 3 + undefined >= 3
True

Constructors

Z

S Nat

Instances

Bounded Nat

The maximum bound here is infinity.

maxBound > (n :: Nat)

Defined in Numeric.Peano

Methods

minBound :: Nat

maxBound :: Nat

Enum Nat

Uses custom enumFrom, enumFromThen, enumFromThenTo to avoid expensive conversions to and from Int.

>>> [1..3]
[1,2,3]
>>> [1..1]
[1]
>>> [2..1]
[]
>>> take 3 [1,2..]
[1,2,3]
>>> take 3 [5,4..]
[5,4,3]
>>> [1,3..7]
[1,3,5,7]
>>> [5,4..1]
[5,4,3,2,1]
>>> [5,3..1]
[5,3,1]

Defined in Numeric.Peano

Methods

succ :: Nat -> Nat

pred :: Nat -> Nat

toEnum :: Int -> Nat

fromEnum :: Nat -> Int

enumFrom :: Nat -> [Nat]

enumFromThen :: Nat -> Nat -> [Nat]

enumFromTo :: Nat -> Nat -> [Nat]

enumFromThenTo :: Nat -> Nat -> Nat -> [Nat]

Eq Nat

Defined in Numeric.Peano

Methods

(==) :: Nat -> Nat -> Bool

(/=) :: Nat -> Nat -> Bool

Integral Nat

Errors on zero.

>>> 5 `div` 2
2

Defined in Numeric.Peano

Methods

quot :: Nat -> Nat -> Nat

rem :: Nat -> Nat -> Nat

div :: Nat -> Nat -> Nat

mod :: Nat -> Nat -> Nat

quotRem :: Nat -> Nat -> (Nat, Nat)

divMod :: Nat -> Nat -> (Nat, Nat)

toInteger :: Nat -> Integer

Data Nat

Defined in Numeric.Peano

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Nat -> c Nat

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Nat

toConstr :: Nat -> Constr

dataTypeOf :: Nat -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Nat)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)

gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r

gmapQ :: (forall d. Data d => d -> u) -> Nat -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Nat -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Nat -> m Nat

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat

Num Nat

Subtraction stops at zero.

n >= m ==> m - n == Z

Defined in Numeric.Peano

Methods

(+) :: Nat -> Nat -> Nat

(-) :: Nat -> Nat -> Nat

(*) :: Nat -> Nat -> Nat

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat

Ord Nat

As lazy as possible

Defined in Numeric.Peano

Methods

compare :: Nat -> Nat -> Ordering

(<) :: Nat -> Nat -> Bool

(<=) :: Nat -> Nat -> Bool

(>) :: Nat -> Nat -> Bool

(>=) :: Nat -> Nat -> Bool

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

Read Nat

Reads the integer representation.

Defined in Numeric.Peano

Methods

readsPrec :: Int -> ReadS Nat

readList :: ReadS [Nat]

readPrec :: ReadPrec Nat

readListPrec :: ReadPrec [Nat]

Real Nat

Defined in Numeric.Peano

Methods

toRational :: Nat -> Rational

Show Nat

Shows integer representation.

Defined in Numeric.Peano

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

Ix Nat

Defined in Numeric.Peano

Methods

range :: (Nat, Nat) -> [Nat]

index :: (Nat, Nat) -> Nat -> Int

unsafeIndex :: (Nat, Nat) -> Nat -> Int

inRange :: (Nat, Nat) -> Nat -> Bool

rangeSize :: (Nat, Nat) -> Int

unsafeRangeSize :: (Nat, Nat) -> Int

Generic Nat

Defined in Numeric.Peano

Associated Types

type Rep Nat :: Type -> Type

Methods

from :: Nat -> Rep Nat x

to :: Rep Nat x -> Nat

NFData Nat

Will obviously diverge for values like maxBound.

Defined in Numeric.Peano

Methods

rnf :: Nat -> ()

type Rep Nat

Defined in Numeric.Peano

type Rep Nat = D1 (MetaData "Nat" "Numeric.Peano" "lean-peano-1.0.1.0-A2gk0TDfF0Z76lWcx2EKyl" False) (C1 (MetaCons "Z" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "S" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Nat)))

foldrNat :: (a -> a) -> a -> Nat -> a

A right fold over the naturals. Alternatively, a function which converts a natural into a Church natural.

foldrNat S Z n === n

foldlNat' :: (a -> a) -> a -> Nat -> a

A strict left fold over the naturals.