PeanoWitnesses-0.1.0.0: GADT type witnesses for Peano-style natural numbers.

Data.Numeric.Witness.Peano

Description

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

Synopsis

# Documentation

data Zero Source

Instances

 ReifyNatural Zero

data Succ n Source

Instances

 ReifyNatural n => ReifyNatural (Succ n)

data Natural n where Source

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 Source

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

Methods

Instances

 ReifyNatural Zero ReifyNatural n => ReifyNatural (Succ n)

type family LessThanOrEqual a b Source

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 Source

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

type family LessThan a b Source

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 Source

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

type family x + y Source

Equations

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

type family x - y Source

Type level subtraction.

Equations

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

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

Addition of naturals at the term and type levels simultaneously.

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

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.