Wed Mar 10 13:11:45 CET 2010

Closing the Stage

Typed compilation[1] and tagless representations (as GADTs or
modules/typeclasses).  The idea is that type checking is a stage, i.e.:

  "To type-compile an untyped term to a higher-order abstract syntax,
  we need staging, or its emulation."

I ran into this before in disguise.  The step is to go from something
``dumb data'' to something with a binding structure and holes in it,
i.e. code.

The paper[2] essentially models MetaOCaml inside System F.  So I
wonder, does this mean it can also be embedded in Haskell?

It also cites "SPIRAL, code generation for DSP platforms[3]" and
"HUME, a domain specific language for real-time embedded systems[4]".

[1] http://lambda-the-ultimate.org/node/2575
[2] http://okmij.org/ftp/Computation/staging/metafx.pdf
[3] http://citeseerx.ist.psu.edu/viewdoc/download?doi=
[4] http://citeseerx.ist.psu.edu/viewdoc/download?doi=