Data.Numeric.Witness.Peano

This module defines GADT type witnesses for Peano-style natural numbers.

Documentation

data Zero

Instances

ReifyNatural Zero

data Succ n

Instances

ReifyNatural n => ReifyNatural (Succ n)

data Natural n where

Natural numbers paired with type-level natural numbers. These terms act as witnesses of a particular natural.

Constructors

Zero :: Natural Zero

Succ :: Natural n -> Natural (Succ n)

Instances

Show (Natural n)

class ReifyNatural n where

Given a context expecting a particular natural, we can manufacture it from the aether.

Methods

reifyNatural :: Natural n

Instances

ReifyNatural Zero

ReifyNatural n => ReifyNatural (Succ n)

type family LessThanOrEqual a b

Type level less-than-or-equal test.

Equations

LessThanOrEqual Zero Zero = True

LessThanOrEqual Zero (Succ m) = True

LessThanOrEqual (Succ n) (Succ m) = LessThanOrEqual n m

LessThanOrEqual x y = False

type (<=) a b = LessThanOrEqual a b ~ True

This constraint is a more succinct way of requiring that a be less than or equal to b.

type family LessThan a b

Type level less-than test.

Equations

LessThan Zero (Succ m) = True

LessThan (Succ n) (Succ m) = LessThan n m

LessThan x y = False

type (<) a b = LessThan a b ~ True

This constraint is a more succinct way of requiring that a be less than b.

type family x + y

Type level addition.

Equations

x + Zero = x

x + (Succ y) = Succ (x + y)

type family x - y

Type level subtraction.

Equations

x - Zero = x

(Succ x) - (Succ y) = x - y

plus :: Natural a -> Natural b -> Natural (a + b)

Addition of naturals at the term and type levels simultaneously.

minus :: b <= a => Natural a -> Natural b -> Natural (a - b)

Subtraction of naturals at the term and type level simultaneously. Note that it is statically prohibited to subtract a number larger than the number from which it is being subtracted.