Sun Aug 23 12:16:37 CEST 2009

Tagless Interpreters

I am going to try to understand this[1].  It is about building a
``tagless staged definitional interpreter''.

It touches on some ideas that I've seen vague hints of writing the PF
and SC interpreters, and trying to see the tradeoffs in
compiling/interpreting LC-based languages.  First, some terminology:

Initial algebra[2]: ``In mathematics, an initial algebra is an initial
object in the category of F-algebras for a given endofunctor F. The
initiality provides a general framework for induction and recursion.''
It seems to be used related to recursive types, which are the yin of
a yang: recursive functions operating on the types.  I guess the
Coalgebraic[3][4] structure is those of recursive functions?

HOAS: higher order abstract syntax.

COGEN: code generator.

1.1 TAGS

The paper starts with explaining the use a universal type `u' (a
tagged union) to represent a dynamic type, to be able to write
something like:

         eval : u list -> exp -> u

Where `u list' is a DeBruyn environment (variables are then DeBruyn
indices).  The disadvantage is that in this representation, `eval' is
a partial function: i.e. it needs to handle cases where it is passed
invalid input, i.e. non-closed terms or ill-typed ones.  In practice
however, when a term is closed and well-typed these cases do not
occur.  Essentially, the algebraic types fail to express in the meta
language that an object expression is closed and well-typed.


Current approaches to solve this uses complex data types like GADTs or
dependent types.  The paper presents an approach that doesn't require
this, by representing object programs using ordinary functions instead
of data structures.  This approach turns evaluation of open object
terms into _ill-typed_ terms in the meta langauge.  Neat!


There is a link between this kind of representation and Staapl's Coma
abstraction: representing target code as procedures operating on a
stack machine code stack.

[1] http://okmij.org/ftp/tagless-final/APLAS.pdf
[2] http://en.wikipedia.org/wiki/Initial_algebra#Use_in_programming_theory
[3] http://en.wikipedia.org/wiki/Coalgebra
[4] http://en.wikipedia.org/wiki/F-coalgebra
[5] http://okmij.org/ftp/Computation/tagless-typed.html
[6] http://lambda-the-ultimate.org/node/2438