Correctness of compiling polymorphism to dynamic typing

Kuen Bang Hou, Nick Benton, Robert Harper

Research output: Contribution to journalArticlepeer-review

2 Scopus citations


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
StatePublished - 2017
Externally publishedYes

Bibliographical note

Funding Information:
This research is sponsored in part by the National Science Foundation under Grant Number 1116703. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.

Publisher Copyright:
Copyright © Cambridge University Press 2016.


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

Cite this