HetMet FAQ

Isn'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 “more-strongly-typed” Template Haskell brackets, the needs of the two systems are radically different:

  • Template Haskell is homogeneous: you're using Haskell to generate Haskell code. Removing the assumption of homogeneity would make Template Haskell much more complicated to use and implement – although it would be quite an interesting tool: sort of like a “strongly typed m4”. Unfortunately such a beast probably wouldn't look much like Template Haskell anymore.

  • Because this patch enables run-time metaprogramming, it is crucial that the type system rule out the possibility of ill-formed code (“template”) operations, since those operations will be performed at runtime. By contrast, ill-formed Template Haskell operations cannot result in run-time errors because all Template Haskell expressions are executed at compile time.

  • Important special case of the previous point: Template Haskell has no notion of “executing” code. Because of this, it has no need for a type system which is capable of distinguishing closed code from open code. This patch's use Taha-Nielsen environment classifiers to make that distinction accounts for the vast bulk of its complexity (and restrictions imposed on users), and it is doubtful that the Template Haskell folks are anxious to take on that burden.

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 ill-typed syntax trees) and fewer type-system-enforced-guarantees than a system for run-time 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:

  • Invertible programming: many Haskell functions are not invertible (i.e. \(x,y) -> x) so an invertible guest language cannot support promotion of arbitrary Haskell functions.

  • Digital circuit design: arbitrary Haskell terms cannot be turned into reasonable hardware (i.e. unbounded-depth recursion, heap allocation, and more); using generalized arrows instead of Haskell Arrows avoids problems with higher-order functions “leaking” into circuits. Multi-level syntax gives ease-of-use comparable to the observable-sharing version of Lava without changing Haskell's operational semantics.

  • Stream processing of trees: not all tree transformations admit a constant-space, single-pass implementation (more details).

  • Distributed Memory Data Parallelism: if the functionals supplied to parallel maps and fold have unrestricted access to the heap, some form of shared memory will be required on the execution platform. This can become an impediment to scalability. Heterogeneous metaprogramming lets one strike a balance between NESL (which required the entire program be written in a special-purpose language) and Nepal/DPH (which allow unrestricted use of Haskell, but cannot be implemented efficiently without shared memory) by constraining only those functions which eventually become involved in parallelized operations.

What Limitations Are There in the current implementation?

The flattener cannot currently handle the following constructs *inside* code-brackets: type-lambda, type-let, coercion-lambda, coercion-application, case-discrimination. Inside code brackets you basically get PCF and not much more. The ability to case-branch 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 Taha-Nielsen Environment Classifiers, yielding a compiler based on the union of System FC and the Taha-Nielsen system λα, with a few minor changes (see the FAQ for details).

Only the renamer and typechecker passes support multi-level terms; none of the compiler passes after the desugarer support multi-level terms. Therefore, the desugarer (or the very first Core-to-Core pass) must eliminate all multi-level terms. The Coq code above does this by exploiting the fact that multi-level languages are generalized arrows – though multi-level 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?

Alert! This is the most experimental part of the HetMet extensions, and the most likely to confuse people. To summarize in one sentence: the syntactical depth of a subterm is the number of enclosing brackets minus the number of enclosing escapes; identifiers with different syntactical depths are distinct identifiers. This may lead to some initially-confusing “not in scope” errors.

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 non-binding 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 cross-stage persistence (so \x -> <[ x ]> would be interpreted as \x -> <[ %%x ]>). In heterogeneous metaprogramming cross-stage 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 cross-stage 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:

  • Syntax: the type of code yielding a value of type t in environment a is written <[t]>@a (rather than <t>a); escape is ~~e, csp is %%e, and code brackets are <[e]>.

  • Environment classifiers of λα become type variables of System FC (in a future revision these variables will be subject to the additional constraint that they be a member of the “magic” type class GHC.HetMet.CodeTypeIndex).

  • System FC's type abstraction is used for environment classifier abstraction, so the special-purpose classifier abstractions (α)t and (α)e of λα is no longer necessary. Likewise for environment classifier application t[α].

  • In λα, code expressions are annotated with their environment classifier; to achieve this effect in GHC, use an explicit type ascription:

    f = (<[ e ]> :: <[t]>@a)

    If the ascription is omitted, GHC will synthesize a fresh type variable for each set of brackets (and then – as with all Haskell terms – compute the most general unifier for all of the synthesized variables). Unlike ML-Like Inference for Classifiers, the option of giving the classifier explicitly is retained and there are no special open/close terms – GHC's higher-rank polymorphic type inference engine is used instead, and any improvements to that inference engine are inherited automatically.

  • The operation run no longer needs to be a distinguished term, since in System FC it can be given the type forall a. (forall c. <[a]>@c) -> a.

  • Identifiers appearing at different syntactic depths are distinct; see the previous FAQ.

The Coq Extraction Fails to Compile

See the note on this page; the current Coq release needs some patches.



rendered from WIX