type-functions- Emulation of type-level functions




class Kind (Domain fun) => TypeFun fun Source

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

Note that the (->) instance of TypeFun slightly abuses the type constructor (->). In representations of type-level functions, (->) denotes the lifting of the type constructor (->). That is if r and r' are representations of functions f and f', the type r -> r' represents the function \t -> (f t -> f' t).

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.


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.

newtype WrappedApp fun arg Source

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


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.

data Id dom Source

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


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.


Kind dom => TypeFun (Const dom val)