Higher Order Modules  - Caludio Russo
-------------------------------------

In my talk, I will sketch how to extend Standard ML Modules to 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 forthcoming 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.