type-indexed-queues-0.1.0.1: Queues with verified and unverified versions.

Safe HaskellNone
LanguageHaskell2010

TypeLevel.Nat

Description

Type-level Peano arithmetic.

Synopsis

Documentation

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

data Nat Source #

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 Source #

The maximum bound here is infinity.

(maxBound :: Nat) > n

Methods

minBound :: Nat #

maxBound :: Nat #

Enum Nat Source #

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 Source # 

Methods

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

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

Integral Nat Source #

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 Source # 

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 Source #

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 Source #

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 Source #

Reads the integer representation.

Real Nat Source #

Reasonably expensive.

Methods

toRational :: Nat -> Rational #

Show Nat Source #

Shows integer representation.

Methods

showsPrec :: Int -> Nat -> ShowS #

show :: Nat -> String #

showList :: [Nat] -> ShowS #

Generic Nat Source # 

Associated Types

type Rep Nat :: * -> * #

Methods

from :: Nat -> Rep Nat x #

to :: Rep Nat x -> Nat #

NFData Nat Source #

Will obviously diverge for values like maxBound.

Methods

rnf :: Nat -> () #

type Rep Nat Source # 
type Rep Nat = D1 (MetaData "Nat" "TypeLevel.Nat" "type-indexed-queues-0.1.0.1-GPaLldpmb1Q20PpM0x8M72" False) ((:+:) (C1 (MetaCons "Z" PrefixI False) U1) (C1 (MetaCons "S" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Nat))))
data The Nat Source #

Singleton for type-level Peano numbers.

data The Nat where

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

Add two type-level numbers.

Equations

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