Types for Higher-Order Modules

Claudio V. Russo

Abstract:

In my talk, I will sketch how to extend Standard ML Modules to higher-order. Functors are given the same status that structures enjoy in Modules: they may be bound as components of structures, specified as functor arguments and returned as functor results.

I'll first motivate the move to higher-order with the help of an example. I'll then discuss the key ideas used in the generalisation. In particular:

My work can be seen as a more accessible, rational reconstruction of previous research by Biswas [1]. I take his ideas further by adding a suitable notion of generativity, using my results in [2]. This work is distinguished from Xavier Leroy's competive proposal [3] based on "dependent types": while he abandons the Definition of Standard ML [0] to start afresh, this work builds directly on the Definition using a simple generalisation of the underlying semantic objects and concepts. The semantic objects show no evidence of dependent types, and support the slogan:

"Dependent Types Considered Unnecessary for Higher-Order Modules".

This talk assumes a passing familiarity with the Definition of Standard ML. This work is part of my thesis.

Presented at the LFCS ML CLub, May 1997.

This is a set of 29 slides, available in the following formats: