-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Peano numbers with attendant bells and whistles.
--   
--   Value-level lazy Peano numbers for all your proof-theoretic and
--   infinity-related needs. The features are: 1) natural and integral
--   numbers (N and Z); 2) lazy infinities; and 3) instances for all
--   relevant typeclasses, meaning that Peano arithmetic can be used in
--   generic functions without extra hassle. The implementation is naive: a
--   number of magnitude n may consume O(n) bytes of memory.
@package numericpeano
@version 0.2.0.0


-- | Value-level Peano arithmetic.
module Numeric.Peano

-- | Lazy Peano numbers. Allow calculation with infinite values.
data Nat

-- | Zero
Z :: Nat

-- | Successor
S :: Nat -> Nat

-- | Sign for whole numbers.
data Sign
Pos :: Sign
Neg :: Sign

-- | Whole numbers (Z).
data Whole

-- | Construct a whole number out of a magnitue and a sign.
Whole :: Nat -> Sign -> Whole

-- | The class of Peano-like constructions (i.e. Nat and Whole).
class Enum a => Peano a
isZero :: Peano a => a -> Bool
infinity :: Peano a => a
fromPeano :: Peano a => a -> Integer
decr :: Peano a => a -> a

-- | Negation of <a>isZero</a>.
isSucc :: Peano n => n -> Bool

-- | Removes at most <a>S</a> constructors from a Peano number. Outputs the
--   number of removed constructors and the remaining number.
takeNat :: (Num a, Enum a, Ord a, Peano n) => a -> n -> (a, n)

-- | The lower bound is zero, the upper bound is infinity.

-- | The bounds are negative and positive infinity.

-- | The <a>pred</a> function is bounded at Zero.

-- | <a>succ</a> and <a>pred</a> work according to the total order on the
--   whole numbers, i.e. <tt>succ n = n+1</tt> and <tt>pred n = n-1</tt>.

-- | 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.
--   
--   <tt>fromInteger</tt> is not injective in case of <a>Nat</a>, since
--   negative integers are all converted to zero (<a>Z</a>).

-- | <a>==</a> and <a>/=</a> work as long as at least one operand is
--   finite.

-- | Positive and negative zero are considered equal.

-- | All methods work as long as at least one operand is finite.

-- | The ordering is the standard total order on Z. Positive and negative
--   zero are equal.

-- | Returns the length of a foldable container as <a>Nat</a>. The number
--   is generated lazily and thus, infinitely large containers are
--   supported.
natLength :: Foldable f => f a -> Nat

-- | Since <a>toRational</a> returns a <tt>Ratio Integer</tt>, it WILL NOT
--   terminate on infinities.

-- | Since negative numbers are not allowed, <tt><a>quot</a> =
--   <a>div</a></tt> and <tt><a>rem</a> = <a>mod</a></tt>. The methods
--   <a>quot</a>, <a>rem</a>, <a>div</a>, <a>mod</a>, <a>quotRem</a> and
--   <a>divMod</a> will terminate as long as their first argument is
--   finite. Infinities in their second arguments are permitted and are
--   handled as follows:
--   
--   <pre>
--   
--   n <a>quot</a> infinity   =   n <a>div</a> infinity   =   0
--   n <a>rem</a>  infinity   =   n <a>mod</a> infinity   =   n
--   </pre>
instance Show Nat
instance Show Sign
instance Eq Sign
instance Ord Sign
instance Enum Sign
instance Read Sign
instance Bounded Sign
instance Integral Nat
instance Real Nat
instance Ord Whole
instance Ord Nat
instance Eq Whole
instance Eq Nat
instance Num Whole
instance Num Nat
instance Enum Whole
instance Enum Nat
instance Bounded Whole
instance Bounded Nat
instance Peano Whole
instance Peano Nat