Lambda the Ultimate

inactiveTopic ML-like Inference for Classifiers
started 1/7/2004; 12:21:49 PM - last post 1/7/2004; 12:21:49 PM
Ehud Lamm - ML-like Inference for Classifiers  blueArrow
1/7/2004; 12:21:49 PM (reads: 7727, responses: 0)
ML-like Inference for Classifiers
Cristiano Calcagno, Eugenio Moggi, and Walid Taha.

Environment classifiers were recently proposed as a new approach to typing multi­stage languages. Safety was established in the simply­typed and let­polymorphic 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 classifier­based 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 run­time 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 quasi­quotation mechanisms of LISP and Scheme. In the statically­ typed setting, however, such quotation mechanisms may prohibit static type­checking.

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