Hostname: page-component-cb9f654ff-9knnw Total loading time: 0 Render date: 2025-08-03T12:27:24.007Z Has data issue: false hasContentIssue false
  • English
  • Français

Correctness of compiling polymorphism to dynamic typing*

Published online by Cambridge University Press:  12 December 2016

KUEN-BANG HOU (Favonia) ,
NICK BENTON  and
ROBERT HARPER
KUEN-BANG HOU (Favonia)
Affiliation:
Carnegie Mellon University Pittsburgh, PA, USA (e-mail: favonia@cs.cmu.edu)
NICK BENTON
Affiliation:
Microsoft Research Cambridge, Cambridgeshire, United Kingdom (e-mail: nick@microsoft.com)
ROBERT HARPER
Affiliation:
Carnegie Mellon University Pittsburgh, PA, USA (e-mail: rwh@cs.cmu.edu)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

The connection between polymorphic and dynamic typing was originally consideredby 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 modernterminology, a dynamic language. Interest in type assignment was revitalized bythe proposals of Bracha et al. (1998, OOPSLA) and Banket al. (1997, POPL) to enrich Java with polymorphism(generics), which in turn sparked the development of other languages, such asScala, with similar combinations of features. In such a setting, where thetarget language already has a monomorphic type system, it is desirable tocompile polymorphism to dynamic typing in such a way that as much static typingas possible is preserved, relying on dynamics only insofar as genericity isactually required. The basic approach is to compile polymorphism usingembeddings from each type into a universal “top” type, ${\mathbb{D}}$ , and partial projections that go in theother direction. This scheme is intuitively reasonable, and, indeed, has beenused in practice many times. Proving its correctness, however, is non-trivial.This paper studies the compilation of System F to anextension of Moggi's computational meta-language with a dynamic type and showshow the compilation may be proved correct using a logical relation.

Information

Type
Theoretical Pearls
Information
Journal of Functional Programming , Volume 27 , 2017 , e1
Copyright
Copyright © Cambridge University Press 2016 

Footnotes

*

This research is sponsored in part by the National Science Foundationunder Grant Number 1116703. Any opinions, findings, and conclusions orrecommendations expressed in this material are those of the author(s)and do not necessarily reflect the views of the National ScienceFoundation.

References

Ahmed, A. (2006) Step-indexed syntactic logical relations for recursive and quantified types. In Programming Languages and Systems, Sestoft, Peter (ed), Lecture Notes in Computer Science, vol. 3924. Berlin, Heidelberg: Springer, pp. 69–83.Google Scholar
Ahmed, A., Findler, R. B., Siek, J. G. & Wadler, P. (2011) Blame for all. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). New York, NY, USA: ACM, pp. 201–214.CrossRefGoogle Scholar
Amadio, R. (1993) On the adequacy of PER models. In Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science (MFCS). LNCS, vol. 711. Berlin, Heidelberg: Springer, pp. 222–231.Google Scholar
Appel, A. W. & McAllester, D. (2001) An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23 (5), 657–683.Google Scholar
Bank, J. A., Myers, A. C. & Liskov, B. (1997) Parameterized types for Java. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). New York, NY, USA: ACM, pp. 132–145.CrossRefGoogle Scholar
Benton, N. (2005) Embedded interpreters. J. Funct. Program. 15 (4), 503–542.CrossRefGoogle Scholar
Benton, N. & Hur, C.-K. (2010) Realizability and Compositional Compiler Correctness for a Polymorphic Language. Technical Report, MSR-TR-2010-62. Microsoft Research.Google Scholar
Bracha, G., Odersky, M., Stoutamire, D. & Wadler, P. (1998) Making the future safe for the past: adding genericity to the Java programming language. In Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA '98), vol. 33. New York, NY, USA: ACM, pp. 183–200.Google Scholar
Crary, K. & Harper, R. (2007) Syntactic logical relations for polymorphic and recursive types. Electron. Notes Theor. Comput. Sci. 172, 259–299.CrossRefGoogle Scholar
Curry, H. B., Hindley, J. R. & Seldin, J. P. (1972) Combinatory Logic, Volume ii. Studies in logic and the foundations of mathematics, vol. 65. North-Holland Publishing Company.Google Scholar
Findler, R. B. & Felleisen, M. (2002) Contracts for higher-order functions. In Proceedings of the International Conference on Functional Programming (ICFP). New York, NY, USA: ACM, pp. 48–59. doi = 10.1145/581478.581484.Google Scholar
Girard, J.-Y. (1972) Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. Ph.D. thesis, Université Paris 7.Google Scholar
Harper, R. (2012) Practical Foundations for Programming Languages. Cambridge University Press.Google Scholar
Hur, C.-K., & Dreyer, D. (2011) A Kripke logical relation between ML and assembly. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). New York, NY, USA: ACM, pp. 133–146.CrossRefGoogle Scholar
Igarashi, A., Pierce, B. C. & Wadler, P. (2001) Featherweight Java: A minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23 (3), 396–450.Google Scholar
McCracken, N. 1979 (June) An Investigation of a Programming Language with a Polymorphic Type Structure. Ph.D. thesis, Syracuse University.Google Scholar
Meyer, A. R., & Wand, M. (1985) Continuation semantics in typed lambda-calculi. In Logics of Programs, Rohit Parikh (ed), Lecture Notes in Computer Science, vol. 193. Berlin, Heidelberg: Springer, pp. 219–224.Google Scholar
Milner, R. (1978) A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17 (3), 348–374.CrossRefGoogle Scholar
Minamide, Y., Morrisett, G. & Harper, Rt. (1996) Typed closure conversion. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). New York, NY, USA: ACM, pp. 271–283.Google Scholar
Moggi, E. (1991) Notions of computation and monads. Inform. Comput. 93 (1), 55–92.CrossRefGoogle Scholar
Moors, A., Piessens, F. & Odersky, M. (2008) Generics of a higher kind. In Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications (OOPSLA). New York, NY, USA: ACM, pp. 423–438.Google Scholar
Pitts, A. M. (1996) Relational properties of domains. Inform. Comput. 127 (2), 66–90.Google Scholar
Plotkin, G. D. (1977) LCF considered as a programming language. Theor. Comput. Sci. 5 (3), 223–255.Google Scholar
Ramsey, N. (2011) Embedding an interpreted language using higher-order functions and types. J. Funct. Program. 21 (6), 585–615.Google Scholar
Reynolds, J. (1983) Types, abstraction and parametric polymorphism. InInformation Processing 83. IFIP Congress Series, vol. 9. North-Holland, pp. 513–523.Google Scholar
Reynolds, J. C. (1974) Towards a theory of type structure. In Programming Symposium, Proceedings Colloque sur la Programmation. Berlin, Heidelberg: Springer-Verlag, pp. 408–423.Google Scholar
Rossberg, A., Russo, C. V., & Dreyer, D. (2010) F-ing modules. In Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI). New York, NY, USA: ACM, pp. 89–102.Google Scholar
Scott, D. (1976) Data types as lattices. SIAM J. Comput. 5 (3), 522–587.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.