explain the limits of the type system

[gelisam]

I no longer like this part of our README:

The variety of type-systems which can be implemented this way is unforunately limited by the core type system to which everything must be rewritten.

because it is not at all clear how big of a limitation this is. I think it would be helpful to list some examples of type systems which can be implemented in Klister and some examples which can't. And of course, for those which can be implemented, it would be nice to eventually implement it and link to that implementation.

[gelisam]

So far, the only example of a custom type system we have is Scala-style implicit conversions.

Other fancy type systems which come to mind are:

• linear types: maybe we can use a type-driven macro to determine which variables need to only occur once, and then have that macro traverse the body to verify that the identifier only occurs once?
• session types. we don't have threads, but maybe we can still check that a do block performs actions in the correct order?
• modal type theory: the big feature is a (Box Integer), meaning an expression of type Integer which does not capture any of the surrounding variables. I think Klister should be able to handle that by messing with the scope-sets of those variables.
• contextual modal type theory: the big feature is (Box [(x Integer)] Integer), meaning an expression which does not capture any of the surrounding variables but does have access to a variable x of type Integer. Introducing that x via a lambda or something seems easy enough, but our types are not expressive enough to store symbols, currently they can only store other types and type constructors.