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).
- Typed metaprogramming:
* Type systems proper: Hindley-Milner (just complex enough to
make inference work) up to the "lambda cube" which contains
systems that can only be checked. Main benefit: prove things
* Type level computations in Haskell using functional dependencies
in type classes. Benefit: allow limited form of computation
without getting into undecidedness.
* MetaOCaml: 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).