Nix.Frames

The type-safe cast operation

Decide an equality of two types

Extract a witness of equality of two types

Applies a type to a function type. Returns: Just u if the first argument represents a function of type t -> u and the second argument represents a function of type t. Otherwise, returns Nothing.

A flexible variation parameterised in a type constructor

Cast over k1 -> k2

Cast over k1 -> k2 -> k3

Decide heterogeneous equality of two types.

Extract a witness of heterogeneous equality of two types

Build a function type.

Force a TypeRep to normal form.

Show a type representation

Splits a type constructor application. Note that if the type constructor is polymorphic, this will not return the kinds that were used.

Takes a value of type a and returns a concrete representation of that type.

Observe the argument types of a type representation

Takes a value of type a and returns a concrete representation of that type.

Observe the type constructor of a quantified type representation.

Proxy is a type that holds no data, but has a phantom parameter of arbitrary type (or even kind). Its use is to provide type information, even though there is no value available of that type (or it may be too costly to create one).

Historically, Proxy :: Proxy a is a safer alternative to the undefined :: a idiom.

>>> Proxy :: Proxy (Void, Int -> Int)Proxy

Proxy can even hold types of higher kinds,

>>> Proxy :: Proxy EitherProxy

>>> Proxy :: Proxy FunctorProxy

>>> Proxy :: Proxy complicatedStructureProxy

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Kind heterogeneous propositional equality. Like :~:, a :~~: b is inhabited by a terminating value if and only if a is the same type as b.

A quantified type representation.

The class Typeable allows a concrete representation of a type to be calculated.