-- 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,
--   meaning that a number of magnitude n may consume O(n) bytes of memory.
@package numericpeano
@version 0.1.0.0

module Numeric.Peano

-- | Lazy Peano numbers. Allow calculation with infinite values.
data Nat
Z :: Nat
S :: Nat -> Nat

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

-- | Whole numbers (Z).
data Whole
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)

-- | Bounded-instance for <a>Nat</a>. The lower bound is zero, the upper
--   bound is infinity.

-- | Bounded-instance for <a>Nat</a>. The bounds are negative and positive
--   infinity.

-- | Enum-instance for <a>Nat</a>. The <a>pred</a> function is bounded at
--   Zero.

-- | Enum-instance for <a>Whole</a>. <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>.

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

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

-- | Eq-instance for <a>Whole</a>. Positive and negative zero are
--   considered equal.

-- | Ord-instance for <a>Nat</a>. All methods work as long as at least one
--   operand is finite.

-- | Returns the length of a list as Nat. Can handle infinite lists,
--   provided that a finite lower bound is checked.
natLength :: [a] -> Nat

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

-- | Integral-instance for <a>Nat</a>. Since negative numbers are not
--   allowed, <tt>quot = div</tt> and <tt>rem = mod</tt>. The methods
--   <tt>quot</tt>, <tt>rem</tt>, <tt>div</tt>, <tt>mod</tt>,
--   <tt>quotRem</tt> and <tt>divMod</tt> will return as long as their
--   first argument is finite. Infinities are handled as follows: <tt> n
--   <a>quot</a> infinity = n <a>div</a> infinity = 0 n <a>rem</a> infinity
--   = n <a>mod</a> infinity = n</tt>
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