|
Cristiano Calcagno, Eugenio Moggi, and Walid Taha.
Environment classifiers were recently proposed as a new approach to typing
multistage languages. Safety was established in the simplytyped and letpolymorphic set
tings. While the motivation for the classifier approach was the feasibility of inference, this
was in fact not established. This paper starts with the observation that inference for the full
classifierbased system fails. We then identify a subset of the original system for which infer
ence is possible. This subset, which uses implicit classifiers, retains significant expressivity
(e.g. it can embed the calculi of Davies and Pfenning) and eliminates the need for classifier
names in terms. Implicit classifiers were implemented in MetaOCaml, and no changes were
needed to make an existing test suite acceptable by the new type checker.
Staging, which was discussed here quite a few times in the past, is an essential ingredient of macros, partial evaluation, and runtime code generation. From a programmer's perspective it seems like no more than a simple extension of regular macro facilities.
In the untyped setting, the behavior of staging constructs is indeed mostly straighforward and resembles the quasiquotation mechanisms of LISP and Scheme. In the statically typed
setting, however, such quotation mechanisms may prohibit static typechecking.
This paper explores this issue, and presents some promising design approaches.
Posted to theory by Ehud Lamm on 1/7/04; 12:29:35 PM
|
|
ML-like Inference for Classifiers
