Klister custom type systems

[gelisam]

I think we should think about and document more explicitly what kind of type system extensions can be implemented in Klister.

For example, once we implement syntax parameters, I think we can claim that Klister supports custom typing rules involving multiple contexts. Each context is a syntax parameter. Every existing rule is automatically extended to pass it on unchanged, for example

Gamma, x:A |- e : B
-----
Gamma |- (lambda (x) e) : (-> A B)

becomes

Delta; Gamma, x:A |- e : Be
-----
Delta; Gamma |- (lambda (x) e) : (-> A B)

The rules which care about that extra context are implemented as macros which look at this syntax pattern and set this parameter locally around the sub-terms. For example,

Delta; Gamma |- e1 : (Box A)
Delta, x:A; Gamma |- e2 : B
-----
Delta; Gamma |- (let-box [x e1] e2) : B

Can be implemented by a let-box macro which expands to

(let [tmp1 e1]
  (case tmp1
    [(mk-box tmp2)
     (syntax-parameterize
       [Delta
        (cons
          (pair 'x tmp2)
          (syntax-parameter-value Delta))]
       e2)]))

Note that this technically implements the rule

Delta; Gamma |- e1 : (Box A)
Delta, x:A; Gamma, tmp1:(Box A), tmp2:Syntax |- e2 : B
-----
Delta; Gamma |- (let-box [x e1] e2) : B

But since tmp1 and tmp2 are invisible to e2, they can be ignored.

This is a good start, especially since the context can have any shape, it is not restricted to be a map from symbol to type. If we allow overriding #%identifier, a #lang would even be able to hide Gamma from the user and to use Delta exclusively, which would make it possible to implement e.g. the linear lambda calculus.

Next, type formers. Above, the Box modality is implemented via a newtype wrapper around the runtime representation, Syntax. The data constructor is not exposed outside of the implementation of the #lang and its type system, so this implementation detail is invisible to the user. Box even shows up in error messages and participates in unification. This is good, but there are a few limitations:

1. Box's argument must be a Type, it can't be e.g. an integer (if we want to implement quantitative type theory) or a list (if we want to implement contextual modal type theory).
2. The unification algorithm is hard-coded, but for e.g. quantitative type theory we would like to sum the numbers and for linear types we would like to use the maximum.
3. Let-generalization is also hard-coded, but for linear types we would like to default to 0 and for contextual type theory we would like to default to the empty list.

To address those limitations, we could allow indices other than Type as long as they provide a typeclass instance providing an implementation for unification and generalization. This also implies that typeclasses should be built-in after all.

Next, some judgments produce a context instead of consuming it, e.g. pattern-matching. I think this would be better served by a custom problem than a custom type. Still, it should be possible to use a custom type which is indexed by a type and a context.

Type systems are very varied, so I'm sure there are some type systems which cannot be implemented by the features above. But it seems sufficient for most purposes, I think?