Using the HetMet Extensions

The extremely brief tutorial below glosses over nearly all of the important theoretical issues; it is just a crash course.

First, add -XModalTypes to your compiler flags; this will automatically turn on the following flags as well: -XExplicitForall, -XRankNTypes, and -XNoMonomorphismRestriction.

Code Expressions

To produce a code expression, simply wrap the expression with code brackets:

Modal Types

The types of these code terms are modal (specifically, type-variable-indexed non-normal modal types: Axiom K and detachment hold, but necessitation does not. The Kripke frames are finitely-branching trees where each world is a node of the tree and is accessible from its immediate ancestor only).

Notice the extra type variable in the second example; we'll come back to that later. The notation <[t]>@c is meant to be the ascii version of ⃞_c t – the use of a “surroundfix” operator rather than a prefix operator minimizes the need for parentheses.

Escaping Code

To paste one piece of code into another, use the escape (~~) operator:

Note that the escape operator ~~ binds more strongly than any other operator; there is also a version ~~$ which binds more weakly than any other. For example, the following two expressions are equivalent and all of the parentheses in the second example are necessary:

An Example

Finally, here is a serious example, ye olde pow function:

More Examples

There is a two-stage regular expression matcher which was transcribed from this paper by Nanevski+Pfenning. Note that the example in the paper is for a modal dialect of ML (which was, to my knowledge, never implemented in any compiler) rather than Haskell. The transcribed version works using -XModalTypes – GHC infers the correct type and correctly rejects small modifications that make it ill-typed.

Environment Classifiers

Observe that the box operator on types is indexed by a type variable. In homogeneous metaprogramming this variable is called an environment classifier; it plays this role in heterogeneous metaprograms as well, but has an additional interpretation which is perhaps easier to understand: think of it as a “code flavor”.

Imagine you might be writing a Haskell program which manipulates guest programs in many different languages (say, Verilog and SQL). If you paste one chunk of code into another, or two chunks of code into a third chunk, all the chunks in question must belong to the “same language”. So you can think of this type variable as tracking which code chunks must come from the same language.

The “environment classifier” role is very similar to the role played by the extra type parameter of the ST monad. Note that you can only “run” an ST monad when it is closed – that is, when it has rank-2 type universally quantified over all possible indices.

rendered from WIX