C. Calcagno, E. Moggi, and W. Taha
ML-like inference for
classifiers
In Programming Languages & Systems, 13th European Symp. Programming, volume 2986 of Lecture Notes in Computer Science
Springer, 2004
Environment classifiers were recently proposed as a new approach to
typing multi-stage languages. Safety was established in the
simply-typed and let-polymorphic settings. 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 inference 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.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43