Correctness of compiling polymorphism to dynamic typing

Kuen Bang Hou, Nick Benton, Robert Harper

Research output: Contribution to journalArticle

Abstract

The connection between polymorphic and dynamic typing was originally considered by Curry et al. (1972, Combinatory Logic, vol. ii) in the form of "polymorphic type assignment" for untyped λ-terms. Types are assigned after the fact to what is, in modern terminology, a dynamic language. Interest in type assignment was revitalized by the proposals of Bracha et al. (1998, OOPSLA) and Bank et al. (1997, POPL) to enrich Java with polymorphism (generics), which in turn sparked the development of other languages, such as Scala, with similar combinations of features. In such a setting, where the target language already has a monomorphic type system, it is desirable to compile polymorphism to dynamic typing in such a way that as much static typing as possible is preserved, relying on dynamics only insofar as genericity is actually required. The basic approach is to compile polymorphism using embeddings from each type into a universal "top" type, ID, and partial projections that go in the other direction. This scheme is intuitively reasonable, and, indeed, has been used in practice many times. Proving its correctness, however, is non-trivial. This paper studies the compilation of System F to an extension of Moggi's computational meta-language with a dynamic type and shows how the compilation may be proved correct using a logical relation.

Original languageEnglish (US)
Article numbere1
JournalJournal of Functional Programming
Volume27
DOIs
StatePublished - Jan 1 2017
Externally publishedYes

Fingerprint Dive into the research topics of 'Correctness of compiling polymorphism to dynamic typing'. Together they form a unique fingerprint.

  • Cite this