Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <kylcarte@indiana.edu>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

Type.Family.Nat

Description

Type-level natural numbers, along with frequently used type families over them.

Synopsis

Documentation

data N Source

Constructors

Z
S N

Instances

Eq N Source
Ord N Source
Show N Source
TestEquality N Nat
DecEquality N Nat Source
Known N Nat Z Source	`Z_` is the canonical construction of a `Nat Z`.
Known N Nat n => Known N Nat (S n) Source	If `n` is a canonical construction of `Nat n`, `S_ n` is the canonical construction of `Nat (S n)`.
(~) N n' (Pred n) => Witness ØC ((~) N (S n') n) (Fin n) Source	A `Fin n` is a `Witness` that `n >= 1`. That is, `Pred n` is well defined.
Witness ØC (Known N Nat n) (Nat n) Source	A `Nat n` is a `Witness` that there is a canonical construction for `Nat n`.
Witness ØC (Known N Nat n) (VT k n f a) Source
type (==) N x y = NatEq x y Source
type KnownC N Nat Z = ØC
type KnownC N Nat (S n) = Known N Nat n Source
type WitnessC ØC ((~) N (S n') n) (Fin n) = (~) N n' (Pred n) Source
type WitnessC ØC (Known N Nat n) (Nat n) = ØC
type WitnessC ØC (Known N Nat n) (VT k n f a) = ØC

type family NatEq x y :: Bool Source

Equations

NatEq Z Z = True
NatEq Z (S y) = False
NatEq (S x) Z = False
NatEq (S x) (S y) = NatEq x y

type family Iota x :: [N] Source

Equations

Iota Z = Ø
Iota (S x) = x :< Iota x

type family Pred x :: N Source

Equations

Pred (S n) = n

type family x + y :: N infixr 6 Source

Equations

Z + y = y
(S x) + y = S (x + y)

type family x * y :: N infixr 7 Source

Equations

Z * y = Z
(S x) * y = (x * y) + y

type family x ^ y :: N infixl 8 Source

Equations

x ^ Z = S Z
x ^ (S y) = (x ^ y) * x

type N0 = Z Source

Convenient aliases for low-value Peano numbers.

type N1 = S N0 Source

type N2 = S N1 Source

type N3 = S N2 Source

type N4 = S N3 Source

type N5 = S N4 Source

type N6 = S N5 Source

type N7 = S N6 Source

type N8 = S N7 Source

type N9 = S N8 Source

type N10 = S N9 Source

type family a == b :: Bool infix 4

A type family to compute Boolean equality. Instances are provided only for open kinds, such as * and function kinds. Instances are also provided for datatypes exported from base. A poly-kinded instance is not provided, as a recursive definition for algebraic kinds is generally more useful.

Instances

type (==) Bool a b = EqBool a b
type (==) Ordering a b = EqOrdering a b
type (==) * a b = EqStar a b
type (==) () a b = EqUnit a b
type (==) N x y = NatEq x y
type (==) [k] a b = EqList k a b
type (==) (Maybe k) a b = EqMaybe k a b
type (==) (k -> k1) a b = EqArrow k k1 a b
type (==) (Either k k1) a b = EqEither k k1 a b
type (==) ((,) k k1) a b = Eq2 k k1 a b
type (==) ((,,) k k1 k2) a b = Eq3 k k1 k2 a b
type (==) ((,,,) k k1 k2 k3) a b = Eq4 k k1 k2 k3 a b
type (==) ((,,,,) k k1 k2 k3 k4) a b = Eq5 k k1 k2 k3 k4 a b
type (==) ((,,,,,) k k1 k2 k3 k4 k5) a b = Eq6 k k1 k2 k3 k4 k5 a b
type (==) ((,,,,,,) k k1 k2 k3 k4 k5 k6) a b = Eq7 k k1 k2 k3 k4 k5 k6 a b
type (==) ((,,,,,,,) k k1 k2 k3 k4 k5 k6 k7) a b = Eq8 k k1 k2 k3 k4 k5 k6 k7 a b
type (==) ((,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8) a b = Eq9 k k1 k2 k3 k4 k5 k6 k7 k8 a b
type (==) ((,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9) a b = Eq10 k k1 k2 k3 k4 k5 k6 k7 k8 k9 a b
type (==) ((,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10) a b = Eq11 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 a b
type (==) ((,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11) a b = Eq12 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 a b
type (==) ((,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12) a b = Eq13 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 a b
type (==) ((,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13) a b = Eq14 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 a b
type (==) ((,,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14) a b = Eq15 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14 a b