TypeLevel.Singletons

Provides singletons and general type-level utilities. singletons are value-level representations of types.

Eisenberg, Richard A., and Stephanie Weirich. “Dependently Typed Programming with Singletons.” In Proceedings of the 2012 Haskell Symposium, 117–130. Haskell ’12. New York, NY, USA: ACM, 2012. doi:10.1145/2364506.2364522.

Documentation

data family The k :: k -> *

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

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

Instances

data The Bool

data The Bool where

• Falsy :: The Bool False
• Truey :: The Bool True

data The Nat

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

Singleton for type-level Peano numbers.

data The Nat where

• Zy :: The Nat Z
• Sy :: The Nat (S n)

data The [k]

data The [k] where

• Nily :: The [k] ([] k)
• (:-) :: The [k] ((:) k x xs)

class KnownSing x where

Class for singletons which can be generated.

Minimal complete definition

sing

Methods

sing :: The k x

Instances

KnownSing Bool False

Methods

sing :: The False x

KnownSing Bool True

Methods

sing :: The True x

KnownNat n => KnownSing Nat n

Methods

sing :: The n x

KnownSing [k] ([] k)

Methods

sing :: The [k] x

(KnownSing [a] xs, KnownSing a x) => KnownSing [a] ((:) a x xs)

Methods

sing :: The ((a ': x) xs) x

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

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

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

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

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

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

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

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

A proof of a total order on the naturals.

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

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

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

Addition of type-level naturals.

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

Methods

sing :: The n x

data The Nat

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