ML-like Inference for Classifiers Seminars/Workshops

Abstract

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. However, inference for the full classifier-based system fails. We 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.