Data.TypeFun

Documentation

class Kind (Domain fun) => TypeFun fun

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

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

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

newtype WrappedApp fun arg

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

Constructors

WrapApp (App fun arg)

unwrapApp :: WrappedApp fun arg -> App fun arg

The inverse of WrapApp.

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

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

data Id dom

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

Instances

Kind dom => TypeFun (Id dom)

data Const dom val

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

Instances

Kind dom => TypeFun (Const dom val)