Over the past several weeks I have implemented most of Simon Peyton Jones’ proposal for a major revision to Template Haskell. This brings several new features to Template Haskell, including:
- Typed Template Haskell brackets and splices.
- Pattern splices and local declaration splices.
- The ability to add (and use) new top-level declarations from within top-level splices.
I will concentrate on the first new feature because it allows us to generate and
compile Haskell values at run-time without sacrificing type safety. The code in
this post is available on github; the
github repository README contains instructions for building the
of GHC, which is where work on typed Template Haskell is being done. The GHC
wiki contains more details about the current implementation
plan is that this work will land in
HEAD before the 7.8 release of GHC.
The staged power function: untyped
The driving example I will use is the staged power function. The idea is that we want to compute $x^n$ where $n$ is known statically (that is, it is a constant we know ahead of time), but $x$ may vary. John Lato wrote a blog post, Runtime Meta-programming in Haskell, that shows how to implement the staged power function while providing a veneer of type-safety on top of unsafe runtime code generation using “classic” Template Haskell. Examining his implementation is instructive, so I’ll start there.
John’s “safe” Template Haskell expression type is a
newtype wrapper around the
Template Haskell expression type,
ExpQ, that adds a phantom type parameter.
This definition means that for all $\alpha$, we can construct a
ExpQ by applying the constructor
Meta. For example
Not very safe! However, using the
Meta type, we can write combinators that
are safe in the sense that if their inputs are “well-typed”
then their outputs will be “well-typed”
Meta values. John defines one such
safe combinator as follows
compose function uses unsafe operations internally, if its two
arguments really are Meta-wrapped Template Haskell expressions with the types
-> b and
b -> c, respectively, then the result really will be a Meta-wrapped
Template Haskell expression of type
a -> c. This isn’t enforced by the type
system, but it’s true nonetheless.
John defines the staged power function as follows
Again, the type system doesn’t enforce safety in the sense that it doesn’t
guarantee that the bit of Template Haskell that
mkPow produces really has type
Int -> Int, but we can see by inspection that it will always return a Template
Haskell expression that has type
Int -> Int. With classic Template Haskell,
this is just about all that we can hope for.
The staged power function: typed
With the new version of Template Haskell, we can do better. Here is the
compose using the new Template Haskell typed brackets and typed
splices (I have also changed the definition of
compose so that the arguments
are in the proper order :)).
We can see a new data type,
TExpQ a, and new syntax for splices and
TExpQ a is a type alias for
Q (TExp a), just as
ExpQ is an alias
Q Exp. A
TExp a is a typed Template Haskell expression—the type
checker guarantees that it is the abstract syntax representation of a Haskell
term of type
a. This is in contrast to
Exp, the existing untyped
expression representation used by Template Haskell. A value of type
Exp is the
abstract syntax of a Haskell expression of some type, but a value of type
TExp a is the abstract syntax of a Haskell expression of type
Values of type
TExp a can only be constructed using typed brackets and typed
splices. The syntax
[||e||] is a typed bracket, and the syntax
$$e is a
typed splice. No other varieties of splice may occur in a typed bracket. In
[||e||] is the only introduction form for
the elimination form. It not the only elimination form; Template Haskell also
provides a constant
unType :: TExp a -> Exp that allows coercion from the type
Template Haskell world to the untyped world; it simply throws away the type
We can now write a completely safe version of the
This version is type-checked by the compiler; there is no unsafe newtype wrapping/unwrapping going on.
Under the covers
If you look at the definition of
TExp in the
you’ll see that it actually is a newtype wrapper.
Why is this safe? Because the compiler is checking that a typed bracket is
well-typed and then creating a
TExp whose type index is that type. Of course
you can always subvert type safety by importing
mucking about with
TExp’s. But as long as you stick to typed brackets and
splices, you will get type safety.
Run time code generation and compilation
Now that we can generate type safe Haskell expressions at run time, can we also safely compile them at run time? The answer is a qualified yes.
First, how can we compile a
TExp a? John uses the plugins
package, originally written by Don
Stewart. I will use the GHC API directly. My implementation strategy is the same
as his: print a Template Haskell expression to a file and compile and load the
file. For this to work, we need two invariants to hold:
The term that we pretty-print must be a faithful representation of the term that was type checked.
The API that we use to compile the term we print out must assign it the same type that GHC did when it checked the term.
You might think that pretty-printing is safe, but in fact I had to fix a few bugs that caused the pretty-printed versions of some Template Haskell terms to not even parse as valid Haskell! I assume that the underlying expression value is a faithful representation of the term that GHC type checked.
The second property does not obviously hold. First of all, we need to make sure (approximately) that the type environment we use to compile the term is the same as the type environment used to type check it. Template Haskell resolves some names so that they are fully qualified. Perhaps we could walk over the term to figure out exactly which modules we need to import to compile the term, but I’m not sure that is sufficient. At the moment I’ve punted, so run time compilation may fail at run time. See the github repository for the details. Furthermore, even if we got all the imports right, defaulting and such might conceivably get in the way, so we slap a type signature on out term when we print it out to make sure the type of out compiled term really matches the type of the typed bracket.
Given the function
compile :: forall a . Typeable a => TExp a -> IO a, which
is defined in the github repository accompanying this post, we can now compile
and run our staged power function. Note that the
Typeable constraint is what
allows us to print out the type of the term when we feed it to the GHC API.
Typed brackets bring much of the power of MetaML1 to Haskell. They are
also similar to F#’s code quotations2; however, Haskell’s untyped
brackets are now completely untyped—the type checker doesn’t check them at
all. In classic Template Haskell, the compiler attempted to type check all
varieties of bracket, but an expression bracket still resulted in a plain old
ExpQ. F#’s untyped quotations are type checked, although their precise
semantics are unclear to me. I like the untyped/typed distinction that is now
made by the new Template Haskell; typed brackets really are typed, and untyped
brackets are only parsed, never type checked.
Typed Template Haskell is quite different from MetaHaskell3, which provides a mechanism for quoting many different object languages while maintaining type safety. MetaHaskell also supports quotation and antiquotation using open code, which introduces a host of difficulties.
W. Taha and T. Sheard, “Multi-stage programming with explicit annotations”, in Proceedings of the 1997 ACM SIGPLAN symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ‘97), Amsterdam, The Netherlands, 1997, pp. 203–217. ↩
G. Mainland, “Explicitly heterogeneous metaprogramming with MetaHaskell”, in Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP ‘12), Copenhagen, Denmark, 2012, pp. 311–322. ↩