A proposed categorical semantics for Pure ML

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.