typerbole-0.0.0.5: A typeystems library with exaggerated claims

Calculi.Lambda.Cube.Dependent

Synopsis

# Documentation

class SimpleType t => Dependent t where Source #

Typesystems which can have values in their types.

Minimal complete definition

valueToType

Associated Types

type DependentTerm t :: * -> * Source #

A value-level term that can be encoded as a type expression.

Of kind * -> * because it expects a typesystem as a parameter.

Methods

valueToType :: DependentTerm t t -> t Source #

Encode a value at the type-level. This could be just a constructor or a complete transformation of the AST, but this typeclass doesn't care.