HetMet FAQIsn't this the same thing as Template Haskell?No. Template Haskell is strictly for compile time metaprogramming (it even says so in the GHC Manual). The functionality offered by this patch is strictly for run time metaprogramming. Okay, but couldn't you have integrated this with Template Haskell?The similarities are only superficial. Even taking into consideration the new GHC7 “morestronglytyped” Template Haskell brackets, the needs of the two systems are radically different:
At the end of the day, Template Haskell is a macro processor (or rather, what macro processors ought to be). This means that it needs more flexibility (like handling untyped and illtyped syntax trees) and fewer typesystemenforcedguarantees than a system for runtime heterogeneous metaprogramming. What is a Generalized Arrow?Here's what the type class looks like:
class Category g => GArrow g (**) u where
id :: g x x comp :: g x y > g y z > g x z ga_first :: g x y > g (x ** z) (y ** z) ga_second :: g x y > g (z ** x) (z ** y) ga_cancell :: g (u**x) x ga_cancelr :: g (x**u) x ga_uncancell :: g x (u**x) ga_uncancelr :: g x (x**u) ga_assoc :: g ((x**y)**z) (x**(y**z)) ga_unassoc :: g (x**(y**z)) ((x**y)**z) The following methods are provided by useful subclasses of GArrow; they account for languages with weakening, exchange, contraction, and recursion:
class GArrow g (**) u => GArrowDrop g (**) u where
ga_drop :: g x u class GArrow g (**) u => GArrowCopy g (**) u where ga_copy :: g x (x**x) class GArrow g (**) u => GArrowSwap g (**) u where ga_swap :: g (x**y) (y**x) class GArrow g (**) u => GArrowLoop g (**) u where ga_loop :: g (x**z) (y**z) > g x y The above five type classes are the only ones which are known to the compiler and given special status. Typically one will write guest programs which are polymorphic in g but have x and y concretely instantiated. Such guest programs may then be “flattened onto” any generalized arrow implementation by instantiating their g type variable and invoking flatten. Eventually the goal is to give more precise types (i.e. assuming g belongs to fewer than all five type classes) to terms which do not use recursion, reorder variables, duplicate values, or ignore variables. This will require a rudimentary form of substructural type inference. What is heteogeneous metaprogramming useful for?Here are a few example applications:
What Limitations Are There in the current implementation?The flattener cannot currently handle the following constructs *inside* codebrackets: typelambda, typelet, coercionlambda, coercionapplication, casediscrimination. Inside code brackets you basically get PCF and not much more. The ability to casebranch on Either and (,) will probably be arriving shortly, though inductive types beyond that are a much bigger challenge. Any expression sent through the flattener (or fcoqpass in general) will have many of its coercions replaced with mkUnsafeCoercion. This is a temporary limitation. System FC has only two kinds: * and k>k. GHC Core has many additional kinds. All of these additional kinds get mapped to * within the Coq code. This too is a temporary limitation. The flattener cannot handle the magic type GHC.Prim.Any. To ensure that GHC gets rid of this type before the flattener is invoked, you may need to add XNoMonoPatBinds. It is not entirely clear why this is necessary. On what theory is this based?Haskell is based on an extension of System F; GHC in particular is based on System FC. This patch extends GHC to include support for TahaNielsen Environment Classifiers, yielding a compiler based on the union of System FC and the TahaNielsen system λ^{α}, with a few minor changes (see the FAQ for details). Only the renamer and typechecker passes support multilevel terms; none of the compiler passes after the desugarer support multilevel terms. Therefore, the desugarer (or the very first CoretoCore pass) must eliminate all multilevel terms. The Coq code above does this by exploiting the fact that multilevel languages are generalized arrows – though multilevel syntax is friendlier to program writers, whereas generalized arrows are friendlier to language implementors. You can find a significantly outdated paper describing the theory behind this translation here. Please keep in mind that it is no longer up to date, and the current implementation diverges from it significantly. I'm working on an updated paper. Do variable scoping rules change?
Identifiers appearing at different syntactic depths are distinct; In other words, this expression is invalid because the occurrence of variable x is not bound:
\x > <[ x ]>
Likewise, in this expression the occurrence of x in a nonbinding position is bound to the first occurrence of x:
<[ \x > ~~( \x > <[ x ]> ) ]>
In homogeneous metaprogramming, use of a variable at a different syntactic depth is sometimes take to be an implicit use of crossstage persistence (so \x > <[ x ]> would be interpreted as \x > <[ %%x ]>). In heterogeneous metaprogramming crossstage persistence is often not supported, so having a common namespace for all syntactic depths is less compelling. Furthermore, a single identifier may need to have a different type at different syntactic depths. Even if we were to substitute implicit escape for implicit crossstage persistence, a term like this:
<[ \x y > x + y ]>
is really
<[ \x y > ~~(+) x y ]>
which will only be well typed if
(+) :: <[ a > b > c ]>
for some a, b, and c. Unfortunately this type is not an instance of the type given for (+) in the Haskell Prelude (or even the Numeric Prelude), and it would require a major contortion of the prelude to make both this and Int>Int>Int be instantiations of some common type. For this reason, we treat each layer of code brackets as a separate namespace, giving us:
<[(+)]> :: Num a => <[ a > a > a ]>
(+) :: Num a => a > a > a What Type System is Used?To be explicit, the resulting type system arises from taking System FC and adding the rules for (monomorphic) λ^{α}, with the following adjustments:
The Coq Extraction Fails to CompileSee the note on this page; the current Coq release needs some patches.
