*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:

- how do we give meaning to signature expressions specifying functors?
- in what sense is a functor more general than another?
- how do we check that a functor matches a functor signature?
- how do we deal with type generativity?

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.

- [0] Robin Milner, Mads Tofte, Robert Harper, "The Definition of Standard ML", MIT Press, 1990.
- [1] Sandip K. Biswas "Higher-order functors with transparent signatures", Proc. 22nd Symp. Principles of Prog. Lang.,1995.
- [2] Claudio Russo "Standard ML Type Generativity as Existential Quantification", LFCS report ECS-LFCS-96-344.
- [3] Xavier Leroy "Applicative functors and fully transparent higher-order modules" Proc. 22nd Symp. Principles of Prog. Lang.,1995.

Presented at the *LFCS ML CLub*, May 1997.

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

- PostScript file (108 Kbytes)
- Gzipped PostScript file (43 Kbytes)