type-indexed-queues-0.1.0.1: Queues with verified and unverified versions.

TypeLevel.Singletons

Description

Synopsis

# Documentation

data family The k :: k -> * Source #

A data family for singletons. The cute name allows code like this:

addZeroZero :: The Nat n -> n + 0 :~: n

Instances

 data The Bool Source # data The Bool whereFalsy :: The Bool FalseTruey :: The Bool True data The Nat Source # This is just a newtype wrapper for Integer. As such, it is only valid if the programmer can't construct values where the type index doesn't match the contained value. For that reason, the constructor is not exported.The reason for this setup is to allow properties and invariants to be proven about the numbers involved, while actual computation can be carried out efficiently on the values at runtime.See the implementation of Data.Heap.Indexed.Leftist for an example of the uses of this type. data The Nat = NatSing Integer data The Nat Source # Singleton for type-level Peano numbers. data The Nat whereZy :: The Nat ZSy :: The Nat (S n) data The [k] Source # data The [k] whereNily :: The [k] ([] k)(:-) :: The [k] ((:) k x xs)

class KnownSing x where Source #

Class for singletons which can be generated.

Minimal complete definition

sing

Methods

sing :: The k x Source #

Instances

 Source # Methods Source # Methods KnownNat n => KnownSing Nat n Source # Methodssing :: The n x Source # KnownSing [k] ([] k) Source # Methodssing :: The [k] x Source # (KnownSing [a] xs, KnownSing a x) => KnownSing [a] ((:) a x xs) Source # Methodssing :: The ((a ': x) xs) x Source #

(*.) :: The Nat n -> The Nat m -> The Nat (n * m) infixl 7 Source #

Multiply two numbers, on both the value and type level.

(+.) :: The Nat n -> The Nat m -> The Nat (n + m) infixl 6 Source #

Add two numbers, on both the value and type level.

(^.) :: The Nat n -> The Nat m -> The Nat (n ^ m) infixr 8 Source #

Raise a number to a power, on the type-level and value-level.

(-.) :: m <= n => The Nat n -> The Nat m -> The Nat (n - m) infixl 6 Source #

Subtract two numbers, on the type-level and value-level, with a proof that overflow can't occur.

(<=.) :: The Nat n -> The Nat m -> The Bool (n <=? m) infix 4 Source #

Test order between two numbers, and provide a proof of that order with the result.

totalOrder :: p n -> q m -> ((n <=? m) :~: False) -> (m <=? n) :~: True Source #

A proof of a total order on the naturals.

type (<=) x y = (x <=? y) :~: True Source #

A proof that x is less than or equal to y.

type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6 #

type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7 #

Multiplication of type-level naturals.

type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #

Exponentiation of type-level naturals.

data Nat :: * #

(Kind) This is the kind of type-level natural numbers.

Instances

 KnownNat n => KnownSing Nat n Source # Methodssing :: The n x Source # data The Nat Source # This is just a newtype wrapper for Integer. As such, it is only valid if the programmer can't construct values where the type index doesn't match the contained value. For that reason, the constructor is not exported.The reason for this setup is to allow properties and invariants to be proven about the numbers involved, while actual computation can be carried out efficiently on the values at runtime.See the implementation of Data.Heap.Indexed.Leftist for an example of the uses of this type. data The Nat = NatSing Integer type (==) Nat a b type (==) Nat a b = EqNat a b