Type-level functions in general

Type-level functions are represented by types. TypeFun is the class of all type-level function representations.

Associated Types

The domain of the type-level function as a subkind representation. Subkind handling is provided by the kinds package.

Instances

Kind dom => TypeFun (Id dom)
(Domain fun ~ Domain fun', TypeFun fun, TypeFun fun') => TypeFun (:-> fun fun')
Kind dom => TypeFun (Const dom val)

type family App fun arg Source

Application of type-level functions. App takes a function representation and an argument and returns the corresponding result.

Specific type-level functions

data Id dom Source

A type Id d represents the type-level identity function whose domain is represented by d.

Constructors

Id dom

Instances

Kind dom => TypeFun (Id dom)

data Const dom val Source

A type Const d v represents the constant type-level function whose domain is represented by d, and whose result is v.

Constructors

Const dom val

Instances

Kind dom => TypeFun (Const dom val)

data fun :-> fun' Source

A type f :-> f' represents the type-level function \arg -> (f arg -> f' arg).

Constructors

fun :-> fun'

Instances

(Domain fun ~ Domain fun', TypeFun fun, TypeFun fun') => TypeFun (:-> fun fun')

newtype WrappedApp fun arg Source

A data type that is isomorphic to the type synonym family App.

Constructors

WrapApp (App fun arg)

The inverse of WrapApp.

type Universal fun = forall arg. Inhabitant (Domain fun) arg => WrappedApp fun argSource

Turns a type-level function into the intersection of all its results.