Using the HetMet ExtensionsThe 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 ExpressionsTo produce a code expression, simply wrap the expression with code brackets:
<[ \x y > x ]>
Modal TypesThe types of these code terms are modal (specifically, typevariableindexed nonnormal modal types: Axiom K and detachment hold, but necessitation does not. The Kripke frames are finitelybranching trees where each world is a node of the tree and is accessible from its immediate ancestor only).
fst :: forall a b. a > b > a
fst = \x y > x fst' :: forall c a b. <[a > b > a]>@c fst' = <[ \x y > x ]> 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 CodeTo paste one piece of code into another, use the escape (~~) operator:
 sort of a boring example...
let fst = <[ \x y > x ]> in example = <[ \x y z > ~~fst y x ]> 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:
<[ ~~foo ~~$ bar baz ]>
<[ (~~$foo) ~~( bar baz) ]> An ExampleFinally, here is a serious example, ye olde pow function:
import GHC.HetMet.GArrow
pow :: forall a. Int > <[ Int > Int ]>@a pow n = if n==0 then <[ \x > 1 ]> else <[ \x > x * ~~(pow $ n1) x ]> More ExamplesThere is a twostage 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 illtyped. Environment ClassifiersObserve 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 rank2 type universally quantified over all possible indices.
