``more powerful'' meaning that it can do some level of introspection, right? I know introspection can be very powerful (I designed Maple's modern reflection and reification facilities...), but I was under the impression that type systems that can handle 'too much' introspection were unsound [a result of Walid Taha].On Wed, 2005-05-04 at 18:29 -0400, Jacques Carette wrote:There is also Template Haskell vs MetaOCaml. For the life of me, I still cannot fathom why Template Haskell is untyped, while MetaOCaml is fully typed. Which is the main reason I write meta-program in MetaOCaml and 'other' programs in Haskell.The reason for this is that Template Haskell is more powerful and correspondingly harder to type so it is currently untyped.
Can't this be regarded as a 'convenience' rather than as actual extra power? Using an abstract interpretation formalism (see papers of Taha and co-authors), it is possible to 'lift' the type of code values into staging-time terms, and pattern-match on that instead. Then well-typedness of transformations is much easier to show. In this way one can even implement some transformations that are equivalent to what are currently 'hints' to GHC as well-typed code [I have some code that does this, but there are only hints of this in a preprint of mine -- see the conclusion section of "Gaussian Elimination: a case study in efficient genericity with MetaOCaml" available from http://www.cas.mcmaster.ca/~carette/publications.html for some hints on how this is doneThe main reason it is more porwerful is that TH allows you to pattern match on the abstract syntax of a quoted expression and perform arbitrary transformations on that. It would be hard to preserve the well-typedness of the AST and still allow arbitrary transformations.
I am eagerly awaiting this! Writing Monadic meta-programs in MetaOCaml is feasible, but the lack of native support for Monads makes it significantly harder. But after spending 12 years writing programs in a fully dynamically typed language (Maple), I am much happier writing all parts of my programs in a strongly typed language!A colleague of mine is currently developing a type system for Template Haskell that should catch most errors without restricting too much the programs you can write.