[Sml-implementers] Moscow ML's higher-order modules are unsound

[Derek D. <dr...@cs...>]

The higher-order module extension to Standard ML provided in the
Moscow ML 2.00 compiler is unsound.  In particular, devious use of a
combination of generative and applicative functors can result, as in
the example given below, in the casting of an integer to a function,
and a segmentation fault when that function is called.  In this note
we proceed to explain what the problem is, how it arises, how it might
be overcome in Moscow ML, and how it can be avoided in the first place
by a stronger theory of type generativity.

The theory of higher-order modules developed in Chapter 5 of Claudio
Russo's thesis, on which the Moscow ML extension is based, supports
applicative functors *in place of* generative functors.  Applicative
functors return equivalent abstract types when applied to modules with
equivalent type components, whereas generative functors return new
abstract types at each application.  The theory naturally includes a
form of applicative functor signature as well, which is necessary to
specify the argument signature of a higher-order functor.

The Moscow ML extension, however, adds applicative functors and their
signatures on top of SML and its generative functors.  In our paper "A
Type System for Higher-Order Modules" (available in expanded form at
http://www.cs.cmu.edu/~dreyer/papers/thoms/full.pdf), we pointed out
that the way the two forms of functors interact in Moscow ML is
undesirable.  Specifically, there is no restriction on the bodies of
applicative functors, which means one can defeat the generativity of a
generative functor by eta-expanding it into an applicative one.  As a
consequence, the invariants one can assume regarding type abstraction
in generative functors are considerably weaker than in SML proper.

By itself, the weakness of Moscow ML's generative functors in the
presence of applicative functors is not unsound.  The unsoundness
arises (in a variant of the eta-expansion problem) because Moscow ML
also includes a form of generative functor *signature*, which is not
present in SML and has no formal basis in Russo's thesis.

We now describe our example of the unsoundness step-by-step (the full
code is given in one piece at the bottom of this note).  First, we
define two generative functors F1 and F2, both of signature UNIT -> S
but with different implementations of the abstract type t in S:

signature S = sig type t val x : t val f : t -> unit end
signature UNIT = sig end
structure Unit = struct end

functor F1 (X:UNIT) :> S =
    struct
        type t = int
        val x = 12
        fun f x = ()
    end

functor F2 (X:UNIT) :> S =
    struct
        type t = unit -> unit
        fun x () = ()
        fun f g = g ()
    end

We now define an *applicative* functor Apply, which takes a
*generative* functor F (of signature UNIT -> S) as its argument and
applies it to Unit.  In Moscow ML, applicative functors and their
signatures are differentiated from generative ones by omitting the
parentheses around the argument:

signature ARG = sig functor F : functor (X:UNIT) -> S end
functor Apply Arg:ARG = Arg.F(Unit)

Moscow ML returns the following signature for Apply:

> New type names: t
  functor Apply :
  {functor F : {}->?t/1.{type t = t/1, val x : t/1, 
                         val f : t/1 -> unit}}
    -> {type t = t, val f : t -> unit, val x : t}

The unsoundness is already foreseeable in this signature: every
instantiation of Apply will yield a module whose type component is
equal to the same abstract type "t", regardless of what the functor
argument F is.  In particular, if we instantiate Apply with F1 and F2,
the resulting type components are both deemed equal to "t", but
underneath the abstraction the types are really different:

structure Res1 = Apply(struct functor F = F1 end)
structure Res2 = Apply(struct functor F = F2 end)

val breakit = Res2.f(Res1.x)  (* core dump ensues *)

To understand why Apply is given an unsound signature, it is necessary
to understand where type abstraction occurs in generative
vs. applicative functors.  Generative functors generate new abstract
types every time they are applied; however, the definition of a
generative functor itself does not create any new abstract types.
Applicative functors are the opposite: new abstract types are created
at the *definition* of an applicative functor, corresponding to the
abstract types in the result.  These types must be parameterized (or
"skolemized") over the abstract types in the functor argument (if
there are any), so that the applicative functor will return equivalent
abstract types in the result only for equivalent arguments.  Once
these abstract type *constructors* have been created, the functor can
be given a fully transparent signature that refers to the constructors.

The problem, then, with the Apply functor above is that its argument
is a generative functor, which has no abstract type components itself,
and so the abstract type t in the result of Apply is not skolemized
over anything.  Another way of saying this is that all generative
functors of a given signature (e.g. UNIT -> S) are considered
trivially to have equivalent type components, since they have none.
That's why every application of Apply produces the same type "t".

One way to fix the unsoundness would be to drop generative functor
*signatures* from Moscow ML and to restrict generative functor
definitions to top-level (as in SML, where functors are first-order).
Apart from limiting the sorts of higher-order modules one can write,
this modification would still suffer from the problem (discussed
above) that generativity is weak in the presence of applicative
functors, but we conjecture that the language would be sound.  There
may be other solutions as well.

A better approach would be to strengthen the notion of generativity.
In particular, as we have argued in our paper (cited above),
generative functors should be treated as if they actually generate new
and possibly different types at each run-time instantiation, even if
such run-time type generation is not actually possible in the
language.  Now it is clearly only sound for a functor to be
"applicative" if every application of the functor to the same argument
produces the same type components in the result.  Thus, under our
interpretation of generativity, an applicative functor may not contain
generative functor applications because they produce types whose
definitions depend (in principle) on run-time conditions.

In our type system, this semantics is achieved by treating
generativity as a "dynamic effect" that is encapsulated by generative
functors and released at their applications.  Applicative functors are
those whose bodies are free of dynamic effects.  In particular, the
Apply functor in the example above could not be considered applicative
in our system because its body contains a generative functor
application, which is effectful.  (See our paper for further details
and comparison with other related work.)  As for the immediate problem
of restoring the soundness of Moscow ML, however, it is not clear to
us how this stronger account of generativity could be incorporated
directly into Russo's formalism for higher-order modules, which
underlies the Moscow ML implementation.

-- Derek Dreyer, Karl Crary and Bob Harper

--------------------------------------------------------------

Here's the unsoundness example in full:

signature S = sig type t val x : t val f : t -> unit end
signature UNIT = sig end
structure Unit = struct end

functor F1 (X:UNIT) :> S =
    struct
        type t = int
        val x = 12
        fun f x = ()
    end

functor F2 (X:UNIT) :> S =
    struct
        type t = unit -> unit
        fun x () = ()
        fun f g = g ()
    end

signature ARG = sig functor F : functor (X:UNIT) -> S end
functor Apply Arg:ARG = Arg.F(Unit)

structure Res1 = Apply(struct functor F = F1 end)
structure Res2 = Apply(struct functor F = F2 end)

val breakit = Res2.f(Res1.x)  (* core dump ensues *)