Mon Aug 8 10:44:12 CEST 2011

Type-level computations / meta systems

Metaprogramming.  I've seen it now from many sides, and it is
fascinating how they are all subtly different but still quite similar.
From logics that say something "about" code, to macro systems that
generate code, either providing types (MetaOCaml) or not

The main "force" seems to be the tension between simple logic systems
that can be reasoned about, and full-blown programming systems that
are limited in analysis by the halting problem (undecidability[3]).

- Typed metaprogramming:

  * Type systems proper: Hindley-Milner[4] (just complex enough to
    make inference work) up to the "lambda cube"[2] which contains
    systems that can only be checked.  Main benefit: prove things
    about programs.

  * Type level computations in Haskell using functional dependencies
    in type classes[1].  Benefit: allow limited form of computation
    without getting into undecidedness.

  * MetaOCaml[5]: proper multi-stage code generation in a typed setting.

- Untyped metaprogramming:

  * Scheme's hygienic macros: generating code programmatically
    respecting binding structure.

  * Typed scheme & macros.  Similar to MetaOCaml but approaching the
    problem from the untyped->typed side.  (find some links).

[1] http://hackage.haskell.org/package/type-level
[2] http://en.wikipedia.org/wiki/Lambda_cube
[3] http://en.wikipedia.org/wiki/Undecidable_problem
[4] http://en.wikipedia.org/wiki/Type_inference
[5] http://www.metaocaml.org/