Type-level functions in general

class Kind (Domain fun) => TypeFun fun Source

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

Associated Types

type Domain fun Source

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)
TypeFun fun => TypeFun (FunMap trans fun)
(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.

Construction of 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

Instances

Kind dom => TypeFun (Const dom val)

data fun :-> fun' Source

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

Constructors

fun :-> fun'

Instances

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

data FunMap trans fun Source

If t is a type of kind * -> *, and f is the representation of a type-level function, FunMap t f represents the function \arg -> t (App f arg).

Instances

TypeFun fun => TypeFun (FunMap trans fun)

Utilities

newtype WrappedApp fun arg Source

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

Constructors

WrapApp (App fun arg)

unwrapApp :: WrappedApp fun arg -> App fun argSource

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.