LFCS

Laboratory for Foundations of Computer Science

Department of Computer Science — The University of Edinburgh

Standard ML Type Generativity as Existential Quantification

by

Claudio V. Russo

LFCS Report Series ECS–LFCS–96–344 LFCS June 1996

Department of Computer Science University of Edinburgh The King’s Buildings Edinburgh EH9 3JZ

Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, LFCS

Standard ML Type Generativity as Existential Quantification

Claudio V. Russo^{∗}

Technical Report ECS–LFCS–96–344 Department of Computer Science University of Edinburgh

June 25, 1996

Abstract: One of the distinguishing features of Standard ML is the use of type generativity. Each declaration of a datatype binds a globally fresh type name to the type identifier introduced. Type generativity has been regarded as an extra-logical device which, though desirable in a programming language to ensure data abstraction, bears no close resemblance to type theoretic constructs. We show that it corresponds precisely to existential quantification over types, and use the observation to suggest proper extensions to the current static semantics of Standard ML.

Keywords: language design, type theory, modules, Standard ML.

1 Introduction

Standard ML[13] has a rich modules language. Core language declarations of value and type identifiers can be packaged together into possibly nested structures. Access to structure components is by the dot notation and provides good control of the name space in a large program development. Structures are transparent: the identity of type components within a structure is evident even outside the structure[10].

ML provides two forms of data abstraction. The first is the datatype declaration which generates a new type with constructors mediating between it and its concrete representation. Each defining occurrence of a datatype is associated with a unique internal stamp, or generative type name; two structurally equivalent declarations result in different types. Hiding access to the constructors makes the type abstract. The second form is the functor. A functor is a mapping from structures to structures and is introduced by specifying an interface, or signature, for the formal argument, and providing an implementation of the body. The body may mention type and value components of the argument. Leaving some type identities in the interface unspecified constrains the functor to behave parametrically on all possible type arguments. A functor may be applied to any structure which supplies at least the components its signature requires. Datatypes defined in the functor body receive generative names each time the functor is applied; this guarantees type security.

∗Dept. of Computer Science, University of Edinburgh, The King’s Buildings, Edinburgh EH9 3JZ, email: cvr@dcs.ed.ac.uk. Supported by an award from the EPSRC. Thanks to D. Sannella, D. Aspinall and J. McKinna.

Traditionally, generativity is explained by the use of a compile-time, global state of names which is extended each time a datatype is declared or a functor applied, reflecting the operational approach used in the Definition[13]. On the other hand, the type theoretic approach to data abstraction relies on weak existential types[15] and is state-less. The relationship between generativity and existential quantification has been alluded to in the literature but was never made precise[15, 4]. We present a variant of the Standard ML static semantics, based directly on the use of existential types, which is provably equivalent to the generative semantics. We claim that the formulation is conceptually clearer, and use it to suggest interesting extensions to Standard ML.

2 Syntax

The syntax of our modules language is defined by

Structure Paths:  sp ::= x | sp.x
Type Expressions:  te ::= t | sp.t | te → te′
Signature Bodies:  D ::= type t = te; D
| type t; D
| structure x : Sg; D
| ϵ_{D}
Signature Expressions: Sg ::= sig D end
Structure Bodies:  d ::= type t = te; d
| datatype t = te; d
| structure x = se; d
| functor f (x : Sg) = se in d
| ϵ_{d}
Structure Expressions: se ::= sp
| struct d end
| f se

where t ∈ TyId, x ∈ StrId and f ∈ FunId range over disjoint sets of type, structure and functor identifiers. The syntax is based on Standard ML [13], however, since we are only concerned with the effect of module expressions on core language types, we have omitted value bindings to expressions from the core language and constructor bindings in type declarations. Our results should carry over easily to deal with local and parameterised type declarations.

To ease the presentation of signature elaboration, we have replaced the post hoc use of type sharing specifications sharing sp.t = sp′.u [13] by manifest type bindings type t = te; D [7, 3]. The result is that elaboration becomes completely syntax directed and we no

α,β,δ,γ ∈ TypeName =^{def} an infinite, denumerable set  type names
N,M,P,Q ∈ NameSet =^{def} Fin(TypeName)  finite name sets
τ or α or τ → τ′ ∈ Type =^{def} TypeName ⨄(Type × Type)  semantic types
S ∈ Str =^{def} TyId →^{fin} Type × StrId →^{fin} Str  structures
X or ∃N.S ∈ ExStr =^{def} NameSet × Str  existential

structures

L or ΛN.S ∈ Sig =^{def} NameSet × Str  parameterised

structures

