Typed metaprogramming languages [closed]

Question

I want to do some metaprogramming in a statically typed language, where both my programs and my meta-programs will be typed. I mean this in a strong sense: if my program generator compiles, I want the type system to be strong enough that only type-correct programs can be generated.

As far as I know, only metaocaml can do this. (No, neither Template Haskell nor C++ templates fit the bill -- see this paper). Question: what other languages/systems allow this?

EDIT: As far as I can tell, metaocaml is dead. Oleg tried to resurrect it, but that is still stuck several versions behind OCaml itself. If one wants to go with experimental languages (i.e. even more so than metaocaml, it seems that Ur and quite possibly Idris fit the bill. Any other new entries to the field?

Answer 1

F# can do this too through Code Quotations.

Answer 2

To do that, you have to ensure that the type system of the underlying languge is directly honored/checked by the metaprogram itself. As a practical matter, this almost forces the metaprogramming to be in the underlying language... so I guess I'm not suprised that you might be able to do this in metaocaml.

Most of us don't get metaprogramming tools built into the underlying language (C++ being rather an exception, and I reject it and reflection based systems as being too weak to carry out arbitrary transformations).

A system that can carry out arbitrary transformations (or metaprograms composed of sets of those) on code is the DMS Software Reengineering Toolkit. DMS has front ends for many real langauges, builds compiler data structures when parsing (including ASTs). DMS provides source-to-source program transformations that represent transformations as AST-rewrites using the surface syntax of the target language. It meets your requirement to a certain degree: if your transformation rules are syntactically correct (and they are checked by DMS), then the transformed program will be syntactically correct. It does not achieve your type-correctness requirement, as the type-checking mechanisms are implemented outside the target language. In principal, one could a type-safe checker to augment the program transformations; in practice, we've found that we can code transformations reliably enough.

And even if you have type-safe transformations, you don't have a guarantee of semantic safety with respect to your original program. So, you'll still have to debug the metaprograms.

Answer 3

http://en.wikipedia.org/wiki/Nemerle

Answer 4

Compile-time metaprogramming in Scala.

Our flavor of macros is reminiscent of Lisp macros, adapted to incorporate type safety and rich syntax. Unlike infamous C/C++ preprocessor macros, Scala macros: 1) are written in full-fledged Scala, 2) work with expression trees, not with raw strings, 3) cannot change syntax of Scala.

Answer 5

Shen (Qi Lisp II) supposedly can/will: http://groups.google.com/group/qilang/browse_thread/thread/d62fc0d9f576838c