Abstract
A denotational semantics of simply typed lambda calculus with a basic type Dynamic, modelling values whose type is to be inspected at runtime, has been given by Abadi e.a.[1]. We extend this interpretation to cover (formally contractive) recursive types as well. Soundness of typing rules and freeness of run-time type errors for well-typed programs hold.
The interpretation works also for implicitly polymorphic languages like ML with Dynamic and recursive types, and for explicitly polymorphic languages under the types-as-ideals interpretation.
This work has been supported by the Esprit Working Group BRA 7232, GENTZEN.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in a statically-typed language. In 16th POPL, pages 213–227, 1989.
M. Abadi, L. Cardelli, B. Pierce, and D. Remy. Dynamic typing in polymorphic languages. In ACM SIGPLAN Workshop on ML and its Applications. San Francisco, California, June 20–21, 1992, pages 92–103, 1992.
L. Cardelli. Amber. In G. Cousineau, P. L. Curien, and B. Robinet, editors, Combinators and Functional Programming Languages. Springer LNCS 242, 1986.
F. Cardone and M. Coppo. Type inference with recursive types: Syntax and semantics. Information and Computation, 92(1):48–80, May 1991.
G. Cousineau and G. Huet. The CAML Primer. Version 2.6. Project Formel, INRIA-ENS, April 1989.
R. Harper, R. Milner, and M. Tofte. The definition on Standard ML — Version 2. LFCS Report Series ECS-LFCS-88-62, Dept. of Computer Science, Univ. of Edinburgh, 1988.
F. Henglein. Dynamic typing. In European Symposium on Programming (ESOP). Rennes, France, pages 233–253. Springer LNCS, vol. 582, 1992.
X. Leroy and M. Mauny. Dynamics in ML. In Conf. on Functional Programming Languages and Computer Architecture. Cambridge, Massachusetts, August 1991, pages 406–426. Springer LNCS 523.
D. MacQueen, G. Plotkin, and R. Sethi. An ideal model for recursive polymorphic types. In Proceedings of the 11th ACM Symposium on Principles of Programming Languages, 1984.
D. C. J. Matthews. Static and Dynamic Type-Checking. In: Papers on Poly/ML. Technical Report 161, Computer Laboratory, University of Cambridge, February 1989.
R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.
A. Mycroft. Dynamic types in statically typed languages (preliminary draft). Unpublished typescript, December 1983.
A. Mycroft. Dynamic types in statically typed languages (2nd draft version). Unpublished typescript, August 1984.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leiß, H. (1993). Combining recursive and dynamic types. In: Bezem, M., Groote, J.F. (eds) Typed Lambda Calculi and Applications. TLCA 1993. Lecture Notes in Computer Science, vol 664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0037111
Download citation
DOI: https://doi.org/10.1007/BFb0037111
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56517-8
Online ISBN: 978-3-540-47586-6
eBook Packages: Springer Book Archive