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

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

Instances details
 Source # The maximum bound here is infinity.maxBound > (n :: Nat) Instance detailsDefined in Numeric.Peano Methods 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 detailsDefined in Numeric.Peano Methodssucc :: 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] # Source # Instance detailsDefined in Numeric.Peano Methods(==) :: Nat -> Nat -> Bool #(/=) :: Nat -> Nat -> Bool # Source # Errors on zero.>>> 5 div 2 2  Instance detailsDefined in Numeric.Peano Methodsquot :: 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) # Source # Instance detailsDefined in Numeric.Peano Methodsgfoldl :: (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 #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 :: forall r r'. (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 # Source # Subtraction stops at zero.n >= m ==> m - n == Z Instance detailsDefined in Numeric.Peano Methods(+) :: Nat -> Nat -> Nat #(-) :: Nat -> Nat -> Nat #(*) :: Nat -> Nat -> Nat #negate :: Nat -> Nat #abs :: Nat -> Nat #signum :: Nat -> Nat # Source # As lazy as possible Instance detailsDefined in Numeric.Peano Methodscompare :: Nat -> Nat -> Ordering #(<) :: Nat -> Nat -> Bool #(<=) :: Nat -> Nat -> Bool #(>) :: Nat -> Nat -> Bool #(>=) :: Nat -> Nat -> Bool #max :: Nat -> Nat -> Nat #min :: Nat -> Nat -> Nat # Source # Reads the integer representation. Instance detailsDefined in Numeric.Peano Methods Source # Instance detailsDefined in Numeric.Peano Methods Source # Shows integer representation. Instance detailsDefined in Numeric.Peano MethodsshowsPrec :: Int -> Nat -> ShowS #show :: Nat -> String #showList :: [Nat] -> ShowS # Source # Instance detailsDefined in Numeric.Peano Methodsrange :: (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 # Source # Instance detailsDefined in Numeric.Peano Associated Typestype Rep Nat :: Type -> Type # Methodsfrom :: Nat -> Rep Nat x #to :: Rep Nat x -> Nat # Source # Will obviously diverge for values like maxBound. Instance detailsDefined in Numeric.Peano Methodsrnf :: Nat -> () # type Rep Nat Source # Instance detailsDefined in Numeric.Peano type Rep Nat = D1 ('MetaData "Nat" "Numeric.Peano" "lean-peano-1.0.2.0-inplace" '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.