Type.Family.Nat

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

Documentation

data N

Constructors

Z

S N

Instances

Eq N

Methods

(==) :: N -> N -> Bool

(/=) :: N -> N -> Bool

Ord N

Methods

compare :: N -> N -> Ordering

(<) :: N -> N -> Bool

(<=) :: N -> N -> Bool

(>) :: N -> N -> Bool

(>=) :: N -> N -> Bool

max :: N -> N -> N

min :: N -> N -> N

Show N

Methods

showsPrec :: Int -> N -> ShowS

show :: N -> String

showList :: [N] -> ShowS

TestEquality N Nat

Methods

testEquality :: f a -> f b -> Maybe ((Nat :~: a) b)

Read1 N Nat

Methods

readsPrec1 :: Int -> ReadS (Some Nat f)

Read1 N Fin

Methods

readsPrec1 :: Int -> ReadS (Some Fin f)

Show1 N Nat

Methods

showsPrec1 :: Int -> f a -> ShowS

show1 :: f a -> String

Show1 N Fin

Methods

showsPrec1 :: Int -> f a -> ShowS

show1 :: f a -> String

Ord1 N Nat

Methods

compare1 :: f a -> f a -> Ordering

(<#) :: f a -> f a -> Bool

(>#) :: f a -> f a -> Bool

(<=#) :: f a -> f a -> Bool

(>=#) :: f a -> f a -> Bool

Ord1 N Fin

Methods

compare1 :: f a -> f a -> Ordering

(<#) :: f a -> f a -> Bool

(>#) :: f a -> f a -> Bool

(<=#) :: f a -> f a -> Bool

(>=#) :: f a -> f a -> Bool

Eq1 N Nat

Methods

eq1 :: f a -> f a -> Bool

neq1 :: f a -> f a -> Bool

Eq1 N Fin

Methods

eq1 :: f a -> f a -> Bool

neq1 :: f a -> f a -> Bool

BoolEquality N Nat

Methods

boolEquality :: f a -> f b -> Boolean ((Nat == a) b)

Known N Nat Z

Z_ is the canonical construction of a Nat Z.

Associated Types

type KnownC Nat (Z :: Nat -> *) (a :: Nat) :: Constraint

Methods

known :: Z a

Read2 N N IFin

Methods

readsPrec2 :: Int -> ReadS (Some2 IFin k f)

Show2 N N IFin

Methods

showsPrec2 :: Int -> f a b -> ShowS

show2 :: f a b -> String

Ord2 N N IFin

Methods

compare2 :: f a b -> f a b -> Ordering

(<##) :: f a b -> f a b -> Bool

(>##) :: f a b -> f a b -> Bool

(<=##) :: f a b -> f a b -> Bool

(>=##) :: f a b -> f a b -> Bool

Eq2 N N IFin

Methods

eq2 :: f a b -> f a b -> Bool

neq2 :: f a b -> f a b -> Bool

Known N Nat n => Known N Nat (S n)

If n is a canonical construction of Nat n, S_ n is the canonical construction of Nat (S n).

Associated Types

type KnownC Nat (S n :: Nat -> *) (a :: Nat) :: Constraint

Methods

known :: S n a

Show1 N (IFin x)

Methods

showsPrec1 :: Int -> f a -> ShowS

show1 :: f a -> String

Ord1 N (IFin x)

Methods

compare1 :: f a -> f a -> Ordering

(<#) :: f a -> f a -> Bool

(>#) :: f a -> f a -> Bool

(<=#) :: f a -> f a -> Bool

(>=#) :: f a -> f a -> Bool

Eq1 N (IFin x)

Methods

eq1 :: f a -> f a -> Bool

neq1 :: f a -> f a -> Bool

(~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as)

Associated Types

type WitnessC (ØC :: Constraint) ((Known N Nat n, Known [k] (Length k) as) :: Constraint) (Length k as) :: Constraint

Methods

(\\) :: ØC => ((Known N Nat n, Known [k] (Length k) as) -> r) -> Length k as -> r

(~) N n' (Pred n) => Witness ØC ((~) N (S n') n) (Fin n)

A Fin n is a Witness that n >= 1.

That is, Pred n is well defined.

Associated Types

type WitnessC (ØC :: Constraint) ((~) N (S n') n :: Constraint) (Fin n) :: Constraint

Methods

(\\) :: ØC => ((N ~ S n') n -> r) -> Fin n -> r

Witness ØC (Known N Nat n) (Nat n)

A Nat n is a Witness that there is a canonical construction for Nat n.

Associated Types

type WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (Nat n) :: Constraint

Methods

(\\) :: ØC => (Known N Nat n -> r) -> Nat n -> r

(~) N x' (Pred x) => Witness ØC ((~) N (S x') x) (IFin x y)

An IFin x y is a Witness that x >= 1.

That is, Pred x is well defined.

Associated Types

type WitnessC (ØC :: Constraint) ((~) N (S x') x :: Constraint) (IFin x y) :: Constraint

Methods

(\\) :: ØC => ((N ~ S x') x -> r) -> IFin x y -> r

Witness ØC (Known N Nat n) (VecT k n f a)

Associated Types

type WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (VecT k n f a) :: Constraint

Methods

(\\) :: ØC => (Known N Nat n -> r) -> VecT k n f a -> r

((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N x' (Pred x)) => Witness ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y)

Associated Types

type WitnessC (ØC :: Constraint) (((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) :: Constraint) (NatGT x y) :: Constraint

Methods

(\\) :: ØC => (((N ~ x) (S x'), Known N Nat y, (Bool ~ lt) False, (Bool ~ eq) False, (Bool ~ gt) True) -> r) -> NatGT x y -> r

((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y)) => Witness ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y)

Associated Types

type WitnessC (ØC :: Constraint) (((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) :: Constraint) (NatEQ x y) :: Constraint

Methods

(\\) :: ØC => (((N ~ x) y, Known N Nat x, (Bool ~ lt) False, (Bool ~ eq) True, (Bool ~ gt) False) -> r) -> NatEQ x y -> r

((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N y' (Pred y)) => Witness ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y)

Associated Types

type WitnessC (ØC :: Constraint) (((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) :: Constraint) (NatLT x y) :: Constraint

Methods

(\\) :: ØC => (((N ~ y) (S y'), Known N Nat x, (Bool ~ lt) True, (Bool ~ eq) False, (Bool ~ gt) False) -> r) -> NatLT x y -> r

type (==) N x y

type (==) N x y = NatEq x y

type KnownC N Nat Z

type KnownC N Nat Z = ØC

type KnownC N Nat (S n)

type KnownC N Nat (S n) = Known N Nat n

type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as)

type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) = (~) N n (Len k as)

type WitnessC ØC ((~) N (S n') n) (Fin n)

type WitnessC ØC ((~) N (S n') n) (Fin n) = (~) N n' (Pred n)

type WitnessC ØC (Known N Nat n) (Nat n)

type WitnessC ØC (Known N Nat n) (Nat n) = ØC

type WitnessC ØC ((~) N (S x') x) (IFin x y)

type WitnessC ØC ((~) N (S x') x) (IFin x y) = (~) N x' (Pred x)

type WitnessC ØC (Known N Nat n) (VecT k n f a)

type WitnessC ØC (Known N Nat n) (VecT k n f a) = ØC

type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y)

type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N x' (Pred x))

type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y)

type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y))

type WitnessC ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y)

type WitnessC ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N y' (Pred y))

fromInt :: Int -> Maybe N

type family IsZero (x :: N) :: Bool where ...

Equations

IsZero Z = True

IsZero (S x) = False

zeroCong :: (x ~ y) :- (IsZero x ~ IsZero y)

zNotS :: (Z ~ S x) :- Fail

type family NatEq (x :: N) (y :: N) :: Bool where ...

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) = (xs :: [N]) | xs -> x where ...

Equations

Iota Z = Ø

Iota (S x) = x :< Iota x

iotaCong :: (x ~ y) :- (Iota x ~ Iota y)

type family Pred (x :: N) :: N where ...

Equations

Pred (S n) = n

type Pos n = n ~ S (Pred n)

predCong :: (x ~ y) :- (Pred x ~ Pred y)

type family (x :: N) + (y :: N) :: N where ... infixr 6

Equations

Z + y = y

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

data AddW f :: N -> * where

Constructors

AddW :: !(f x) -> !(f y) -> AddW f (x + y)

addCong :: (w ~ y, x ~ z) :- ((w + x) ~ (y + z))

type family (x :: N) * (y :: N) :: N where ... infixr 7

Equations

Z * y = Z

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

data MulW f :: N -> * where

Constructors

MulW :: !(f x) -> !(f y) -> MulW f (x * y)

mulCong :: (w ~ y, x ~ z) :- ((w * x) ~ (y * z))

type family (x :: N) ^ (y :: N) :: N where ... infixl 8

Equations

x ^ Z = S Z

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

expCong :: (w ~ y, x ~ z) :- ((w ^ x) ~ (y ^ z))

type family Len (as :: [k]) :: N where ...

Equations

Len Ø = Z

Len (a :< as) = S (Len as)

lenCong :: (as ~ bs) :- (Len as ~ Len bs)

type family Ix (x :: N) (as :: [k]) :: k where ...

Equations

Ix Z (a :< as) = a

Ix (S x) (a :< as) = Ix x as

ixCong :: (x ~ y, as ~ bs) :- (Ix x as ~ Ix y bs)

type family (x :: N) < (y :: N) :: Bool where ... infix 4

Equations

Z < Z = False

Z < (S y) = True

(S x) < Z = False

(S x) < (S y) = x < y

type (<=) x y = (x == y) || (x < y) infix 4

type family (x :: N) > (y :: N) :: Bool where ... infix 4

Equations

Z > Z = False

Z > (S y) = False

(S x) > Z = True

(S x) > (S y) = x > y

type (>=) x y = (x == y) || (x > y) infix 4

type N0 = Z

Convenient aliases for low-value Peano numbers.

type N1 = S N0

type N2 = S N1

type N3 = S N2

type N4 = S N3

type N5 = S N4

type N6 = S N5

type N7 = S N6

type N8 = S N7

type N9 = S N8

type N10 = S N9