numericpeano-0.2.0.0: Peano numbers with attendant bells and whistles.

Numeric.Peano

Description

Value-level Peano arithmetic.

Synopsis

# Documentation

data Nat Source

Lazy Peano numbers. Allow calculation with infinite values.

Constructors

 Z Zero S Nat Successor

Instances

 Bounded Nat The lower bound is zero, the upper bound is infinity. Enum Nat The `pred` function is bounded at Zero. Eq Nat `==` and `/=` work as long as at least one operand is finite. Integral Nat Since negative numbers are not allowed, `quot = div` and `rem = mod`. The methods `quot`, `rem`, `div`, `mod`, `quotRem` and `divMod` will terminate as long as their first argument is finite. Infinities in their second arguments are permitted and are handled as follows: ``` n `quot` infinity = n `div` infinity = 0 n `rem` infinity = n `mod` infinity = n``` Num Nat Addition, multiplication, and subtraction are lazy in both arguments, meaning that, in the case of infinite values, they can produce an infinite stream of S-constructors. As long as the callers of these functions only consume a finite amount of these, the program will not hang. `fromInteger` is not injective in case of `Nat`, since negative integers are all converted to zero (`Z`). Ord Nat All methods work as long as at least one operand is finite. Real Nat Since `toRational` returns a `Ratio Integer`, it WILL NOT terminate on infinities. Show Nat Peano Nat

data Sign Source

Sign for whole numbers.

Constructors

 Pos Neg

Instances

 Bounded Sign Enum Sign Eq Sign Ord Sign Read Sign Show Sign

data Whole Source

Whole numbers (Z).

Constructors

 Whole Nat Sign Construct a whole number out of a magnitue and a sign.

Instances

 Bounded Whole The bounds are negative and positive infinity. Enum Whole `succ` and `pred` work according to the total order on the whole numbers, i.e. `succ n = n+1` and `pred n = n-1`. Eq Whole Positive and negative zero are considered equal. Num Whole Ord Whole The ordering is the standard total order on Z. Positive and negative zero are equal. Peano Whole

class Enum a => Peano a where Source

The class of Peano-like constructions (i.e. Nat and Whole).

Methods

isZero :: a -> Bool Source

Test for zero.

infinity :: a Source

An unobservable infinity. For all finite numbers `n`, `n < infinity` must hold, but there need not be a total function that tests whether a number is infinite.

fromPeano :: a -> Integer Source

Converts the number to an Integer.

decr :: a -> a Source

Reduces the absolute value of the number by 1. If `isZero n`, then `decr n = n` and vice versa.

Instances

 Peano Whole Peano Nat

isSucc :: Peano n => n -> Bool Source

Negation of `isZero`.

takeNat :: (Num a, Enum a, Ord a, Peano n) => a -> n -> (a, n) Source

Removes at most `S` constructors from a Peano number. Outputs the number of removed constructors and the remaining number.

natLength :: Foldable f => f a -> Nat Source

Returns the length of a foldable container as `Nat`. The number is generated lazily and thus, infinitely large containers are supported.