Data.TypeFun

Emulation of type-level functions.

Type-level functions in general

class Kind (Domain fun) => TypeFun fun

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

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)

Associated Types

type Domain (Id dom) :: *

TypeFun fun => TypeFun (FunMap trans fun)

Associated Types

type Domain (FunMap trans fun) :: *

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

Associated Types

type Domain ((:->) fun fun') :: *

Kind dom => TypeFun (Const dom val)

Associated Types

type Domain (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.

Instances

type App (Id dom) arg

type App (Id dom) arg = arg

type App (FunMap trans fun) arg

type App (FunMap trans fun) arg = trans (App fun arg)

type App ((:->) fun fun') arg

type App ((:->) fun fun') arg = App fun arg -> App fun' arg

type App (Const dom val) arg

type App (Const dom val) arg = val

Construction of type-level functions

data Id dom

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)

Associated Types

type Domain (Id dom) :: *

type Domain (Id dom)

type Domain (Id dom) = dom

type App (Id dom) arg

type App (Id dom) arg = arg

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.

Constructors

Const dom

Instances

Kind dom => TypeFun (Const dom val)

Associated Types

type Domain (Const dom val) :: *

type Domain (Const dom val)

type Domain (Const dom val) = dom

type App (Const dom val) arg

type App (Const dom val) arg = val

data fun :-> fun' infixr 1

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

Constructors

fun :-> fun' infixr 1

Instances

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

Associated Types

type Domain ((:->) fun fun') :: *

type Domain ((:->) fun fun')

type Domain ((:->) fun fun') = Domain fun

type App ((:->) fun fun') arg

type App ((:->) fun fun') arg = App fun arg -> App fun' arg

data FunMap trans fun

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)

Associated Types

type Domain (FunMap trans fun) :: *

type Domain (FunMap trans fun)

type Domain (FunMap trans fun) = Domain fun

type App (FunMap trans fun) arg

type App (FunMap trans fun) arg = trans (App fun arg)

Utilities

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.