Atsushi Ohori
Kazuhiko Kato
ABSTRACT
We propose a method to extend an ML-style polymorphic language with transparent communication primitives, and give their precise operational semantics. These primitives allow any polymorphic programs definable in ML to be used remotely in a manner completely transparent to the programmer. Furthermore, communicating programs may be based on different architecture and use different data representations.
We define a polymorphic functional calculus with transparent communication primitives, which we call dML, as an extension of Damas and Milner's proof system for ML. We then develop an algorithm to translate dML to a “core” language containing only low-level communication primitives that are readily implementable in most of distributed environments. To establish the type safety of communicating programs, we define an operational semantics of the core language and prove that the polymorphic type system of dML is sound with respect to the operational semantics of the translated terms of the core language.
- ABC+83.M.P. Atldnson, P.J. Bailey, K.J. Chisholm, W.P. Cockshott, and R. Morrison. An approach to persistent programming. Computer Journal, 26(4), November 1983.Google Scholar
- ACPP91.M. Abadi, L. Cardelli, B. Pierce, and G. Plotldn. Dynamic typing in a statically-typed language. A CM Transcations on Programming Languages and Systems, 13(2):237-268, 1991. Google ScholarDigital Library
- ACPR92.M. Abadi, L. Cardelli, B. Pierce, and D. R~my. Dynamic typing in polymorphie languages, in A CM SIGPLAN Workshop on ML and its Applications, 1992.Google Scholar
- BMT92.D. Berry, R. Milner, and D. Turner. A semantics for ML concurrency primitives. In Proceedings of ACM Symposium on Principles of Programming Languages, pages 119-129, 1992. Google ScholarDigital Library
- BN84.A.D. BirreU and B. J. Nelson. Implementing remote procedure calls. A CM Transaction on Computer Systems, 2(1):39-59, 1984. Google ScholarDigital Library
- BO92.P. Buneman and A. Ohori. Polymoprhism and type inference in database programming. Technical report, University of Pennsylvania, 1992. To appear in A CM Transaction on Database Systems. Google ScholarDigital Library
- BST89.H.E. Bal, J. G. Steiner, and A. S. Tanenbaum. Programming languages for distributed computing systems. Computing Surveys, 21(3):261- 322, 1989. Google ScholarDigital Library
- CK92.R. Cooper and C. Krumvioda. Distributed programming with asynchronous ordered channels in distributed ML. In Proceedings of the A CM SIGPLAN Workshop on ML and its Applications, June 1992.Google Scholar
- CW85.L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471-522, December 1985. Google ScholarDigital Library
- DM82.L. Damas and R. Milner. Principal type-schemes for functional programs. In Proceedings ofA CM Symposium on Principles of Programming Languages, pages 207-212, 1982. Google ScholarDigital Library
- HL82.M. Hedihy and B. Liskov. A value transmission method for abstract data types. ACM Transactions on Programming Languages and Systems, 4(4):527-551, 1982. Google ScholarDigital Library
- HS87.R. Hayes and R. D. Schlichting. Facilitating mixed language programming in distributed systems. IEEE Transcations on Software Engineering, SE-13(12):1254--1264, December 1987. Google ScholarDigital Library
- JR86.M.B. Jones and R. E Rashid. Mach and Matchmaker: kernel and language support for objectoriented distributed systems. In Proceedings of A CM OOPSLA Conference, pages 67-77, 1986. Google ScholarDigital Library
- KO92.K. Kato and A Ohod. An approach to multilanguage persistent type system. In Proc. Hawaii International Confernece on System Science, pages 810-819, 1992.Google ScholarCross Ref
- LBG+87.B. Liskov, T. Bloom, D. Gifford, R. Scheifler, and W. Weihl. Communication in the Mercury system. Programming Methodology Group Memo 59, MIT, 1987.Google Scholar
- Ler92.X. Leroy. Unboxed objects and polymorphic typing. In Proceedings of ACM Symposium on Principles of Programming Languages, pages 177-188, 1992. Google ScholarDigital Library
- LM91.X. Leroy and M. Mauny. Dynamics in ML. In Proceedings of the A CM Conference on Functional Programming Languages and Computer Architecture, 199 I. Google ScholarDigital Library
- LMO92.G. Lindstrom, J. Maluszytiski, and T. Ogi. Our LISP are sealed: Interfacing functional and logic programming systems. In Proceedings of Symposium on Programming Language implementation and Logic Programming, Springer Lecture Notes in Computer Science, vol. 631., pages 428-442, 1992. August. Google Scholar
- Mac88.D. MacQueen. References and weak polymorphism. Note in Standard ML of New Jersey Distribution Package, 1988.Google Scholar
- MH88.j.C. Mitchell and R. Harper. The essence of ML. In Proceedings of A CM Symposium on Principles of Programming Languages, pages 28-46, San Diego, California, January 1988. Google ScholarDigital Library
- Mil78.R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, 1978.Google ScholarCross Ref
- MP88.J.C. Mitchell and G.D. Plotldn. Abstract types have existential type. A CM Transactions on Programming Languages and Systems, 10(3):470- 502, 1988. Google ScholarDigital Library
- MTH90.Ro Milner, M. Tofte, and R. Harper. The Definition of StandardML. The MIT Press, 1990. Google ScholarDigital Library
- Oho92.A Ohori. A compilation method for ML-style polymorphic record calculi, in Proceedings of A CM Symposium on Principles of Programming Languages, pages 154-165, 1992. Google ScholarDigital Library
- Rep91.J.H. Reppy. CML: A higher-order concurrent language, in Proceedings of A CM Conference on Programming Language Design and Implementation, pages 294-305, 1991. Google ScholarDigital Library
- Tof88.M. Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, Department of Computer Science, University of Edinburgh, 1988.Google Scholar
Index Terms
- Semantics for communication primitives in a polymorphic language
Recommendations
On polymorphic gradual typing
We study an extension of gradual typing—a method to integrate dynamic typing and static typing smoothly in a single language—to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically ...
Structural semantics for polymorphic data types (preliminary report)
POPL '83: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesThe semantic modeling of data types has been the subject of increased interest over the last few years, enhanced by the development of applicative languages such as Edinburgh's ML and HOPE, by the need for flexible highly structured languages that would ...
Comments