Safe Haskell | None |
---|---|

Language | Haskell2010 |

- 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.

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.

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.