lean-peano-1.0.1.0: A maximally lazy, simple implementation of the Peano numbers with minimal dependencies

Safe HaskellSafe
LanguageHaskell2010

Numeric.Peano

Description

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
Synopsis

Documentation

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

data Nat Source #

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 Source #

The maximum bound here is infinity.

maxBound > (n :: Nat)
Instance details

Defined in Numeric.Peano

Methods

minBound :: Nat #

maxBound :: Nat #

Enum Nat Source #

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]
Instance details

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 Source # 
Instance details

Defined in Numeric.Peano

Methods

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

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

Integral Nat Source #

Errors on zero.

>>> 5 `div` 2
2
Instance details

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 Source # 
Instance details

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 Source #

Subtraction stops at zero.

n >= m ==> m - n == Z
Instance details

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 Source #

As lazy as possible

Instance details

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 Source #

Reads the integer representation.

Instance details

Defined in Numeric.Peano

Real Nat Source # 
Instance details

Defined in Numeric.Peano

Methods

toRational :: Nat -> Rational #

Show Nat Source #

Shows integer representation.

Instance details

Defined in Numeric.Peano

Methods

showsPrec :: Int -> Nat -> ShowS #

show :: Nat -> String #

showList :: [Nat] -> ShowS #

Ix Nat Source # 
Instance details

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 Source # 
Instance details

Defined in Numeric.Peano

Associated Types

type Rep Nat :: Type -> Type #

Methods

from :: Nat -> Rep Nat x #

to :: Rep Nat x -> Nat #

NFData Nat Source #

Will obviously diverge for values like maxBound.

Instance details

Defined in Numeric.Peano

Methods

rnf :: Nat -> () #

type Rep Nat Source # 
Instance details

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 Source #

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 Source #

A strict left fold over the naturals.