Safe Haskell  Safe 

Language  Haskell2010 
Peano numerals. Effort is made to make them as efficient as possible, and as lazy as possible, but they are many orders of magnitude less efficient than machine integers. They are primarily used for typelevel programming, and occasionally for calculations which can be shortcircuited.
For instance, to check if two lists are the same length, you could write:
length
xs ==length
ys
But this unnecessarily traverses both lists. The more efficient version, on the other hand, is less clear:
sameLength [] [] = True sameLength (_:xs) (_:ys) = sameLength xs ys sameLength _ _ = False
Using
, on the other hand, the laziness of
genericLength
will indeed shortcircuit:Nat
>>>
genericLength [1,2,3] == genericLength [1..]
False
Documentation
>>>
import Test.QuickCheck
>>>
import Data.List (genericLength)
>>>
default (Nat)
>>>
:{
instance Arbitrary Nat where arbitrary = fmap (fromInteger . getNonNegative) arbitrary :}
Peano numbers. Care is taken to make operations as lazy as possible:
>>>
1 > S (S undefined)
False>>>
Z > undefined
False>>>
3 + undefined >= 3
True
Instances
Bounded Nat Source #  The maximum bound here is infinity. maxBound > (n :: Nat) 
Enum Nat Source #  Uses custom

Eq Nat Source #  
Integral Nat Source #  Errors on zero.

Data Nat Source #  
Defined in Numeric.Peano gfoldl :: (forall d b. Data d => c (d > b) > d > c b) > (forall g. g > c g) > Nat > c Nat # gunfold :: (forall b r. Data b => c (b > r) > c r) > (forall r. r > c r) > Constr > c Nat # dataTypeOf :: Nat > DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) > Maybe (c Nat) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) > Maybe (c Nat) # gmapT :: (forall b. Data b => b > b) > Nat > Nat # gmapQl :: (r > r' > r) > r > (forall d. Data d => d > r') > Nat > r # gmapQr :: forall r r'. (r' > r > r) > r > (forall d. Data d => d > r') > Nat > r # gmapQ :: (forall d. Data d => d > u) > Nat > [u] # gmapQi :: Int > (forall d. Data d => d > u) > Nat > u # gmapM :: Monad m => (forall d. Data d => d > m d) > Nat > m Nat # gmapMp :: MonadPlus m => (forall d. Data d => d > m d) > Nat > m Nat # gmapMo :: MonadPlus m => (forall d. Data d => d > m d) > Nat > m Nat #  
Num Nat Source #  Subtraction stops at zero. n >= m ==> m  n == Z 
Ord Nat Source #  As lazy as possible 
Read Nat Source #  Reads the integer representation. 
Real Nat Source #  
Defined in Numeric.Peano toRational :: Nat > Rational #  
Show Nat Source #  Shows integer representation. 
Ix Nat Source #  
Generic Nat Source #  
NFData Nat Source #  Will obviously diverge for values like 
Defined in Numeric.Peano  
type Rep Nat Source #  
Defined in Numeric.Peano 