article · KiltHub Repository · 2018

Correctness of Compiling Polymorphism to Dynamic Typing

Hou, Kuen-Bang, Benton, Nick, Harper, Robert

Cited by 0Open access

Abstract

The connection between polymorphic and dynamic typing was originally considered by Curry, et al. 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. and Bank, et al. to enrich Java with polymorphism (generics), which in turn sparked the development of other languages, such as Scala, with similar combinations of features. In that setting 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, dyn, 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 metalanguage with a dynamic type and shows how the compilation may be proved correct using a logical relation.

Cite this paper

APA 7

Hou, K.-B., Benton, N., & Harper, R. (2018). Correctness of Compiling Polymorphism to Dynamic Typing. KiltHub Repository. https://doi.org/10.1184/r1/6604526

MLA 9

Hou, Kuen-Bang, et al. “Correctness of Compiling Polymorphism to Dynamic Typing.” KiltHub Repository, 2018, https://doi.org/10.1184/r1/6604526.

Chicago

Hou, Kuen-Bang, Nick Benton, and Robert Harper. 2018. “Correctness of Compiling Polymorphism to Dynamic Typing.” KiltHub Repository. https://doi.org/10.1184/r1/6604526.

Harvard

Hou, K.-B., Benton, N. and Harper, R. (2018) ‘Correctness of Compiling Polymorphism to Dynamic Typing’, KiltHub Repository. Available at: https://doi.org/10.1184/r1/6604526.

BibTeX

@article{hou2018correctness,
  title = {{Correctness of Compiling Polymorphism to Dynamic Typing}},
  author = {Hou, Kuen-Bang and Benton, Nick and Harper, Robert},
  journal = {KiltHub Repository},
  year = {2018},
  doi = {10.1184/r1/6604526}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.