Φ or ∀N.S → X ∈ FunSig =^{def} NameSet ×(Str × ExStr)  functor signatures
C or (C_{t}, C_{x}, C_{f}) ∈ Context =^{def} \{ \begin{matrix}TyId →^{fin} Type × \\ StrId →^{fin} Str × \\ FunId & →^{fin} & FunSig \end{matrix}  contexts

Figure 1: Semantic Objects

longer have to introduce the notion of principal signature [13]. Our simplification is not essential [9, 1].

Finally, Standard ML functors may only be declared at top-level. To avoid introducing a further phrase class, we instead allow local declarations of functors in structure bodies, e.g. functor f (x : Sg) = se in d: the scope of f is d. Moreover, f does not become a component of the resulting semantic structure. Structure bodies thus serve the function of ML’s top-level. Note that the language is still first-order: functors may neither take functors as arguments nor return them as results.

In Standard ML, the structure expression struct d end introduces a generative structure name, used to identify the module. We ignore the largely orthogonal issues of structure identity and the use of structure sharing specifications within signatures, but retain the phrase for familiarity.

3 Semantic Objects

Figure 1 defines the semantic objects assigned to module expressions. They serve the role of types in the module semantics. We let O range over all semantic objects.

Notation. For sets A and B, Fin(A) denotes the set of finite subsets of A, and A →^{fin} B denotes the set of finite maps (partial functions with finite domain) from A to B. A finite map will often be written explicitly as a set in the form {a_{1} ↦ b_{1}, ⋯, a_{k} ↦ b_{k}}, k ≥ 0. Let f and g be finite maps. Dom(f) and Rng(f) denote the domain of definition and range of f. The finite map f + g has domain Dom(f) ∪ Dom(g) and values (f + g)(a) =^{def} if a ∈ Dom(g) then g(a) else f(a). If Rng(g) = Dom(f) then f ∘ g is the finite map with values (f ∘g)(a) =^{def} f(g(a)). For A ⊆ Dom(f), the restriction f ↓ A is the finite map with domain A and values (f ↓ A)(a) =^{def} f(a).

Definition 1 (Semantic Structures). A semantic structure S consists of a pair (S_{t}, S_{x}) of finite maps binding type identifiers to semantic types and structure identifiers to semantic structures respectively. For notational convenience we will define extension and retrieval

functions [t = τ]S =^{def} ({t ↦ τ} + S_{t}, S_{x}), S(t) =^{def} S_{t}(t), [x : S′]S =^{def} (S_{t}, {x ↦ S′} + S_{x})

and S(x) =^{def} S_{x}(x). Let ϵ_{S} denote the empty semantic structure (∅, ∅).

Note that Λ, ∃ and ∀ bind type names. The object ΛN.S describes a family of structures, whose members are obtained by substituting types for the parameters in N. The object ∃N.S on the other hand, is a semantic structure in which occurrences of certain types have been made abstract by existential quantification. In a functor signature ∀N.S → X, names in N are bound simultaneously in S and X. These names capture the type components of the argument structure S on which the functor behaves parametrically; their possible occurrence in the result X caters for the propagation of type identities from the functor’s actual argument. The range X is always of the form X ≡ ∃M.S′ for a set M of names. Typically, M is non-empty. It corresponds to the generative name set of the functor signature as in the Definition of Standard ML [13]. Applying a functor with the above signature results in a variant of the structure S′, obtained by choosing fresh names to replace those in M.

Standard ML is decidedly non-committal in its choice of binding operators, using parenthesised name sets uniformly to indicate binding in semantic objects. We prefer to differentiate binders with the more suggestive notation ∀, ∃ and Λ.

Definition 2 (Contexts). A context C consists of a triple (C_{t}, C_{x}, C_{f}) of finite maps binding type identifiers to semantic types, structure identifiers to semantic structures and functor identifiers to functor signatures respectively. We define extension and retrieval functions C[t = τ] =^{def} (C_{t} + {t ↦ τ}, C_{x}, C_{f}), C(t) =^{def} C_{t}(t), C[x : S] =^{def} (C_{t}, C_{x} +

{x ↦ S}, C_{f}), C(x) =^{def} C_{x}(x), C[f : Φ] =^{def} (C_{t}, C_{x}, C_{f} + {f ↦ Φ}) and C(f) =^{def} C_{f}(f).

Note that rebindings to identifiers take precedence to the right in both semantic structures and contexts. However, we “extend” structures to the left, and contexts to the right.

We will let FN(O) denote the set of names free in O, where the notions of free and bound name are defined as usual.

Definition 3 (Renamings). A renaming is a finite map from type names to type names. We let ρ, σ, and π range over renamings. We will use the more suggestive notation [M/N] to denote a bijective renaming with domain N and range M, which simply swaps names. The effect of applying a renaming ρ to a name α, written ρ⟨α⟩, is defined to be ρ⟨α⟩ =^{def} if α ∈ Dom(ρ) then ρ(α) else α. We extend the operation of renaming free names compositionally to all semantic objects in such a way that bound variables are renamed only when necessary to avoid capture of names; and ρ⟨O⟩ ≡ σ⟨O⟩ whenever ρ⟨α⟩ = σ⟨α⟩ for every α ∈ FN(O). Let Inv(ρ) =^{def} Dom(ρ) ∪ Rng(ρ) describe the set of names involved in the renaming ρ.

C ⊢ sp : S  \begin{matrix}C(x) = S \\ C ⊢ x : S \end{matrix} \begin{matrix}C ⊢ sp : S′ & S′(x) = S \\ C ⊢ sp.x : S \end{matrix}
C ⊢ te ▷ τ  \begin{matrix}C(t) = τ \\ C ⊢ t ▷ τ \end{matrix} \begin{matrix}C ⊢ sp : S′ & S′(t) = τ \\ C ⊢ sp.t ▷ τ \end{matrix} \begin{matrix}C ⊢ te ▷ τ & C ⊢ te′ ▷ τ′ \\ C ⊢ te → te′ ▷ τ → τ′ \end{matrix}

C ⊢ D ▷ L

C ⊢ te ▷ τ C[t = τ] ⊢ D ▷ ΛQ.S Q ∩ FN(τ) = ∅
C ⊢ type t = te; D ▷ ΛQ.[t = τ]S
C[t = α] ⊢ D ▷ ΛP.S α ∉ FN(C) ∪ P
C ⊢ type t; D ▷ Λ{α} ∪ P .[t = α]S
C ⊢ Sg ▷ ΛP.S P ∩ FN(C) = ∅ C[x : S] ⊢ D ▷ ΛQ.S′ Q ∩ (P ∪ FN(S)) = ∅

C ⊢ structure x : Sg; D ▷ ΛP ∪ Q.[x : S]S′

C ⊢ ϵ_{D} ▷ Λ∅.ϵ_{S}  \begin{matrix}C ⊢ D ▷ L′ & L′ ≡^{α} L \\ C ⊢ D ▷ L \end{matrix}
C ⊢ Sg ▷ L  \begin{matrix}C ⊢ D ▷ L \\ C ⊢ sig D end ▷ L \end{matrix} \begin{matrix}C ⊢ Sg ▷ L′ & L′ ≡^{α} L \\ C ⊢ Sg ▷ L \end{matrix}

Figure 2: Judgements common to both static semantics

Definition 4 (α-Equivalence). The notion of α-equivalence of semantic objects is defined as usual, in particular: for X ≡ ∃P.S and X′ ≡ ∃P′.S′, X ≡^{α} X′ iff there is a bijective renaming [P′/P] such that [P′/P]⟨S⟩ ≡ S′ and FN(X) = FN(X′).

Definition 5 (Enrichment Relation). Given two structures S ≡ (S_{t}, S_{x}) and S′ ≡ (S′_{t}, S′_{x}), S enriches S′, written S ⪰ S′, iff

1. Dom(S_{t}) ⊇ Dom(S′_{t}) and for all t ∈ Dom(S′_{t}), S(t) = S′(t), and

2. Dom(S_{x}) ⊇ Dom(S′_{x}) and for all x ∈ Dom(S′_{x}), S(x) ⪰ S′(x).

Definition 6 (Instantiation Relation). S → X ≤ ∀N.S′ → X′ iff there exists a substitution, φ, of semantic types for type names, with Dom(φ) = N, such that S ≡ φ (S′)

and X ≡^{α} φ (X′).

4 Static Semantics

In this section we introduce two distinct static semantics for structure bodies and structure expressions. The systems rely on shared judgement forms dealing with structure paths, type expressions, signature bodies and signature expressions. The common judgements are shown in Figure 2. We can factor out these judgements because they do not generate any new free names in their conclusions.

C, N ⊢ d ⇒ S, M  C, N ⊢ ϵ_{d} ⇒ ϵ_{S}, ∅ (E-1)

\begin{matrix}C ⊢ te ▷ τ & C[t = τ], N ⊢ d ⇒ S, M \\ C, N ⊢ type t = te; d ⇒ [t = τ]S, M \end{matrix} (E-2)
C ⊢ te ▷ τ δ ∉ N C[t = δ], N ∪ {δ} ⊢ d ⇒ S, Q

C, N ⊢ datatype t = te; d ⇒ [t = δ]S, {δ} ∪ Q (E-3)

C, N ⊢ se ⇒ S, P C[x : S], N ∪ P ⊢ d ⇒ S′, Q

C, N ⊢ structure x = se; d ⇒ [x : S]S′, P ∪ Q

(E-4)

\begin{matrix}C ⊢ Sg ▷ ΛP.S′ & P ∩ N = ∅ \\ C[x : S′], N ∪ P ⊢ se ⇒ S′′, Q & C[f : ∀P.S′ → ∃Q.S′′], N ⊢ d ⇒ S, M \end{matrix}

C, N ⊢ functor f (x : Sg) = se in d ⇒ S, M

(E-5)

C, N ⊢ se ⇒ S, M \begin{matrix}C ⊢ sp : S \\ C, N ⊢ sp ⇒ S, ∅ \end{matrix} (E-6) C, N ⊢ d ⇒ S, M C, N ⊢ struct d end ⇒ S, M (E-7)

\begin{aligned}C, N ⊢ se ⇒ S′, P & S′′ → ∃Q.S ≤ C(f) & S′ ⪰ S′′ & Q ∩ (N ∪ P) = ∅ \\ & C, N ⊢ f se ⇒ S, P ∪ Q \end{aligned} (E-8)

Figure 3: Elaboration rules based on generative names

4.1 Elaboration Semantics

Figure 3 presents the Standard ML style static semantics for our language. Consider the form of the judgements C, N ⊢ d ⇒ S, M and C, N ⊢ se ⇒ S, M. The explicit set of names, N, is meant to capture a superset of the names generated so far. Elaboration produces, besides the semantic object S, the set of names M generated during the elaboration of the phrase d or se. The name sets are threaded through elaboration trees in a global, state-like manner. This avoids any unsafe confusion of existing names with the fresh names generated by datatypes (Rule (E-3)) and functor applications (Rule (E-8)). The generative nature of elaboration is expressed by the following property:

Property 1 (Generativity). If C, N ⊢ d/se ⇒ S, M then N ∩ M = ∅.^{1}

Note that the sets of generated names are not redundant. Suppose we deleted them from the elaboration judgements and replaced occurrences of N by FN(C). Then it is easy to see that

structure x = struct datatype t = int end;
structure y = struct structure x = struct end;

datatype u = bool end

⇒ \begin{matrix}[x : & [t = α]] \\ [y : & [x : ϵ_{S}] \\ [u = α] & ] \end{matrix}

so that x.t = y.u even though it is definitely the case that bool ≠ int. This is a type insecurity. The problem arises because the name α generated for t is no longer free in the

1When P is a predicate, we use the abbreviation P (d/se) to mean P (d) and P (se).

C ⊢ d : X  C ⊢ ϵ_{d} : ∃∅.ϵ_{S} (T-1)
\begin{matrix}C ⊢ te ▷ τ & C[t = τ] ⊢ d : ∃P.S & P ∩ FN(τ) = ∅ \\ C ⊢ type t = te; d : ∃P.[t = τ]S \end{matrix} (T-2)
C ⊢ te ▷ τ δ ∉ FN(C) ∪ Q C[t = δ] ⊢ d : ∃Q.S
C ⊢ datatype t = te; d : ∃{δ} ∪ Q.[t = δ]S

(T-3)

C ⊢ se : ∃P.S P ∩ FN(C) = ∅ C[x : S] ⊢ d : ∃Q.S′ Q ∩ (P ∪ FN(S)) = ∅
C ⊢ structure x = se; d : ∃P ∪ Q.[x : S]S′

(T-4)

C ⊢ Sg ▷ ΛP.S P ∩ FN(C) = ∅ C[x : S] ⊢ se : X′ C[f : ∀P.S → X′] ⊢ d : X
C ⊢ functor f (x : Sg) = se in d : X

(T-5)

C ⊢ se : X  \begin{matrix}C ⊢ sp : S \\ C ⊢ sp : ∃∅.S \end{matrix} (T-6) C ⊢ d : X C ⊢ struct d end : X (T-7)

\begin{aligned}C ⊢ se : ∃P.S′ & P ∩ (FN(C(f)) ∪ Q) = ∅ & S′′ → ∃Q.S ≤ C(f) & S′ ⪰ S′′ \\ & C ⊢ f se : ∃P ∪ Q.S \end{aligned} (T-8)

≡^{α} -conversion \begin{matrix}C ⊢ d : X′ & X′ ≡^{α} X \\ C ⊢ d : X \end{matrix} (T-9) \begin{matrix}C ⊢ se : X′ & X′ ≡^{α} X \\ C ⊢ se : X \end{matrix} (T-10)

Figure 4: Type system based on existential quantification

context by the time we need to guess a fresh name for u: it is hiding in the shadow of the second binding to x in the context [x : [t = α]][x : ϵ_{S}]. In the elaboration semantics, the prior use of α will be recorded in the set of names N ∪ {α} at the point at which we are elaborating datatype u = int, forcing us to choose a distinct name. These observations motivate:

Definition 7 (Rigidity). A context C is rigid w.r.t. N, written C, N rigid, iff FN(C) ⊆ N.

As long as we start with C, N rigid, as a consequence of Property 1, those names in M resulting from the elaboration of d and se will never be confused with names visible in the context, even if these are temporarily hidden by bindings added to C during subelaborations.

4.2 Type Theoretic Semantics

Figure 4 presents an alternative static semantics for structure bodies and expressions, defined by the judgements C ⊢ d : ∃M.S and C ⊢ se : ∃M.S. Rather than maintaining a global state of names threaded through elaborations, we adopt the view that module expressions type-check to existentially quantified semantic structures. The key idea is to replace global generativity with implicit elimination and introduction of existential types — in essence: local generativity. In the rules, the side conditions on names sets prevent capture of names in the usual way. Rules (T-9) and (T-10) ensure that we can always rename bound variables if necessary to satisfy the side conditions. We will give an intuitive explanation of some of the rules:

type t = te; d We simplify te to find a corresponding semantic type τ. We then check d in the context extended by the binding of τ to t, to obtain an existentially quantified structure ∃P.S. Provided τ does not contain any of the names bound by P in ∃P.S we can eliminate the existential, extend S by the binding to t and then hide the hypothetical types by existentially quantifying over the resulting structure.

datatype t = te; d We proceed as in the previous case, except that instead of binding t to its definition, we bind it a locally fresh type name δ. Type checking d results in semantic structure ∃Q.S, which may contain occurrences of δ. We conceptually eliminate the existential quantification over S, extend S by the abstract binding to t and then existentially quantify over both the abstract type δ and the Q hypothetical types we just eliminated.

structure x = se; d We typecheck se to an existential structure ∃P.S. We locally eliminate the existential, introducing fresh hypothetical types P, and type check d in the suitably extended context to obtain a semantic structure ∃Q.S′. Now ∃Q.S′ may contain some of the locally introduced hypothetical types in P, and these should not escape their scope. We eliminate the existential ∃Q.S′, extend the result by the binding to x and existentially quantify over the types P ∪ Q.

functor f (x : Sg) = se in d The signature expression Sg denotes a family of semantic structures, ΛP.S. We want f to be applicable to all enrichments of instances of ΛP.S. To this end, we type check the body se of f in a context extended with a generic instance of ΛP.S, i.e. S, where we ensure that P is a locally fresh choice of type names. Now se will typecheck to an existentially quantified structure X′, which may contain occurrences of our generic names P. Since the functor typechecks for a generic choice of names, it will typecheck for any substitution of types for these names. We universally quantify over P, and add the polymorphic binding to f locally to the context. Type checking the scope d of the functor declaration yields the result X for the entire phrase. Note that the result does not contain a “functor binding” for f.

f se Type check se to obtain an existentially quantified structure ∃P.S′. Locally eliminate the quantifier to see whether the functor may be applied to the structure (a combination of instantiation and enrichment), obtaining an existentially quantified result of type ∃Q.S. The functor may propagate some of the hypothetical types in P. To prevent them escaping their scope, we hide them by extending the existential quantification over S to cover both P and Q.

sp We simply look up sp in the context to obtain an (unquantified) semantic structure. Note that the dot notation is completely independent of the treatment of existentials.

Before proceeding to the statement of the main result we need one last concept:

Definition 8 (Well-formedness). A functor signature Φ ≡ ∀N.S → X is well-formed, written Φ WF, iff for every α ∈ N, α ∈ FN(X) only if α ∈ FN(S).

A context C is well-formed, written C WF, precisely when all the functor signatures in its range are well-formed.

The well-formedness of a functor signature Φ ensures that whenever we apply the functor, the free names of the result are either propagated from the actual argument, or were already free in Φ:

Lemma 2. If Φ WF and S → X ≤ Φ then FN(X) ⊆ FN(S) ∪ FN(Φ).

In the elaboration semantics, if we start with a well-formed context, then the names occuring in the result of the elaboration will be a subset of the names occuring in the input and output name sets, i.e. the state will correctly record the set of generated names. In the type-theoretic semantics, well-formedness of the context ensures that the free names of the result are a subset of the free names of the context:

Lemma 3 (Free Names). If C WF then C ⊢ d/se : X implies FN(X) ⊆ FN(C).

Proof(Sketch). The proof follows easily by rule induction. The idea is to maintain wellformedness as an invariant of the system and appeal to Lemma 2 in the functor application rule.

5 Main Result

Having defined our systems, we are now in a position to state the main result of the paper:

Theorem 4 (Main Result). Provided C WF and C, N rigid:

Completeness If C, N ⊢ d/se ⇒ S, M then C ⊢ d/se : ∃M.S.

Soundness If C ⊢ d/se : X then, for some M and S, C, N ⊢ d/se ⇒ S, M with X ≡^{α} ∃M.S.

An operational view of the system in Figure 4 is that we have replaced the notion of global generativity by local generativity and the ability to rename bound names when necessary. The proof of completeness is easy because, if a name is globally fresh, it will certainly be locally fresh, enabling a straightfoward construction of a corresponding derivation.

Proof(Completeness). We use simultaneous induction on the elaboration rules to prove the theorems:

C, N ⊢ d/se ⇒ S, M ⊃ C WF ⊃ C, N rigid ⊃ C ⊢ d/se : ∃M.S

For lack of space, we will only consider the rule for structure declarations:

Rule (E-4) Assume the premises

C, N ⊢ se ⇒ S, P (i)  C[x : S], N ∪ P ⊢ d ⇒ S′, Q (ii)

and induction hypotheses:

C WF ⊃ C, N rigid ⊃ C ⊢ se : ∃P.S  (iii)
C[x : S] WF ⊃ C[x : S], N ∪ P rigid ⊃ C[x : S] ⊢ d : ∃Q.S′  (iv)

Suppose C WF (v) and C, N rigid (vi). Using induction hypothesis (iii) on (v) and (vi) we obtain:

C ⊢ se : ∃P.S  (vii)

Property 1 of (i), together with (vi), ensures that:

P ∩ FN(C) = ∅  (viii)

Clearly (v) extends to C[x : S] WF (ix). Hence Lemma 3 on (vii) guarantees FN(∃P.S) ⊆ FN(C). It follows from (vi) that FN(S) ⊆ N ∪ P (x) and consequently C[x : S], N ∪ P rigid (xi). Applying the induction hypothesis (iv) to (ix) and (vi) yields:

C[x : S] ⊢ d : ∃Q.S′  (xii)

Property 1 of (ii) ensures Q ∩ (N ∪ P) = ∅ which, together with (x), entails:

Q ∩ (P ∪ FN(S)) = ∅  (xiii)

Rule (T-4) on (vii), (viii), (xiii) and (xii) derives

C ⊢ structure x = se; d : ∃P ∪ Q.[x : S]S′

as desired.

In the complete proof, Property 1 and Lemma 3 conspire to ensure the side conditions of Rules (T-1)—(T-8) hence appeals to the α-conversion Rules (T-9) and (T-10) are never required.

5.1 Soundness

Soundness is more difficult to prove, because the type system in Figure 4 only requires subderivations to hold for particular choices of locally fresh names. A name may be locally fresh without being globally fresh, foiling naive attempts to construct an elaboration from a typing derivation.

C ⊢′ d : X  C ⊢ te ▷ τ δ ∉ Q ∀γ.C[t = γ] ⊢′ d : [γ/δ]⟨∃Q.S⟩ C ⊢′ datatype t = te; d : ∃{δ} ∪ Q.[t = δ]S (T’-3)

\begin{matrix}C ⊢′ se : ∃P.S & Q ∩ (P ∪ FN(S)) = ∅ \\ ∀π.Dom(π) = P ⊃ C[x : π⟨S⟩] ⊢′ d : π⟨∃Q.S′⟩ \end{matrix}

C ⊢′ structure x = se; d : ∃P ∪ Q.[x : S]S′

(T’-4)

\begin{matrix}C ⊢ Sg ▷ ΛP.S & P ∩ FN(C) = ∅ \\ ∀π.Dom(π) = P ⊃ C[x : π⟨S⟩] ⊢′ se : π⟨X′⟩ & C[f : ∀P.S → X′] ⊢′ d : X \end{matrix}

C ⊢′ functor f (x : Sg) = se in d : X

(T’-5)

C ⊢′ se : X \begin{matrix}C ⊢′ se : ∃P.S′ & P ∩ (FN(C(f)) ∪ Q) = ∅ \\ ∀π.Dom(π) = P ⊃ ∃S′′.S′′ → π⟨∃Q.S⟩ ≤ C(f) ∧ π⟨S′⟩ ⪰ S′′ \end{matrix} ; C ⊢′ f se : ∃P ∪ Q.S (T’-7)

Figure 5: Type system with generalised premises

To address this problem, we introduce a modified formulation of the type system with the judgement forms C ⊢′ d : ∃M.S and C ⊢′ se : ∃M.S. The modified rules appear in Figure 5. Instead of requiring premises to hold for particular choices of fresh names, they require them to hold for every choice of names. This makes it easy to reconstruct an elaboration tree from a judgement in the generalised system. Note that the inference rules are no longer finitely branching, yet they remain well-founded and amenable to inductive arguments. The technique is adapted from McKinna and Pollack’s formalisation of αconversion[12].

The strategy for proving soundness is to first show that any derivation in the original type theoretic system gives rise to a corresponding derivation in the generalised system:

Lemma 5 (Soundness — Part I). If C WF and C ⊢ d/se : X then C ⊢′ d/se : X.

One then proves that any derivation in the generalised system gives rise to a corresponding elaboration:

Lemma 6 (Soundness — Part II). If C WF and C ⊢′ d/se : X then, for any N satisfying C, N rigid, we can find an M and S such that C, N ⊢ d/se ⇒ S, M, with X ≡^{α} ∃M.S.

Proof(Lemma 5). We use simultaneous induction on the rules to prove the stronger theorems:

C ⊢ d/se : X ⊃ C WF ⊃ ∀ρ.ρ⟨C⟩ ⊢′ d/se : ρ⟨X⟩

Lemma 5 follows immediately by choosing ρ to be the empty (identity) renaming.

For lack of space, we will only consider the rule for structure declarations. The other cases are similar.

Rule (T-4) Assume the premises

C ⊢ se : ∃P.S_{p} (i)  P ∩ FN(C) = ∅ (ii)
C[x : S_{p}] ⊢ d : ∃Q.S_{q} (iii)  Q ∩ (P ∪ FN(S_{p})) = ∅ (iv)

and induction hypotheses:

C WF ⊃ ∀ρ.ρ⟨C⟩ ⊢′ se : ρ⟨∃P.S_{p}⟩  (v)
C[x : S_{p}] WF ⊃ ∀ρ.ρ⟨C[x : S_{p}]⟩ ⊢′ d : ρ⟨∃Q.S_{q}⟩  (vi)

Suppose C WF (vii) and consider an arbitrary renaming ρ. We need to show:

ρ⟨C⟩ ⊢′ structure x = se; d : ρ⟨∃P ∪ Q.[x : S_{p}]S_{q}⟩  (viii)

Choose a fresh set of names M and structure S_{m} such that

∃P ∪ Q.[x : S_{p}]S_{q} ≡^{α} ∃M.S_{m}

and M ∩ (Inv(ρ) ∪ P ∪ FN(ρ⟨C⟩)) = ∅. By the definition of ≡^{α} we must have some bijective renaming σ with domain P ∪ Q and range M such that S_{m} ≡ σ⟨[x : S_{p}]S_{q}⟩. Let

P′ =^{def} σ⟨P ⟩, Q′ =^{def} σ⟨Q⟩, [P′/P] =^{def} σ ↓ P, [Q′/Q] =^{def} σ ↓ Q, S′_{p} =^{def} σ⟨S_{p}⟩ and S′_{q} =^{def} σ⟨S_{q}⟩.

Re-expressing the previous equation we have:

∃P ∪ Q.[x : S_{p}]S_{q} ≡^{α} ∃P′ ∪ Q′.[x : S′_{p}]S′_{q}

Moreover, it is easy to verify that:

P′ ∩ Q′ = ∅ (ix)  ∃P.S_{p} ≡^{α} ∃P′.S′_{p} (x)  ∃Q.S_{q} ≡^{α} [P/P′]⟨∃Q′.S′_{q}⟩ (xi)

By induction hypothesis (v) on (vii) and ρ we obtain ρ⟨C⟩ ⊢′ se : ρ⟨∃P.S_{p}⟩ (xii). Now

ρ⟨∃P.S_{p}⟩ ≡^{α} ρ⟨∃P′.S′_{p}⟩ ≡^{α} ∃P′.ρ⟨S′_{p}⟩ by (x) and since P′ ∩ Inv(ρ) = ∅, so by α-conversion

(Rule (T’-10)) on (xii) we can derive:

ρ⟨C⟩ ⊢′ se : ∃P′.ρ⟨S′_{p}⟩  (xiii)

By Lemma 3 on (i) and (vii) we have FN(∃P.S_{p}) ⊆ FN(C) from which it is easy to deduce that FN(ρ⟨S′_{p}⟩) ⊆ P′ ∪ FN(ρ⟨C⟩). Together with (ix) and our choice of M this ensures:

Q′ ∩ (P′ ∪ FN(ρ⟨S′_{p}⟩)) = ∅  (xiv)

It remains to show:

∀π.Dom(π) = P′ ⊃ ρ⟨C⟩[x : π⟨ρ⟨S′_{p}⟩⟩] ⊢′ d : π⟨∃Q′.ρ⟨S′_{q}⟩⟩  (xv)

Consider an arbitrary renaming π with domain P′. Let ρ′ =^{def} ρ + (π ∘ [P′/P]). Clearly (vii) extends to C[x : S_{p}] WF. Applying induction hypotheses (vi) to ρ′ establishes

ρ′⟨C[x : S_{p}]⟩ ⊢′ d : ρ′⟨∃Q.S_{q}⟩  (xvi)

Now ρ′⟨C⟩ ≡ ρ + (π ∘ [P′/P])⟨C⟩ ≡ ρ⟨C⟩ since P ∩ FN(C) = ∅ and

ρ′⟨S_{p}⟩ ≡ π⟨ρ + [P′/P]⟨S_{p}⟩⟩  by considering α ∈ FN(S_{p})
≡ π⟨ρ⟨[P′/P]⟨S_{p}⟩⟩⟩  since P′ ∩ Dom(ρ) = ∅
≡ π⟨ρ⟨σ⟨S_{p}⟩⟩⟩  since Q ∩ FN(S_{p}) = ∅
≡ π⟨ρ⟨S′_{p}⟩⟩  (xvii)

so we can re-express (xvi) as ρ⟨C⟩[x : π⟨ρ⟨S′_{p}⟩⟩] ⊢′ d : ρ′⟨∃Q.S_{q}⟩ (xviii). Observe that

ρ′⟨∃Q.S_{q}⟩ ≡^{α} ρ + (π ∘ [P′/P])⟨[P/P′]⟨∃Q′.S′_{q}⟩⟩ by (xi)
≡ π⟨ρ + [P′/P]⟨∃Q′.S′_{q}⟩⟩  by considering α ∈ FN(∃Q′.S′_{q})
≡ π⟨ρ⟨∃Q′.S′_{q}⟩⟩  since P ∩ FN(∃Q′.S′_{q}) = ∅
≡^{α} π⟨∃Q′.ρ⟨S′_{q}⟩⟩  since Q′ ∩ Inv(ρ) = ∅.

Using α-conversion (Rule (T’-9)) on (xviii) and the last equation we can derive:

ρ⟨C⟩[x : π⟨ρ⟨S′_{p}⟩⟩] ⊢′ d : π⟨∃Q′.ρ⟨S′_{q}⟩⟩  (xix)

Since π was arbitrary we have established (xv). Rule (T’-4) on (xiii), (xiv) and (xv) lets us derive:

ρ⟨C⟩ ⊢′ structure x = se; d : ∃P′ ∪ Q′.[x : ρ⟨S′_{p}⟩]ρ⟨S′_{q}⟩  (xx)

Finally, ∃P′ ∪ Q′.[x : ρ⟨S′_{p}⟩]ρ⟨S′_{q}⟩ ≡^{α} ρ⟨∃P ∪ Q.[x : S_{p}]S_{q}⟩ follows easily from (P′ ∪ Q′) ∩

Inv(ρ) = ∅. Applying α-conversion (Rule (T’-9)) on (xx) and the last equation yields (viii) as desired.

Before proceeding with the proof of Lemma 6 we will require the counterpart to Lemma 3 (proof omitted but easy):

Lemma 7 (Free Names). If C WF and C ⊢′ d/se : X then FN(X) ⊆ FN(C).

Proof(Lemma 6). We use simultaneous induction on the rules to prove the theorems:

C ⊢′ d/se : X ⊃ C WF ⊃ ∀N. C, N rigid ⊃ ∃M, S. C, N ⊢ d/se ⇒ S, M ∧ X ≡^{α} ∃M.S

Again, we will only consider the rule for structure declarations. The other cases are similar.

Rule (T’-4) Assume the premises

C ⊢′ se : ∃P.S_{p} (i) Q ∩ (P ∪ FN(S_{p})) = ∅ (ii)
∀π.Dom(π) = P ⊃ C[x : π⟨S_{p}⟩] ⊢′ D : π⟨∃Q.S_{q}⟩ (iii)

and induction hypotheses:

(iv) C WF ⊃ ; ∀N. C, N rigid ⊃ ; \begin{aligned}∃P′, S′_{p}. & C, N ⊢ se ⇒ S′_{p}, P′ \\ & ∧ ∃P.S_{p} ≡^{α} ∃P′.S′_{p} \end{aligned}

(v)

∀π.Dom(π) = P ⊃

C[x : π⟨S_{p}⟩] WF ⊃ ; ∀N. C[x : π⟨S_{p}⟩], N rigid ⊃ ; \begin{aligned}∃Q′, S′_{q}. & C[x : π⟨S_{p}⟩], N ⊢ d ⇒ S′_{q}, Q′ \\ & ∧ π⟨∃Q.S_{q}⟩ ≡^{α} ∃Q′.S′_{q} \end{aligned}

Suppose C WF (vi) and consider an arbitrary N with C, N rigid (vii). We need to show:

∃M, S. C, N ⊢ structure x = se; d ⇒ S, M ∧ ∃P ∪ Q.[x : S_{p}]S_{q} ≡^{α} ∃M.S

From induction hypothesis (iv) we obtain a P′ and S′_{p} satisfying:

C, N ⊢ se ⇒ S′_{p}, P′ (viii)  ∃P.S_{p} ≡^{α} ∃P′.S′_{p} (ix)

Hence we must have [P′/P]⟨S_{p}⟩ ≡ S′_{p} (x) for some bijective renaming [P′/P]. Clearly (vi) extends to C[x : [P′/P]⟨S_{p}⟩] WF (xi). Lemma 7 on (vi) and (i) establishes FN(∃P.S_{p}) ⊆ FN(C) (xii). From (ix) and (vii) it follows that FN([P′/P]⟨S_{p}⟩) ⊆ N ∪ P′ and thus C[x : [P′/P]⟨S_{p}⟩], N ∪ P′ rigid. We are now in a position to apply induction hypotheses (v) to the renaming [P′/P] resulting in a Q′ and S′_{q} with:

C[x : S′_{p}], N ∪ P′ ⊢ d ⇒ S′_{q}, Q′ (xiii)  [P′/P]⟨∃Q.S_{q}⟩ ≡^{α} ∃Q′.S′_{q} (xiv)

Rule (E-4) on (viii) and (xiii) derives:

C, N ⊢ structure x = se; d ⇒ [x : S′_{p}]S′_{q}, P′ ∪ Q′  (xv)

We still need to show ∃P ∪ Q.[x : S_{p}]S_{q} ≡^{α} ∃P′ ∪ Q′.[x : S′_{p}]S′_{q}.

First, observe that FN(S_{p}) ⊆ FN(C) ∪ P by (xii). Applying premise (iii) to the identity renaming on P yields C[x : S_{p}] ⊢′ d : ∃Q.S_{q}. An application of Lemma 7 yields FN(S_{q}) ⊆ FN(C) ∪ P ∪ Q (since (vi) extends to C[x : S_{p}] WF). Using equations (ix) and (xiv) one easily obtains FN(S′_{p}) ⊆ FN(C)∪P′ and FN(S′_{q}) ⊆ FN(C)∪P′ ∪ Q′. Moreover, Property 1 of (viii) together with (vii) ensures Q′ ∩ (FN(C) ∪ P′) = ∅. Now choose a “fresh” bijective renaming [Q̂/Q] with Q̂ ∩ (P ∪ P′ ∪ Q ∪ Q′ ∪ FN(C)) = ∅. Then it is easy to see that

∃Q.S_{q} ≡^{α} ∃Q̂.[Q̂/Q]⟨S_{q}⟩

and consequently

∃Q′.S′_{q} ≡^{α} [P′/P]⟨∃Q.S_{q}⟩
≡^{α} [P′/P]⟨∃Q̂.[Q̂/Q]⟨S_{q}⟩⟩

≡^{α} ∃Q̂.[P′/P]⟨[Q̂/Q]⟨S_{q}⟩⟩.

Hence there is a bijection [Q′/Q̂] such that S′_{q} ≡ [Q′/Q̂]⟨[P′/P]⟨[Q̂/Q]⟨S_{q}⟩⟩⟩. With these observations, it is easy to show:

∃P ∪ Q.[x : S_{p}]S_{q} ≡^{α} ∃P ∪ Q̂.[x : [Q̂/Q]⟨S_{p}⟩][Q̂/Q]⟨S_{q}⟩
≡ ∃P ∪ Q̂.[x : S_{p}][Q̂/Q]⟨S_{q}⟩
≡^{α} ∃P′ ∪ Q̂.[x : [P′/P]⟨S_{p}⟩][P′/P]⟨[Q̂/Q]⟨S_{q}⟩⟩
≡ ∃P′ ∪ Q̂.[x : S′_{p}][P′/P]⟨[Q̂/Q]⟨S_{q}⟩⟩
≡^{α} ∃P′ ∪ Q′.[x : [Q′/Q̂]⟨S′_{p}⟩][Q′/Q̂]⟨[P′/P]⟨[Q̂/Q]⟨S_{q}⟩⟩⟩
≡ ∃P′ ∪ Q′.[x : S′_{p}]S′_{q}

Choosing M =^{def} P′ ∪ Q′ and S =^{def} [x : S′_{p}]S′_{q} yields the desired result.

6 Contribution

Theorem 4 is essentially an equivalence result. However, we feel that the type theoretic presentation of the static semantics provides a better conceptual understanding of the type structure of Standard ML. To illustrate, we will briefly consider some extensions of the static semantics. They are readily suggested by the type system in Figure 4, but, in the author’s view, are less apparent from the elaboration semantics. We make no formal claim of type security for these extensions, but conjecture them to be sound [16].

6.1 Projections from Arbitrary Structure Expressions

At the moment, projections of type and structure components from structures are restricted to the case where we are projecting from a structure path sp. We can lift this restriction, as long as we ensure that hypothetical types do not escape their scope. Consider adding the structure expression se.x and replacing the type expression sp.t by se.t. The rules are simple to state:

\begin{matrix}C ⊢ se : ∃P.S′ & S′(x) = S \\ C ⊢ se.x : ∃P.S \end{matrix} \begin{aligned}C ⊢ se : ∃P.S & S(t) = τ & P ∩ FN(τ) = ∅ \\ & C ⊢ se.t ▷ τ \end{aligned}

For example, we now allow functor applications to appear in type expressions, as long as this does not require an abstract type to escape its scope. The extension is complete for programs in the original system: a path always type-checks to an existential structure with an empty quantifier so we are free to project any of its type components without violating P ∩ FN(τ) = ∅.

6.2 Applicative Functors

Although the Standard ML approach of generating fresh names for the datatypes returned by a functor at each application is sufficient to ensure type safety, it is certainly not necessary. One need only observe that, because of the absence of conditional module expressions, the generative types returned by a functor can at most depend on the types imported from the argument, but never on the run-time value of the argument. Roughly speaking, if we apply a functor to two arguments with equal type components but possibly differing value components, then the types created by the applications can safely be identified [8]. To capture this intuition, we first modify the rule for existential introduction, to take account of the fact that the new name δ depends on the free names {α_{1}, …, α_{n}} (n ≥ 0) of its definition τ. The dependency is expressed by parameterising δ by α_{1}, …, α_{n} in the bindings to t, in effect skolemising the existential variable [6]:

\begin{aligned}& & & Q ∩ \{δ, α_{1}, …, α_{n}\} = ∅ \\ C ⊢ te ▷ τ & \{α_{1}, …, α_{n}\} = FN(τ) & δ ∉ FN(C) & C[t = δ(α_{1}, …, α_{n})] ⊢ d : ∃Q.S \end{aligned}

C ⊢ datatype t = te; d : ∃{δ} ∪ Q.[t = δ(α_{1}, …, α_{n})]S

Typically, the type names free in τ will just be the free names introduced by the elimination of existential quantifiers. However, after type checking the body of a functor, we discharge the parametric type names of the argument signature by universally quantifying them. With our modified rule for datatypes, all occurrences of existentials will be parameterised by the functor argument types on which they depend, allowing us to lift the existential from the functor result over the entire functor signature:

\begin{matrix}C ⊢ Sg ▷ ΛP.S_{p} & P ∩ FN(C) = ∅ & C[x : S_{p}] ⊢ se : ∃Q.S_{q} \\ Q ∩ (FN(C) ∪ P) = ∅ & C[f : ∀P.S_{p} → S_{q}] ⊢ d : ∃M.S & M ∩ Q = ∅ \end{matrix}

C ⊢ functor f (x : Sg) = se in d : ∃Q ∪ M.S

As an example, consider the sequence of declarations:

functorf(x : sig type t end) = struct datatype u = x.t
: ∀α.[t = α] → [u = δ(α)][v = γ]  datatype v = bool

end

in

structure x = f (struct type t = int end): [u = δ(int)][v = γ]; structure y = f (struct type t = bool end): [u = δ(bool)][v = γ]; structure z = f (struct type t = int end): [u = δ(int)][v = γ];

From the annotated semantic objects^{2} we can see that x.u = z.u, x.u ≠ y.u, x.u ≠ int, y.u ≠ bool and x.v = z.v = y.v. In the original system, the types would all be distinct. If we were to neglect the parameterisation of δ by α, then we would have x.u = y.u, which is unsound assuming int ≠ bool.

2δ and γ are fresh names

Since functors now return unquantified result structures instead of existential structures, we can simplify the functor signatures of Figure 1 to Φ or ∀N.S → S′ ∈ FunSig =^{def} NameSet ×(Str × Str). The required changes to Definition 6 and Rule (T-8) are easy and left to the reader.

6.3 Abstract Signature Constraints

Standard ML has a construct (se:Sg) which is used to curtail the visibility of components of se to those specified in the signature Sg. Consider generalising signature expressions so that they denote families of existential structures (L or ΛN.∃M.S ∈ Sig =^{def} NameSet × ExStr) and introduce a new form of type specification in signature bodies datatype t; D with corresponding rule:

C[t = α] ⊢ D ▷ ΛP.∃Q.S α ∉ FN(C) ∪ P ∪ Q
C ⊢ datatype t; D ▷ ΛP.∃{α} ∪ Q.[t = α]S

The required modifications to the existing rules for signature expressions are easy and left to the reader. For L ≡ ΛN.X′, define X ≤ L iff X ≡^{α} φ (X′) for some substitution φ with Dom(φ) = N. Similarly, for X ≡ ∃M.S′ define S ≤ X iff S ≡ φ (S′) for some substitution φ with Dom(φ) = M. Consider the generalised signature matching rule:

\begin{aligned}C ⊢ se : ∃P.S_{p} & C ⊢ Sg ▷ L & P ∩ FN(L) = ∅ & S_{p} ⪰ S & S ≤ ∃Q.S_{q} & ∃Q.S_{q} ≤ L \\ & & C ⊢ (se:Sg) : ∃P ∪ Q.S_{q} \end{aligned}

Matching a structure against a signature can hide both components (by only requiring S_{p} ⪰ S) and the identities of specified types (by the additional quantification over Q). Note that when L has the form ΛN.∃∅.S we obtain the rule of Standard ML which merely hides the accessibility of unspecified components, yet preserves all type identities. Interpreting the ML signature ΛN.S as the generalised signature Λ∅.∃N.S one obtains MacQueen’s notion of abstraction [14] (implemented in NJ/SML), which hides the identities of generic type components. We offer a mixture of the two.

Of course, we now admit richer specifications of the arguments to functors, since we can state that some of the type components are not just arbitrary but abstract. Correspondingly, functor signatures can be generalised to the form Φ or ∀N.X → X′ ∈ FunSig =^{def} NameSet ×(ExStr × ExStr). The natural generalisation of the functor declaration rule is to to disallow the functor from propagating (via its result) the existentially quantified types of the argument, providing a greater control over modularity: in essence, the functor is restricted to making only local use of the formal argument’s datatypes. The other changes to the rules are straightforward, although we should point out that the naive combination of applicative functors and generalised signature matching is unsound. Applying a signature constraint to the body of a functor may hide the dependencies of datatypes on parameters of the functor.

7 Related Work & Conclusion

The use of existential types for data abstraction was first explored in [15], but then rejected by MacQueen[10] as an inadequate explanation of SML modules. Instead, he suggested an account based on first-order dependent types which was expanded by Harper and Mitchell[4]. Unfortunately, static checking of dependently typed terms requires the evaluation of terms, which is undesirable in general-purpose programming languages[5]. More recent proposals [3, 7], based on the restricted use of dependent types, avoid this problem but bear little direct relationship to the semantics of SML. In the author’s view, the syntax of SML, allowing occurrences of structure identifiers within type expressions, is misleading: the actual semantic objects show no evidence of first-order dependencies. Our account of generativity can be compared to that of Leroy [7, 9, 8]. Where he uses the dot notation as the elimination form for existentials [2], we treat the issue of existential elimination and the dot notation separately. We do not require syntactic representations of abstract types and can therefore accommodate local declarations in the style of SML. Leroy’s notion of applicative functor is similar to ours, but admits fewer equalities between abstract types. Leroy’s calculus supports higher-order functors, which we have not addressed. Biswas [1] proposes an elegant higher-order extension of a semantics similar to ours. It does not handle generativity but the simplifications to functor signatures sketched in Section 6.2 combined with the generalised dot notation of Section 6.1 are compatible with his work, promising an account [16] of higher-order functors and abstract types without resorting to the heavy machinery of [11]. Since we use existential, not dependent types, it is also possible to consider relaxing the stratification between Core and Modules.

To summarise, we have provided an explanation of Standard ML type generativity in terms of existential quantification. Our account is novel in that it does not use first-order dependent types. We suggest that SML modules can be understood as a combination of polymorphism (functors), existential types (generativity), and a subtyping relation on structures (enrichment). We sketched proper extensions to the semantics based on these observations.

References

[1] Sandip K. Biswas. Higher-order functors with transparent signatures. In Proc. 22nd Symp. Principles of Prog. Lang., pages 154–163. ACM Press, 1995.

[2] Luca Cardelli and Xavier Leroy. Abstract types and the dot notation. In IFIP TC2 working conference on programming concepts and methods, 1990.

[3] Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In 21st ACM Symp. Principles of Prog. Lang., 1994.

[4] Robert Harper and John C Mitchell. On the type structure of Standard ML. In ACM Trans. Prog. Lang. Syst., volume 15(2), pages 211–252, 1993.

[5] Robert Harper, John C Mitchell, and Eugenio Moggi. Higher-order modules and the phase distinction. Technical Report ECS-LFCS-90-112, Department of Computer Science, University of Edinburgh, April 1990.

[6] Stefan Kahrs. First-class polymorphism for ML. In Europ. Symp. on Programming Languages and Systems, 1994.

[7] Xavier Leroy. Manifest types, modules, and separate compilation. In Proc. 21st Symp. Principles of Prog. Lang., pages 109–122. ACM press, 1994.

[8] Xavier Leroy. Applicative functors and fully transparent higher-order modules. In Proc. 22nd Symp. Principles of Prog. Lang., pages 142–153. ACM Press, 1995.

[9] Xavier Leroy. A syntactic theory of type generativity and sharing. To appear in Journal of Functional Programming., 1995.

[10] David MacQueen. Using dependent types to express modular structure. In 13th ACM Symp. on Principles of Prog. Lang., 1986.

[11] David MacQueen and Mads Tofte. A semantics for higher-order functors. In Donald Sannella, editor, Programming Languages and Systems - ESOP ’94, volume 788 of LNCS. Springer Verlag, 1994.

[12] James McKinna and Robert Pollack. Pure Type Sytems formalized. In Proc. Int’l Conf. on Typed Lambda Calculi and Applications, Utrecht, pages 289–305, 1993.

[13] Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, 1990.

[14] Robing Milner and Mads Tofte. Commentary on Standard ML. MIT Press, 1991.

[15] John C Mitchell and Gordon D Plotkin. Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3):470–502, July 1988.

[16] Claudio V. Russo. Types for program modules. PhD thesis, Uni. of Edinburgh, forthcoming in 1996.