Type-level functions are represented by types.
TypeFun is the class of all function
Note that the
(->) instance of
TypeFun slightly abuses the type
(->). In representations of type-level functions,
(->) denotes the
lifting of the type constructor
(->). That is if
representations of functions
f', the type
r -> r' represents
\t -> (f t -> f' t).
The domain of the type-level function as a subkind representation. Subkind handling is provided by the kinds package.
Application of type-level functions.
App takes a function representation and an argument
and returns the corresponding result.
A data type that is isomorphic to the type synonym family
Turns a type-level function into the intersection of all its results.
Id d represents the type-level identity function whose domain is represented