Type structures

[jonhue]

Type structures should allow relating types to values.

A type structure is separated into a formal definition (declaration) and instantiations much like type classes.

A type structure consists of a name, a named list of variables it will be instantiated with, and a list of properties/invariants relating the variables that have to be proven for all instantiations (or, alternatively, assumed to be true).

Each instantiation refers to a concrete type, concrete values for each of the variables, and proofs for all invariants.

Example:

structure Monoid<m>(
  e :: m,
  f :: m -> m -> m
) where
  a :: m. e `f` a = a
  a :: m. a `f` e = a
  a :: m, b :: m, c :: m. (a `f` b) `f` c = a `f` (b `f` c)

It still needs to be investigated whether it's worth including invariants in this definition.