garden
Maintainergatlin@niltag.net
Safe HaskellSafe
LanguageHaskell2010

Peano

Description

Definition of type-level Peano numerals along with type operators to inspect and manipulate them.

Synopsis

Natural numbers

data Natural (n :: Type) Source #

Natural numbers paired with type-level natural numbers. These terms each act as a witness for a particular natural.

Constructors

n ~ Z => Zero 
forall t.n ~ S t => Succ (Natural t) 

data Z Source #

Instances

Instances details
ReifyNatural Z Source # 
Instance details

Defined in Peano

Minus x Z Source # 
Instance details

Defined in Peano

Associated Types

type x - Z Source #

Methods

minus :: Natural x -> Natural Z -> Natural (x - Z) Source #

Plus x Z Source # 
Instance details

Defined in Peano

Associated Types

type x + Z Source #

Methods

plus :: Natural x -> Natural Z -> Natural (x + Z) Source #

Replicable Z (x :: k) Source # 
Instance details

Defined in Lists

Associated Types

type Replicate Z x Source #

LT Z Z Source # 
Instance details

Defined in Peano

Associated Types

type LessThan Z Z :: Bool Source #

LTE Z Z Source # 
Instance details

Defined in Peano

Associated Types

type LessThanOrEqual Z Z :: Bool Source #

LT Z (S m :: Type) Source # 
Instance details

Defined in Peano

Associated Types

type LessThan Z (S m) :: Bool Source #

LTE Z (S m :: Type) Source # 
Instance details

Defined in Peano

Associated Types

type LessThanOrEqual Z (S m) :: Bool Source #

LT (S n :: Type) Z Source # 
Instance details

Defined in Peano

Associated Types

type LessThan (S n) Z :: Bool Source #

LTE (S n :: Type) Z Source # 
Instance details

Defined in Peano

Associated Types

type LessThanOrEqual (S n) Z :: Bool Source #

Functor t => Cross (S Z) t Source # 
Instance details

Defined in Sheet

Methods

cross :: Counted (S Z) (t a) -> Nested (NestedNTimes (S Z) t) (Counted (S Z) a) Source #

type x - Z Source # 
Instance details

Defined in Peano

type x - Z = x
type x + Z Source # 
Instance details

Defined in Peano

type x + Z = x
type Replicate Z (x :: k) Source # 
Instance details

Defined in Lists

type Replicate Z (x :: k) = Nil
type LessThan Z Z Source # 
Instance details

Defined in Peano

type LessThan Z Z = 'False
type LessThanOrEqual Z Z Source # 
Instance details

Defined in Peano

type LessThan Z (S m :: Type) Source # 
Instance details

Defined in Peano

type LessThan Z (S m :: Type) = 'True
type LessThanOrEqual Z (S m :: Type) Source # 
Instance details

Defined in Peano

type LessThanOrEqual Z (S m :: Type) = 'True
type LessThan (S n :: Type) Z Source # 
Instance details

Defined in Peano

type LessThan (S n :: Type) Z = 'False
type LessThanOrEqual (S n :: Type) Z Source # 
Instance details

Defined in Peano

type LessThanOrEqual (S n :: Type) Z = 'False

data S (n :: k) Source #

Instances

Instances details
Plus x y => Plus x (S y) Source # 
Instance details

Defined in Peano

Associated Types

type x + (S y) Source #

Methods

plus :: Natural x -> Natural (S y) -> Natural (x + S y) Source #

Replicable n x => Replicable (S n) (x :: k) Source # 
Instance details

Defined in Lists

Associated Types

type Replicate (S n) x Source #

LT Z (S m :: Type) Source # 
Instance details

Defined in Peano

Associated Types

type LessThan Z (S m) :: Bool Source #

LTE Z (S m :: Type) Source # 
Instance details

Defined in Peano

Associated Types

type LessThanOrEqual Z (S m) :: Bool Source #

LT (S n :: Type) Z Source # 
Instance details

Defined in Peano

Associated Types

type LessThan (S n) Z :: Bool Source #

LTE (S n :: Type) Z Source # 
Instance details

Defined in Peano

Associated Types

type LessThanOrEqual (S n) Z :: Bool Source #

LT n m => LT (S n :: Type) (S m :: Type) Source # 
Instance details

Defined in Peano

Associated Types

type LessThan (S n) (S m) :: Bool Source #

LTE (S n :: Type) (S m :: Type) Source # 
Instance details

Defined in Peano

Associated Types

type LessThanOrEqual (S n) (S m) :: Bool Source #

ReifyNatural n => ReifyNatural (S n) Source # 
Instance details

Defined in Peano

Methods

reifyNatural :: Natural (S n) Source #

(Cross (S n) t, Functor t, Functor (Nested (NestedNTimes (S n) t))) => Cross (S (S n)) t Source # 
Instance details

Defined in Sheet

Methods

cross :: Counted (S (S n)) (t a) -> Nested (NestedNTimes (S (S n)) t) (Counted (S (S n)) a) Source #

Functor t => Cross (S Z) t Source # 
Instance details

Defined in Sheet

Methods

cross :: Counted (S Z) (t a) -> Nested (NestedNTimes (S Z) t) (Counted (S Z) a) Source #

Minus x y => Minus (S x) (S y) Source # 
Instance details

Defined in Peano

