TypeLevel.Nat

Type-level Peano arithmetic.

Documentation

>>> import Test.QuickCheck
>>> :{
instance Arbitrary Nat where
    arbitrary = fmap (fromInteger . getNonNegative) arbitrary
:}

data Nat

Peano numbers. Care is taken to make operations as lazy as possible:

>>> 1 > S (S undefined)
False
>>> Z > undefined
False
>>> 3 + (undefined :: Nat) >= 3
True

Constructors

Z

S Nat

Instances

Bounded Nat

The maximum bound here is infinity.

(maxBound :: Nat) > n

Methods

minBound :: Nat

maxBound :: Nat

Enum Nat

Uses custom enumFrom, enumFromThen, enumFromThenTo to avoid expensive conversions to and from Int.

>>> [1..3] :: [Nat]
[1,2,3]
>>> [1..1] :: [Nat]
[1]
>>> [2..1] :: [Nat]
[]
>>> take 3 [1,2..] :: [Nat]
[1,2,3]
>>> take 3 [5,4..] :: [Nat]
[5,4,3]
>>> [1,3..7] :: [Nat]
[1,3,5,7]
>>> [5,4..1] :: [Nat]
[5,4,3,2,1]
>>> [5,3..1] :: [Nat]
[5,3,1]

Methods

succ :: Nat -> Nat

pred :: Nat -> Nat

toEnum :: Int -> Nat

fromEnum :: Nat -> Int

enumFrom :: Nat -> [Nat]

enumFromThen :: Nat -> Nat -> [Nat]

enumFromTo :: Nat -> Nat -> [Nat]

enumFromThenTo :: Nat -> Nat -> Nat -> [Nat]

Eq Nat

Methods

(==) :: Nat -> Nat -> Bool

(/=) :: Nat -> Nat -> Bool

Integral Nat

Not at all optimized.

>>> 5 `div` 2 :: Nat
2

Methods

quot :: Nat -> Nat -> Nat

rem :: Nat -> Nat -> Nat

div :: Nat -> Nat -> Nat

mod :: Nat -> Nat -> Nat

quotRem :: Nat -> Nat -> (Nat, Nat)

divMod :: Nat -> Nat -> (Nat, Nat)

toInteger :: Nat -> Integer

Data Nat

Methods

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

toConstr :: Nat -> Constr

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 :: (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

Subtraction stops at zero.

n >= m ==> m - n == Z

Methods

(+) :: Nat -> Nat -> Nat

(-) :: Nat -> Nat -> Nat

(*) :: Nat -> Nat -> Nat

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat

Ord Nat

As lazy as possible

Methods

compare :: Nat -> Nat -> Ordering

(<) :: Nat -> Nat -> Bool

(<=) :: Nat -> Nat -> Bool

(>) :: Nat -> Nat -> Bool

(>=) :: Nat -> Nat -> Bool

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

Read Nat

Reads the integer representation.

Methods

readsPrec :: Int -> ReadS Nat

readList :: ReadS [Nat]

readPrec :: ReadPrec Nat

readListPrec :: ReadPrec [Nat]

Real Nat

Reasonably expensive.

Methods

toRational :: Nat -> Rational

Show Nat

Shows integer representation.

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

Generic Nat

Associated Types

type Rep Nat :: * -> *

Methods

from :: Nat -> Rep Nat x

to :: Rep Nat x -> Nat

NFData Nat

Will obviously diverge for values like maxBound.

Methods

rnf :: Nat -> ()

type Rep Nat

type Rep Nat = D1 (MetaData "Nat" "TypeLevel.Nat" "type-indexed-queues-0.1.0.0-673DidVnYBH7pHDFM1KZLj" False) ((:+:) (C1 (MetaCons "Z" PrefixI False) U1) (C1 (MetaCons "S" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Nat))))

data The Nat

Singleton for type-level Peano numbers.

data The Nat where

• Zy :: The Nat Z
• Sy :: The Nat (S n)

type family (n :: Nat) + (m :: Nat) :: Nat where ... infixl 6

Add two type-level numbers.

Equations

Z + m = m

(S n) + m = S (n + m)