Emulation of type-level functions.
- class Kind (Domain fun) => TypeFun fun where
- type Domain fun
- type family App fun arg
- data Id dom = Id dom
- data Const dom val = Const dom
- data fun :-> fun' = fun :-> fun'
- data FunMap trans fun
- newtype WrappedApp fun arg = WrapApp (App fun arg)
- unwrapApp :: WrappedApp fun arg -> App fun arg
- type Universal fun = forall arg. Inhabitant (Domain fun) arg => WrappedApp fun arg
Type-level functions in general
Type-level functions are represented by types.
TypeFun is the class of all type-level
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.
Construction of type-level functions
Id d represents the type-level identity function whose domain is represented
Const d v represents the constant type-level function whose domain is
d, and whose result is
|fun :-> fun'|
t is a type of kind
* -> *, and
f is the representation of a
FunMap t f represents the function
\arg -> t (App f arg).
A data type that is isomorphic to the type synonym family