Associated Types

type (S x) - (S y) Source #

Methods

minus :: Natural (S x) -> Natural (S y) -> Natural (S x - S y) Source #

type x + (S y) Source # 
Instance details

Defined in Peano

type x + (S y) = S (x + y)
type Replicate (S n) (x :: k) Source # 
Instance details

Defined in Lists

type Replicate (S n) (x :: k) = x :-: Replicate n x
type LessThan Z (S m :: Type) Source # 
Instance details

Defined in Peano

type LessThan Z (S m :: Type) = 'True
type LessThanOrEqual Z (S m :: Type) Source # 
Instance details

Defined in Peano

type LessThanOrEqual Z (S m :: Type) = 'True
type LessThan (S n :: Type) Z Source # 
Instance details

Defined in Peano

type LessThan (S n :: Type) Z = 'False
type LessThanOrEqual (S n :: Type) Z Source # 
Instance details

Defined in Peano

type LessThanOrEqual (S n :: Type) Z = 'False
type LessThan (S n :: Type) (S m :: Type) Source # 
Instance details

Defined in Peano

type LessThan (S n :: Type) (S m :: Type) = LessThan n m
type LessThanOrEqual (S n :: Type) (S m :: Type) Source # 
Instance details

Defined in Peano

type LessThanOrEqual (S n :: Type) (S m :: Type) = LessThanOrEqual n m
type (S x) - (S y) Source # 
Instance details

Defined in Peano

type (S x) - (S y) = x - y

class ReifyNatural (n :: Type) where Source #

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

Instances

Instances details
ReifyNatural Z Source # 
Instance details

Defined in Peano

ReifyNatural n => ReifyNatural (S n) Source # 
Instance details

Defined in Peano

Methods

reifyNatural :: Natural (S n) Source #

Partial ordering

Less-than

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

This constraint is similar to <=.

class LT (a :: k1) (b :: k2) Source #

Type-level < test.

Associated Types

type LessThan a b :: Bool Source #

Instances

Instances details
LT Z Z Source # 
Instance details

Defined in Peano

Associated Types

type LessThan Z Z :: Bool Source #

LT Z (S m :: Type) Source # 
Instance details

Defined in Peano

Associated Types

type LessThan Z (S m) :: Bool Source #

LT (S n :: Type) Z Source # 
Instance details

Defined in Peano

Associated Types

type LessThan (S n) Z :: Bool Source #

LT n m => LT (S n :: Type) (S m :: Type) Source # 
Instance details

Defined in Peano

Associated Types

type LessThan (S n) (S m) :: Bool Source #

Less-than-or-equal

type (<=) a b = (LessThanOrEqual a b ~ True, Minus b a) Source #

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

class LTE (a :: k1) (b :: k2) Source #

Type-level <= test.

Associated Types

type LessThanOrEqual a b :: Bool Source #

Instances

Instances details
LTE Z Z Source # 
Instance details

Defined in Peano

Associated Types

type LessThanOrEqual Z Z :: Bool Source #

LTE Z (S m :: Type) Source # 
Instance details

Defined in Peano

Associated Types

type LessThanOrEqual Z (S m) :: Bool Source #

LTE (S n :: Type) Z Source # 
Instance details

Defined in Peano

Associated Types

type LessThanOrEqual (S n) Z :: Bool Source #

LTE (S n :: Type) (S m :: Type) Source # 
Instance details

Defined in Peano

Associated Types

type LessThanOrEqual (S n) (S m) :: Bool Source #

Arithmetic

Addition

type family x + y :: Type Source #

Instances

Instances details
type x + Z Source # 
Instance details

Defined in Peano

type x + Z = x
type x + (S y) Source # 
Instance details

Defined in Peano

type x + (S y) = S (x + y)

class Plus (x :: Type) (y :: Type) where Source #

Natural addition

Associated Types

type x + y :: Type Source #

Methods

plus :: Natural x -> Natural y -> Natural (x + y) Source #

Instances

Instances details
Plus x Z Source # 
Instance details

Defined in Peano

Associated Types

type x + Z Source #

Methods

plus :: Natural x -> Natural Z -> Natural (x + Z) Source #

Plus x y => Plus x (S y) Source # 
Instance details

Defined in Peano

Associated Types

type x + (S y) Source #

Methods

plus :: Natural x -> Natural (S y) -> Natural (x + S y) Source #

Subtraction

type family x - y :: Type Source #

Instances

Instances details
type x - Z Source # 
Instance details

Defined in Peano

type x - Z = x
type (S x) - (S y) Source # 
Instance details

Defined in Peano

type (S x) - (S y) = x - y

class Minus (x :: Type) (y :: Type) where Source #

Natural subtraction

Associated Types

type x - y :: Type Source #

Methods

minus :: LessThanOrEqual y x ~ True => Natural x -> Natural y -> Natural (x - y) Source #

Instances

Instances details
Minus x Z Source # 
Instance details

Defined in Peano

Associated Types

type x - Z Source #

Methods

minus :: Natural x -> Natural Z -> Natural (x - Z) Source #

Minus x y => Minus (S x) (S y) Source # 
Instance details

Defined in Peano

Associated Types

type (S x) - (S y) Source #

Methods

minus :: Natural (S x) -> Natural (S y) -> Natural (S x - S y) Source #