| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Calculi.Lambda.Cube.Dependent
- class SimpleType t => Dependent t where
- type DependentTerm t :: * -> *
Documentation
class SimpleType t => Dependent t where Source #
Typesystems which can have values in their types.
Minimal complete definition
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.