Abstract
This paper outlines an approach to modelling the purely functional fragment of ML: it concentrates on the semantics of the Modules system. Our proposed semantics is set-theoretic: types and values are modelled by sets and functions in a topos, a categorical model of constructive set theory. Synthetic domain theory allows us to make sense of fixed points and recursive domains in a set-theoretic setting, while the notions of classifying topos and ‘generic’ structure provide a useful way of interpreting signatures, functors and sharing, as well as Extended ML specifications. We only give an informal account, concentrating on motivation and examples rather than giving a rigorous formal development—only elementary category theory is used.
Research supported by SERC grant GR/F 31199, ‘Formal System Design’; the first author was also supported by an 1851 Research Fellowship
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
P. Freyd, P. Mulry, G. Rosolini, D. S. Scott: Extensional PERs, in: Proc. of 5th Annual Symposium on Logic in Computer Science, 1990.
R. Harper, R. Milner, M. Tofte: A type discipline for program modules, in: Proc. of TAPSOFT '87, Springer LNCS 250, 1987.
R. Harper, J. Mitchell, E. Moggi: Higher-order modules and the phase distinction, in: Proc. 17th ACM Symposium on Principles of Programming Languages, 1990.
J. M. E. Hyland: The effective topos, in: The L. E. J. Brouwer Centenary Symposium (ed. A. S. Troelstra, D. van Dalen), North-Holland, 1982.
J. M. E. Hyland, E. P. Robinson, G. Rosolini: The discrete objects in the effective topos, Proc. Lond. Math. Soc. (3) 60 (1990) 1–36.
P. T. Johnstone: Topos Theory, Academic Press, 1977.
E. Kazmierczak: An institution for Extended ML, talk at the 9th Workshop on Abstract Data Types; report, in preparation.
J. Lambek, P. J. Scott: Introduction to Higher-Order Categorical Logic, Cambridge University Press, 1986.
D. MacQueen: Modules for Standard ML, in: Standard ML (R. Harper, D. MacQueen, R. Milner), available as ECS-LFCS-86-2, Laboratory for the Foundations of Computer Science, University of Edinburgh.
D. MacQueen: Using dependent types to express modular structure, in: Proc. 13th ACM Symposium on Principles of Programming Languages, 1990.
R. Milner, M. Tofte: Commentary on Standard ML, MIT Press, 1990.
R. Milner, M. Tofte, R. Harper: The Definition of Standard ML, MIT Press, 1990.
J. Mitchell, R. Harper: The essence of ML, in: Proc. 15th ACM Symposium on Principles of Programming Languages, 1988.
J. Mitchell, G. D. Plotkin: Abstract data types have existential types, ACM Trans. Programming Languages and Systems, 10(3):470–502.
W. K.-S. Phoa: Effective domains and intrinsic structure, in: Proc. of 5th Annual Symposium on Logic in Computer Science, 1990.
W. K.-S. Phoa: Domain Theory in Realizability Toposes, dissertation, University of Cambridge, November 1990; available as CST-82-91/ECS-LFCS-91-171, Department of Computer Science, University of Edinburgh.
W. K.-S. Phoa: A simple categorical model of first-order polymorphism, submitted.
G. Rosolini: Categories and effective computations, in: Lecture Notes in Computer Science 283, Springer, 1987.
D. T. Sannella, A. Tarlecki: Extended ML, an institution-independent framework for formal program development, in: Proc. of Category Theory and Computer Programming (Guildford), Springer LNCS 240, 1987.
R. D. Tennent, Semantics of Programming Languages, Prentice-Hall, 1991.
M. Tofte: Operational Semantics and Polymorphic Type Inference, dissertation, 1988; available as CST-52-88/ECS-LFCS-88-54, Department of Computer Science, University of Edinburgh.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Phoa, W., Fourman, M. (1992). A proposed categorical semantics for Pure ML. In: Kuich, W. (eds) Automata, Languages and Programming. ICALP 1992. Lecture Notes in Computer Science, vol 623. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55719-9_102
Download citation
DOI: https://doi.org/10.1007/3-540-55719-9_102
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55719-7
Online ISBN: 978-3-540-47278-0
eBook Packages: Springer Book Archive