Numeric.Peano

Documentation

data Nat

Lazy Peano numbers. Allow calculation with infinite values.

Constructors

Z

S Nat

Instances

Bounded Nat

Bounded-instance for Nat. The lower bound is zero, the upper bound is infinity.

Enum Nat

Enum-instance for Nat. The pred function is bounded at Zero.

Eq Nat

Eq-instance for Nat. == and /= work as long as at least one operand is finite.

Integral Nat

Integral-instance for Nat. Since negative numbers are not allowed, quot = div and rem = mod. The methods quot, rem, div, mod, quotRem and divMod will return as long as their first argument is finite. Infinities are handled as follows: n quot infinity = n div infinity = 0 n rem infinity = n mod infinity = n

Num Nat

Num-instance for 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 Z.

Ord Nat

Ord-instance for Nat. All methods work as long as at least one operand is finite.

Real Nat

Real-instance for 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

Instances

Bounded Whole

Bounded-instance for Nat. The bounds are negative and positive infinity.

Enum Whole

Enum-instance for 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

Eq-instance for Whole. Positive and negative zero are considered equal.

Num Whole

Ord Whole

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.

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.

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 :: [a] -> Nat

Returns the length of a list as Nat. Can handle infinite lists, provided that a finite lower bound is checked.