ABSTRACT
This paper relates two views of the operational semantics of a language with multiple inheritance. It is shown that the introduction of explicit coercions as an interpretation for the implicit coercion of inheritance does not affect the evaluation of a program in an essential way. The result is proved by semantic means using a denotational model and a computational adequacy result to relate the operational and denotational semantics.
- BCGS89.V. Breazu-Tannen, T. Coquand, C. A. Gunter, and A. Scedrov. Inheritance and explicit coercion (preliminary report). In R. Parikh, editor, Logic in Computer Science, pages 112- 134, IEEE Computer Society, June 1989. Google ScholarDigital Library
- BCGS90.V. Breazu-Tannen, T. Coquand, C. A. Gunter, and A. Scedrov. Inheritance as implicit coercion. University of Pennsylvania, Depamnent of Computer and Information Science technical report number MS-CIS-89-01. Journal version of {BCGS89} submitted to Information and Computation. Google ScholarDigital Library
- Car89.L. Cardelli. Typeful programming. Research Report 45, DEC Systems, Palo Alto, May 1989.Google Scholar
- CW85.L. Cardelli and P. Wegner. On understanding types, data abstraction and polymorphism. ACM Computing Surveys, 17(4):471-522, 1985. Google ScholarDigital Library
- Mey88.A.R. Meyer. Semantical paradigms: notes for an invited lecture. In Y. Gurevich, editor, Logic in Computer Science, pages 236-253, iEEE Computer Society, July 1988.Google Scholar
- Mog88.E. Moggi. The Partial l_~nbda-Calculus. PhD thesis, University of Edinburgh, 1988.Google Scholar
- OBB89.A. Ohori, P. Buneman, and V. Breazu-Tannen. Datbase programming in Machiavelli--a polymorphic language with static type inference. In SIGMOD Conference on the Management of Data, pages 46--57, ACM, 1989. Google ScholarDigital Library
- Plo77.G.D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223-255, 1977.Google ScholarCross Ref
- Wan89.M. Wand. Type inference for record concatenation and multiple inheritance. In Proceedings of the Symposium on Logic in Computer Science, pages 92-97, IEEE, June 1989. Google ScholarDigital Library
Index Terms
- Computing with coercions
Recommendations
Coercions in a polymorphic type system
We incorporate the idea of coercive subtyping, a theory of abbreviation for dependent type theories, into the polymorphic type system in functional programming languages. The traditional type system with let-polymorphism is extended with argument ...
Toward efficient gradual typing for structural types via coercions
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and ImplementationGradual typing combines static and dynamic typing in the same program. Siek et al. (2015) describe five criteria for gradually typed languages, including type soundness and the gradual guarantee. A significant number of languages have been developed in ...
Dynamic Translucency with Abstraction Kinds and Higher-Order Coercions
When a module language is combined with forms of non-parametric type analysis, abstract types require an opaque dynamic representation in order to maintain abstraction safety. As an idealisation of such a module language, we present a foundational ...
Comments