A proposed categorical semantics for Pure ML
Wesley Phoa and Michael FourmanAbstract: 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.
A revised version is available.
Previous | Index | Next