Abstract
The integration of polymorphism (in the style of the ML let-construct), subtyping, and effects (modelling assignment or communication) into one common type system has proved remarkably difficult. One line of research has succeeded in integrating polymorphism and subtyping; adding effects in a straightforward way results in a semantically unsound system. Another line of research has succeeded in integrating polymorphism, effects, and subeffecting; adding subtyping in a straight-forward way invalidates the construction of the inference algorithm. This paper integrates all of polymorphism, effects, and subtyping into an annotated type and effect system for Concurrent ML and shows that the resulting system is a conservative extension of the ML type system.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
T. Amtoft, F. Nielson, H.R. Nielson: Type and behaviour reconstruction for higher-order concurrent programs. To appear in Journal of Functional Programming, 1997.
T. Amtoft, F. Nielson, H.R. Nielson, J. Ammann: Polymorphic subtypes for effect analysis: the dynamic semantics. This volume of SLNCS, 1997.
L. Damas and R. Milner: Principal type-schemes for functional programs. In Proc. of POPL '82. ACM Press, 1982.
Y.-C. Fuh and P. Mishra: Polymorphic subtype inference: closing the theory practice gap. In Proc. TAPSOFT '89. SLNCS 352, 1989.
Y.-C. Fuh and P. Mishra: Type inference with subtypes. Theoretical Computer Science, 73, 1990.
F. Henglein: Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):253–289, 1993.
F. Henglein and C. Mossin: Polymorphic binding-time analysis. In Proc. ESOP '94, pages 287–301. SLNCS 788, 1994.
M.P. Jones: A theory of qualified types. In Proc. ESOP '92, pages 287–306. SLNCS 582, 1992.
X. Leroy and P. Weis: Polymorphic type inference and assignment. In Proc. POPL '91, pages 291–302. ACM Press, 1991.
R. Milner: A theory of type polymorphism in programming. Journal of Computer Systems, 17:348–375, 1978.
J.C. Mitchell: Type inference with simple subtypes. Journal of Functional Programming, 1(3), 1991.
F. Nielson and H.R. Nielson: Constraints for polymorphic behaviours for Concurrent ML. In Proc. CCL'94. SLNCS 845, 1994.
F. Nielson, H.R. Nielson, T. Amtoft: Polymorphic subtypes for effect analysis: the algorithm. This volume of SLNCS, 1997.
H.R. Nielson and F. Nielson: Automatic binding analysis for a typed λ-calculus. Science of Computer Programming, 10:139–176, 1988.
H.R. Nielson and F. Nielson: Higher-order concurrent programs with finite communication topology. In Proc. POPL'94, pages 84–97. ACM Press, 1994.
P. Panangaden and J.H. Reppy: The essence of Concurrent ML. In ML with Concurrency: Design, Analysis, Implementation and Application (editor: Flemming Nielson), Springer-Verlag, 1996.
J.H. Reppy: Concurrent ML: Design, application and semantics. In Proc. Functional Programming, Concurrency, Simulation and Automated Reasoning, pages 165–198. SLNCS 693, 1993.
G.S. Smith: Polymorphic inference with overloading and subtyping. In SLNCS 668, Proc. TAPSOFT '93, 1993. Also see: Principal Type Schemes for Functional Programs with Overloading and Subtyping: Science of Computer Programming 23, pp. 197–226, 1994.
J.P. Talpin and P. Jouvelot: The type and effect discipline. Information and Computation, 111, 1994.
Y.-M. Tang: Control flow analysis by effect systems and abstract interpretation. PhD thesis, Ecoles des Mines de Paris, 1994.
M. Tofte. Type inference for polymorphic references. Information and Computation, 89:1–34, 1990.
M. Tofte and L. Birkedal: Region-annotated types and type schemes, 1996. Submitted for publication.
A.K. Wright: Typing references by effect inference. In Proc. ESOP '92, pages 473–491. SLNCS 582, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Riis Nielson, H., Nielson, F., Amtoft, T. (1997). Polymorphic subtyping for effect analysis: The static semantics. In: Dam, M. (eds) Analysis and Verification of Multiple-Agent Languages. LOMAPS 1996. Lecture Notes in Computer Science, vol 1192. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62503-8_8
Download citation
DOI: https://doi.org/10.1007/3-540-62503-8_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62503-2
Online ISBN: 978-3-540-68052-9
eBook Packages: Springer Book Archive