|Version 1 (modified by 4 years ago) (diff),|
Add MetaML-style quotes
In the case of terms (only), we know from MetaML that we can have typed quotations. These are rather useful as the metaocaml exploration of the Shonan Challenge report and code (amongst others) shows. Right now, however, all this work is done in (the recently reborn) metaocaml rather than in (Template) Haskell because of the availability of typed quotes and splices for increased correctness.
- Add a new abstract type of typed expressions TExp a
- Add a new term quotation form
[|| e ||], called a typed quote; the type of the quote is
TExp ty, where
tyis the type of
e. In the type-system jargon, this is the "introduction form" for
- Add a new splice form
$$e, called a typed splice. The term
emust have type
TExp ty, and the splice
$$ethen has type ty. This is the "elimination form" for
- Add a constant which takes a typed quote and returns an untyped one:
unType :: TExp a -> Q Exp
- Run these new typed splices in the typechecker, not the renamer.
- Use renaming of binding forms to insure capture-avoidance (a la MetaML).
- Cross-stage persistence will remain unchanged. To be able to use an identifier at future stages, it must be fully available, which means that it needs to be defined in a previous compilation unit if it will be spliced (by name) into a term.
The justification for 2 and 3 are classical. For ensuring type-safety (at the current state of knowledge), it is important that
TExp be abstract, as sound typed-expression manipulation is very hard to achieve, especially in the presence of binders. A future extension may open this up, whenever this particular tough nut is cracked, but for now we must have 1. In theory,
unType (4) is not needed; in practice, it probably will be. 5 is obvious: type information needs to be available for typed splices, and this is not available in the renamer. 6 comes from MetaML, and basically just means that the renamer will be applied to typed splices as well. 7 documents a non-change [which is a little awkward in code, was not present in the old metaocaml, but is actually in the new metaocaml).