Numeric.Peano

Value-level Peano arithmetic.

Documentation

data Nat

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

Sign for whole numbers.

Constructors

Pos

Neg

Instances

Bounded Sign

Enum Sign

Eq Sign

Ord Sign

Read Sign

Show Sign

data Whole

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

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

Methods

isZero :: a -> Bool

Test for zero.

infinity :: a

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

Converts the number to an Integer.

decr :: a -> a

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

Negation of isZero.

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

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

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