![[BACK]](/cvsweb/icons/back.gif){kind=icon}
Return to paper.ms CVS log ![[TXT]](/cvsweb/icons/text.gif){kind=icon}
![[DIR]](/cvsweb/icons/dir.gif){kind=icon}
Up to [Research Unix] / researchv10no / cmd / sml / doc / papers / modimp|
Return to paper.ms CVS log | Up to [Research Unix] / researchv10no / cmd / sml / doc / papers / modimp |
1.1 root 1: .RP
2: .ND March 11, 1988
3: .TL
4: An Implementation of Standard ML Modules
5: .AU
6: David MacQueen
7: .AI
8: AT&T Bell Laboratories
9: Murray Hill, NJ 07974
10: .AB
11: Standard ML includes a set of module constructs that support
12: programming in the large. These constructs extend ML's basic
13: polymorphic type system by introducing the dependent types of Martin
14: L\o'o"'f's Intuitionistic Type Theory. This paper discusses the
15: problems involved in implementing Standard ML's modules and describes
16: a practical, efficient solution to these problems. The
17: representations and algorithms of this implementation were inspired by
18: a detailed formal semantics of Standard ML developed by Milner, Tofte,
19: and Harper. The implementation is part of a new Standard ML compiler
20: that is written in Standard ML using the module system.
21: .AE
22: .EQ
23: delim %%
24: .EN
25: .de M1 \" start of a program display
26: .DS
27: .ft CW
28: ..
29: .de M2
30: .ft R
31: .DE
32: ..
33: .de M3
34: .if "\\$2"" \\&\f(CW\\$1\f1
35: .if !"\\$2"" \\&\f(CW\\$1\f1\\&\\$2
36: ..
37: .fp 5 CW
38: .NH
39: Introduction
40: .PP
41: An important part of the revision of ML that led to
42: the Standard ML language was the inclusion of module
43: facilities for the support of ``programming in the large.''
44: The design of these facilities went through several
45: versions [8] and was supported by concurrent investigations
46: of the type theory of ML and related systems [9,11].
47: The central idea behind the design was to support modularity
48: by introducing a stratified system of dependent types as suggested
49: by Martin L\o'o"'f's Intuitionistic Type Theory [10].
50: In late 1985 Bob Harper added a prototype implementation of
51: most of the module facilities to the Edinburgh ML compiler,
52: which was serving as a test-bed for the evolving Standard ML design.
53: .PP
54: Starting in the spring of 1986, Andrew Appel, Trevor Jim, and I have
55: implemented a new Standard ML compiler, written in Standard ML,
56: and initially bootstrapped from the Edinburgh compiler. An overview of
57: this new compiler, known as Standard ML of New Jersey, is given in [1].
58: The implementation of modules in this new compiler went through
59: two generations.
60: A first version was done in the fall of 1986, but it was completely
61: rewritten in the summer of 1987 following discussions of the
62: operational static semantics of modules with Robin Milner, Mads Tofte,
63: and Bob Harper [6,7,12].
64: Like Harper's prototype implementation, the new modules implementation
65: was inspired by the static semantics, but it uses a \fIstructure sharing\fP
66: strategy [3,13]
67: to avoid serious performance problems associated with a naive
68: implementation of the static semantics.
69: Although precise comparative measurements are not yet available, our
70: experience shows that the symbol table size for a large ML program
71: such as the ML compiler is several times smaller with the
72: new compiler than with the old compiler.
73: .PP
74: The objective of this paper is to describe our implementation of the
75: Standard ML module facilities, with particular emphasis on the
76: techniques used to minimize the space consumed by static representations
77: of modules (\fIi.e.\fP symbol table structures).
78: We begin by reviewing the elements of the module language.
79: .NH
80: Summary of the module constructs
81: .PP
82: Before describing the basic issues concerning implementation
83: of Standard ML modules, we need to review the main elements
84: of the module language.
85: There are three principal notions:
86: .in .3i
87: .IP (1)
88: \f2signature\f1 \- interface specification or ``type'' of modules.
89: .IP (2)
90: \f2structure\f1 \- an environment; a collection of type,
91: structure, value, and exception bindings; corresponds to
92: the conventional idea of a module.
93: .IP (3)
94: \f2functor\f1 \- function mapping structures to structures;
95: a form of parametric module.
96: .in -0.3i
97: .LP
98: Figure 1 below contains simple examples of each of these constructs.
99: .M1
100: signature ORD =
101: sig
102: type t
103: val le : t*t -> bool
104: end
105:
106: structure S =
107: struct
108: datatype t = A | B of t
109: val x = A
110: fun le(A,_) = true
111: | le(_,A) = false
112: | le(B x, B y) = le(x,y)
113: end
114:
115: signature LEXORD =
116: sig
117: structure A : ORD
118: val lexord : A.t list * A.t list -> bool
119: end
120:
121: functor LexOrd(O: ORD) : LEXORD =
122: struct
123: structure A = O
124: fun lexord([],_) = true
125: | lexord(_,[]) = false
126: | lexord(x::l,y::m) = ... O.le(x,y) ...
127: end
128:
129: structure LS = LexOrd(S)
130: .M2
131: .tl ''\f2Figure 1\f1''
132: .PP
133: This example contains declarations of two signatures,
134: .M3 ORD
135: and
136: .M3 LEXORD ,
137: two structures,
138: .M3 S
139: and
140: .M3 LS ,
141: and one functor,
142: \&\f5LexOrd\fP, mapping a structure of signature \&\f5ORD\fP
143: to a new structure of signature \&\f5LEXORD\fP.
144: The structure
145: .M3 LS
146: is defined as the result of applying
147: .M3 LexOrd
148: to
149: .M3 S .
150: We refer to components of a structure using qualified names or
151: paths formed with the usual ``dot'' notation: \fIe.g.\fP \&\f5S.t\fP,
152: \&\f5S.x\fP, \&\f5LS.A.le\fP.
153: .PP
154: A signature can be regarded as a form of ``type''
155: for structures, or as a schematic representation
156: of a class of structures, and a
157: structure \f2matches\f1 a signature if it satisfies the specifications
158: given in the signature. A structure does not have to agree exactly with
159: a signature in order for it to match the signature;
160: in this example the structure
161: .M3 S
162: matches the signature
163: .M3 ORD ,
164: even though
165: .M3 S
166: has an additional value component
167: .M3 x
168: not specified in
169: .M3 ORD .
170: In such cases signature matching has a coercive
171: effect, producing a ``thinned'' structure that exactly
172: agrees with the signature in terms of number of
173: components and their types.
174: .PP
175: Signature matching is performed in two contexts:
176: (1) when a signature constraint is given in a structure
177: declaration, as in:
178: .M1
179: structure R : ORD = S
180: .M2
181: and (2) when a functor is applied to an argument structure,
182: which must match the signature specified for the formal
183: parameter, as in
184: .M1
185: structure LS = LexOrd(S)
186: .M2
187: where
188: .M3 S
189: must match
190: .M3 ORD .
191: Actually, these two contexts are closely related under Landin's
192: principle of correspondence. In the first case, \&\f5R\fP is bound
193: to a thinned version of \&\f5S\fP that does not contain an \&\f5x\fP
194: component, and in the second case, the formal parameter \&\f5O\fP, and hence
195: the substructure \&\f5LS.A\fP, is also bound to a thinned version of \&\f5S\fP.
196: .PP
197: Another kind of specification that may appear in signatures
198: is the \f2sharing constraint\f1, the purpose of which is to
199: insure a kind of type coherence among functor parameters.
200: The program sketch in Figure 2 illustrates the use of sharing constraints.
201: .M1
202: signature SYMBOL = sig type symbol ... end
203:
204: signature LEX =
205: sig
206: structure Symbol : SYMBOL
207: val next : unit -> Symbol.symbol
208: ...
209: end
210:
211: signature SYMBOLTABLE =
212: sig
213: structure Symbol : SYMBOL
214: type var
215: val bind : Symbol.symbol * var -> unit
216: ...
217: end
218:
219: signature PARSE_ARGS =
220: sig
221: structure Lex : LEX
222: structure SymTab : SYMBOLTABLE
223: sharing Lex.Symbol = SymTab.Symbol
224: end
225:
226: functor Parse(A: PARSE_ARGS) =
227: struct ... A.SymTab.bind(A.Lex.next(), v) ... end
228: .M2
229: .tl ''\f2Figure 2\f1''
230: .PP
231: The functor
232: .M3 Parse
233: essentially takes two structure arguments,
234: .M3 Lex
235: (implementing a lexical analyzer) and
236: .M3 SymTab
237: (implementing a symbol table), which are bundled as components
238: of a single parameter structure.
239: The sharing specification in
240: .M3 PARSE_ARGS
241: requires that the same
242: .M3 Symbol
243: structure be used in both
244: .M3 Lex
245: and
246: .M3 SymTab .
247: This insures that
248: .M3 Lex
249: and
250: .M3 SymTab
251: can consistently interact, as in the expression
252: .M3 "A.Symtab.bind(A.Lex.next(),v)" ,
253: which is well-typed only if
254: .M3 A.Lex.Symbol.symbol
255: and
256: .M3 A.Symtab.Symbol.symbol
257: are the same type.
258: .PP
259: An important point about datatype and structure declarations
260: is that they are \f2generative\f1, meaning
261: that each time they are elaborated (\fIe.g.\fP in a functor body as a result
262: of functor applications) a new, distinct structure or type is created.
263: For example, in
264: .M1
265: functor F () =
266: struct
267: datatype t = A | B of t
268: end
269:
270: structure S1 = F()
271: structure S2 = F()
272: .M2
273: .M3 S1
274: and
275: .M3 S2
276: are distinct structures and
277: .M3 S1.t
278: and
279: .M3 S2.t
280: are distinct types, so
281: .M3 S1.B(S2.A)
282: is an ill-typed expression.
283: .PP
284: On the other hand, simple type definitions (whether occurring inside or
285: outside of structures) are \f2transparent\f1 rather than generative.
286: For instance, in
287: .M1
288: structure IntOrd =
289: struct
290: type t = int
291: fun le(x,y) = x <= y
292: end
293: .M2
294: the type
295: .M3 S.t
296: is identical to \&\f5int\fP.
297: In other words, there is no information hiding or abstraction
298: inherent in the formation of structures.
299: This applies even to the results of functor applications; type
300: information is propagated through functor applications, so that after
301: the declaration
302: .M1
303: structure IntLexOrd = LexOrd (IntOrd)
304: .M2
305: .M3 IntLexOrd.le
306: has type
307: .M3 "int list * int list -> bool" .
308: This reflects the dependent product nature of functor signatures, and
309: the fact that structures represent a form of \fIstrong\fP dependent sum
310: (see [9,11] for discussion of the relation between ML modules and dependent
311: types).
312: .NH
313: Implementation of modules
314: .PP
315: The principal tasks that an implementation must deal with are as follows:
316: .IP (1)
317: representation of signatures, structures, and functors.
318: .IP (2)
319: signature matching, including instantiation of the signature
320: template and possible thinning of the matched structure.
321: .IP (3)
322: functor application, including
323: .RS
324: .IP (a)
325: matching formal signature to actual parameter, with possible thinning
326: of the parameter.
327: .IP (b)
328: creation of the result structure, including propagation of type information from
329: parameter to result and generation of new instances of datatypes and
330: structures.
331: .RE
332: .IP (4)
333: representation and checking of sharing constraints.
334: .PP
335: Most of these tasks have two parts, the \f2static\f1 or compile-time
336: task and the \f2dynamic\f1 or run-time task.
337: The run-time problems are straightforward and are discussed in the
338: next subsection.
339: Our main focus will be on the static aspects of the module language,
340: for which our principal implementation goals are:
341: .IP (1)
342: compact representation of structures having a given signature
343: .IP (2)
344: efficient signature matching and functor application, with minimal
345: duplication of static (\fIi.e.\fP symbol table) information
346: .IP (3)
347: efficient representation and checking of sharing constraints.
348: .NH 2
349: Dynamic representations and processes.
350: .PP
351: The run-time representations of modules are remarkably simple [1].
352: Signatures and types have no run-time representation \(em they exist
353: only at the static level. A structure is represented as a record
354: whose components represent the dynamic
355: structure components (\fIi.e.\fP substructures, values, and exceptions) in a
356: canonical order. A functor is represented as an ordinary function
357: closure, and functor application corresponds to the normal application
358: of this function to a record representing the argument structure. The
359: thinning coercions associated with signature matching give rise to
360: in-line code to construct the thinned record.
361: .PP
362: In the middle-end of the compiler, all module constructs are reduced
363: to the same simple lambda-calculus based intermediate language that is
364: used for the core ML constructs of value declarations and expressions.
365: In effect, the back-end of the compiler is unaware of the existence of
366: the module constructs \(em they have been reduced to common notions of
367: records and functions.
368: .NH 2
369: Static Representations
370: .PP
371: A naive representation of signatures and structures can be modeled
372: more or less directly on the semantic constructs used in the operational static
373: semantics [5,6].
374: There a structure is modeled by an environment %E%
375: that maps component identifiers to the appropriate sort of
376: static binding (type, structure, variable, etc.), and a
377: \fIstamp\fP,* %n%, that uniquely identifies the structure:
378: %str^=^(n,E)%.
379: .FS
380: *We prefer the term ``stamp'' for this purpose, rather than the term
381: ``name'' used in [6,7],
382: since ``name'' could also refer to the identifier to which a structure
383: is bound or an identifier bound within a structure.
384: .FE
385: We can view a structure as a tree or dag with nodes labeled by stamps
386: and edges labeled by component names.
387: A signature is then a structure together with a designated set of
388: \fIbound\fP or \fIschematic\fP stamps occurring within the structure:
389: %sig^=^(N)(n,E)%.
390: .PP
391: We illustrate this with the definitions in Figure 3
392: and the corresponding graphs in Figure 4 (adapted from [6]), in which
393: \fI(a)\fP represents the structure \&\f5C\fP and \fI(b)\fP represents
394: the signature \&\f5SIGC\fP.
395: Our convention for distinguishing between constant and bound stamps
396: is that metavariables %k sub i%
397: range over constant stamps, while metavariables %x sub i% range over
398: bound stamps in a signature. This is a more concise alternative to the
399: separate specification of the graph and the set of bound stamps
400: We emphasize the distinction by using solid
401: circles for nodes with constant stamps and open circles for nodes with
402: bound stamps.
403: A structure will always contain only constant
404: stamps, while a signature will typically contain only bound stamps. The
405: graphs are simplified by showing only structure components, but type
406: components are dealt with similarly.
407:
408: .DS
409: .ft 5
410: .ta 3i
411: structure A = signature SIGA =
412: struct sig
413: type t = int type t
414: fun f n = 2 * n val f : t -> t
415: end end
416:
417: structure B = signature SIGB =
418: struct sig
419: structure BA = A structure BA: SIGA
420: fun g x = BA.f(x) + 1 val g: BA.t -> BA.t
421: end end
422:
423: structure C = signature SIGC =
424: struct sig
425: structure CA = A structure CA : SIGA
426: structure CB = B structure CB : SIGB
427: fun h x = CB.g(CA.f x) val h: CA.t -> CA.t
428: end end
429: .ft R
430: .DE
431: .tl ''\f2Figure 3\f1''
432: .PS
433: circlerad = 0.05i
434: define str '
435: {C1: circle
436: move to C1
437: move down right
438: C2: circle
439: move to C2
440: move down left
441: C3: circle
442: A1: arrow from C1.c to C2.c chop
443: A2: arrow from C2.c to C3.c chop
444: A3: arrow from C1.c to C3.c chop
445: "%k sub 1% " at C1.w rjust
446: " %k sub 3%" at C2.e ljust
447: "%k sub 2% " at C3.w rjust
448: " CB" at A1.center ljust
449: " BA" at A2.center ljust
450: "CA " at A3.center rjust
451: move to C1
452: move down 1.3i
453: "\f5structure C\fR" center
454: }
455: '
456: define sig '
457: {C1: circle
458: move to C1
459: move down left
460: C2: circle
461: move to C1
462: move down right
463: C3: circle
464: move to C3
465: move down
466: C4: circle
467: A1: arrow from C1.c to C2.c chop
468: A2: arrow from C1.c to C3.c chop
469: A3: arrow from C3.c to C4.c chop
470: " %x sub 1%" at C1.e ljust
471: "%x sub 2% " at C2.w rjust
472: " %x sub 3%" at C3.e ljust
473: " %x sub 4%" at C4.e ljust
474: "CA " at A1.center rjust
475: " CB" at A2.center ljust
476: " BA" at A3.center ljust
477: move to C1
478: move down 1.3i
479: "\f5signature SIGC\fR" center
480: }
481: '
482: H: str; move to H; move right 2.25i; sig
483: .PE
484: .tl ''\f2Figure 4\f1''
485:
486: .PP
487: The purpose of a signature matching \&\f5S: SIG\fP is to produce a
488: structure \&\f5S'\fP that has exactly the form specified by
489: \&\f5SIG\fP and yet shares the identity (\fIi.e.\fP the stamps) of
490: \&\f5S\fP. In some cases, \&\f5S\fP and \&\f5S'\fP are identical, as
491: when \&\f5S\fP had already matched the signature \&\f5SIG\fP. In
492: other cases \&\f5S'\fP is a thinned version of \&\f5S\fP having fewer
493: components or components whose types are generic instances of their
494: types in \&\f5S\fP. Another product of matching is the realization
495: map, whose use in functor applications is explained in Section 3.5.
496: .PP
497: We can think of \&\f5SIG\fP as a scheme analogous to a generic type scheme or
498: polytype in the core ML type system [4], with the bound stamps
499: playing the role of generic type variables in a type scheme. The
500: product of matching is then an instance of this scheme under the
501: substitution represented by the realization map. The details of this
502: analogy have been worked out by Mads Tofte, including a version of the
503: principal typing theorem of [4].
504: .PP
505: A naive implementation of matching would make a copy of the signature
506: \&\f5SIG\fP, in the process replacing each bound stamp by the corresponding
507: constant stamp from \&\f5S\fP. This would involve copying most of the
508: environment part of the signature, since we have to instantiate the
509: type specifications of values and exceptions as well as instantiating
510: the types and substructures themselves. However, the environment or
511: symbol table part of the signature can be regarded as a template
512: relative to its type and substructure components, which are the only
513: parts that need to change during signature matching. For instance, a
514: type specification like \&\f5f: t->t\fP can remain fixed if it is interpreted
515: relative to the type component \&\f5t\fP. We can abstract out the type and
516: structure components carrying the bound stamps and use the rest of the
517: information in a signature as an unchanging template that can be
518: shared by all instances of the signature. This is the familiar
519: \fIstructure sharing\fP idea first proposed by Boyer and Moore in the
520: context of resolution theorem proving [3] and later exploited in the
521: implementation of Prolog [13]. The use of structure sharing in
522: the basic ML type system has been considered, but in that context it
523: does not appear to have a clear advantage over the simpler approach of
524: instantiation by copying. In the case of signature matching, however,
525: the shared information in the template is typically of considerable
526: volume, so structure sharing is quite effective in saving space
527: relative to copying.
528: .PP
529: The definitions of the basic datatypes used to represent type
530: constructors, structures and signatures are given in Figure 5. The
531: representations of structures and signatures both use the \&\f5Structure\fP
532: datatype, and differ only in the value of the \&\f5kind\fP field. The \&\f5stamp\fP
533: field contains the identifying stamp, the \&\f5table\fP is the environment
534: component represented as a hash table mapping symbols to the various
535: sorts of bindings, and the \&\f5env\fP field contains a pair of instance
536: vectors for type and structure components. The \&\f5sign\fP field in
537: a signature to identify the signature (the \&\f5stamp\fP field
538: will have a formal value representing a bound stamp); in
539: a structure it identifies the signature the structure is an instantiation of,
540: if any. Bound and constant stamps are both represented as integers;
541: stamps greater than some base value are constant stamps, while stamps
542: less than that value are bound. Within a given signature, bound
543: stamps are canonically numbered starting from 0.
544: .M1
545: datatype tycon
546: = TYCON of {stamp : stamp, ...}
547: | INDtyc of int list
548:
549: datatype Structure
550: = STRstr of
551: {stamp : stamp,
552: sign : stamp option,
553: table : symtable,
554: env : strenv,
555: kind : strkind}
556: | INDstr of int
557:
558: and strkind
559: = STRkind
560: | SIGkind of
561: {share : sharespec,
562: bindings : binding list,
563: stampcounts : {s : int, t : int}}
564: .M2
565: .tl ''\f2Figure 5\f1''
566:
567: .PP
568: The \&\f5INDtyc\fP and \&\f5INDstr\fP forms of type constructors and structures are
569: used within the symbol table to refer indirectly to components stored
570: in the instance vectors. The term \&\f5INDtyc[%i%]\fR refers to the ith
571: element of the type instance vector, while \&\f5INDtyc[%i%,%j%]\fR refers to the
572: jth element of the type vector of the ith element of the structure
573: vector. The type specifications
574: .M1
575: f: t -> t
576: h: CA.t -> CA.t
577: .M2
578: from Figure 3 are represented internally as
579: .M1
580: f: INDtyc[0] -> INDtyc[0]
581: h: INDtyc[0,0] -> INDtyc[0,0]
582: .M2
583: The representation of the entire signature SIGC from Figure 3 can be
584: summarized as follows:
585: .M1
586: SIGC:
587: stamp: 0
588: table: CA => INDstr 0
589: CB => INDstr 1
590: h => VAR: INDtyc[0,0] -> INDtyc[0,0]
591: strenv: structures = <SIGA',SIGB'>
592: types = <>
593:
594: SIGA':
595: stamp: 1
596: table: t => INDtyc[0]
597: f => VAR: INDtyc[0] -> INDtyc[0]
598: strenv: structures = <>
599: types = <DUMMY 0>
600:
601: .M2
602: .M1
603: SIGB':
604: stamp: 2
605: table: BA => INDstr 0
606: g => VAR: BA.t -> BA.t
607: strenv: structures = <SIGA''>
608: types = <>
609:
610: SIGA'':
611: stamp: 3
612: table: t => INDtyc[0]
613: f => VAR: INDtyc[0] -> INDtyc[0]
614: strenv: structures = <>
615: types = <DUMMY 1>
616: .M2
617: .LP
618: Note that there are two copies of the signature \&\f5SIGA\fP, identified
619: as \&\f5SIGA'\fP and \&\f5SIGA''\fP, each with its own stamp. This
620: duplication is required to get the canonical numbering of stamps for
621: each component of \&\f5SIGC\fP, but each of these copies shares the
622: original symbol table component from \&\f5SIGA\fP. \&\f5DUMMY 0\fP
623: and \&\f5DUMMY 1\fP are dummy type constructor components, which have
624: their own separate numbering within the context of \&\f5SIGC\fP.
625: .NH 2
626: Signature Matching
627: .PP
628: We now describe the process of signature matching in terms of the
629: representation described above. Given a signature \&\f5sig\fP and
630: structure \&\f5str\fP represented as
631: .M1
632: sig = STRstr{stamp = x, sign = n, table = sigtab, env = sigenv,
633: kind = SIGkind{bindings,stampcounts,sharing}}
634:
635: str = STRstr{stamp = k, sign = s, table = strtab, env = strenv,
636: kind=STRkind}
637: .M2
638: we first check whether \&\f5s=n\fP , and if so
639: return \&\f5str\fP, because \&\f5str\fP is already an instance of
640: \&\f5sig\fP. Otherwise we attempt to construct a new instance of
641: \&\f5sig\fP. We start by allocating a new pair of instance vectors,
642: \&\f5newenv={s=sNew,t=tNew}\fP, based on the size information in the
643: \&\f5stampcounts\fP field. Then we iterate through the list of all
644: of \&\f5sig\fP's bindings (\fIi.e.\fP specifications), which is
645: available in the field \&\f5bindings\fP. For each structure binding
646: \&\f5(id,INDstr i)\fP in \&\fIsig\fP, we look up a structure named
647: \&\fIid\fP in \&\f5strtab\fP. If it does not exist, matching fails.
648: If it does exist, we recursively match it against the substructure
649: signature bound to \&\f5id\fP in \&\f5sig\fP (obtained as the ith
650: element of the structure vector in \&\f5sigenv\fP), and if successful
651: use the result to define the ith element of \&\f5sNew\fP. Similarly
652: for type bindings, where we check that the type constructor bound in
653: \&\f5str\fP agrees with the specification in sig (\fIe.g.\fP they must have
654: the same arity). For value specifications like \&\f5x: ty\fP, we
655: interpret indirect type constructors in \&\f5ty\fP with respect to
656: \&\f5newenv\fP and check that we have a generic instance of the type
657: of the corresponding component of \&\f5str\fP. Checking value
658: components has no effect on the instance vectors, but if necessary
659: (\fIi.e.\fP if \&\f5sig\fP has fewer value components than
660: \&\f5str\fP) we calculate the translation between the old and new
661: runtime positions of the components and collect this information in a
662: thinning specification to be applied at runtime.
663: .PP
664: When we have successfully matched all the bindings in \&\f5sig\fP we build the
665: result structure
666: .M3 str\'
667: using
668: .M3 sig \'s
669: table and
670: .M3 sign ,
671: .M3 str \'s
672: stamp ,
673: and
674: .M3 newenv
675: .M1
676: str' = STRstr {stamp=n, sign=SOME k, table=sigtab,
677: env=newenv, kind=STRkind}
678: .M2
679: Finally any sharing constraints (from sharing) are checked as
680: described in Section 3.5, and we return \&\f5str'\fP and a thinning
681: specification as the result of the match. Note that
682: the bulk of the information in the signature is in
683: .M3 sigtab ,
684: and this is directly shared with the instantiation
685: .M3 str\' .
686: .PP
687: As a shortcut, when elaborating a declaration like
688: .M1
689: structure S: SIG = struct \fIdeclarations\fP end
690: .M2
691: we do not build the structure on the right-hand side before doing
692: the signature match. Instead we elaborate the body declarations in
693: the top-level environment and then do the signature matching using
694: the top-level environment in the place of the target structure.
695: .NH 2
696: Functors and functor application
697: .PP
698: In the static semantics a functor %F% is modeled by a pair of
699: structures representing the parameter and body of the functor, and
700: two sets of bound stamps.
701: .EQ I
702: F ~ = ~ ( N ) ( S sub p , ^ ( N ' ) S sub b )
703: .EN
704: %N% is the set of bound stamps in the parameter structure, which may
705: also occur in the body %S sub b%, while %N '%
706: is the set of stamps associated with generative elements of the
707: functor body. To apply %F% to an argument structure %A% we perform
708: the following steps
709: .EQ I
710: r ~ = ~ match ( ( N ) S sub p , ^ A )
711: .EN
712: .EQ I
713: g ~ = ~ generate ( N ' )
714: .EN
715: .EQ I
716: F ( A ) ~ = ~ g ( r ( S sub b ) )
717: .EN
718: That is, we match the parameter signature and the argument to produce
719: a realization map %r%, then we generate a realization map %g% that maps
720: each bound stamp in %N '% to a unique, new constant stamp, and finally
721: we produce the result structure by using %r% and %g% to instantiate
722: the body structure.
723: .PP
724: The implementation of functors follows this scheme closely. The
725: datatype used to represent functors is defined by
726: .M1
727: datatype Functor = FUNCTOR of
728: {param : Structure,
729: body : Structure,
730: tycCount : int}
731: .M2
732: The bound stamps in the \&\f5param\fP structure are numbered from 0 to
733: %n% and these may also occur in the \&\f5body\fP structure.
734: Generative stamps in the body are numbered from %n+1% to %n+m%, which
735: is the value of \&\f5tycCount\fP.
736: .PP
737: If the functor declaration provides an explicit result signature, as in
738: .M1
739: functor F(X : SIGP) : SIGR = struct ... end
740: .M2
741: the body will naturally be schematic (i.e. the parts with bound stamps will
742: be isolated in instance vectors) as a result of the signature
743: matching between the body and the result signature. However, if there
744: is no result signature, we explicitly abstract these ``volatile'' parts of
745: the body structure to get an instantiable scheme so that the body's
746: symbol table may be shared by all structures produced by the functor.
747: .PP
748: To apply the functor, signature matching is performed between the
749: parameter signature and the argument to build a realization map for
750: the bound stamps in the parameter. Then the body is instantiated
751: using this realization map and introducing new constant stamps to
752: replace generative bound stamps as required. The actual algorithm
753: is more complicated than this because functor application can occur
754: within the body of functor declaration, as in
755: .M1
756: functor F(X : SIGP) =
757: struct
758: structure A = G(X)
759: structure B = H(A)
760: ...
761: end
762: .M2
763: In cases like the applications of \&\f5G\fP and \&\f5H\fP in this
764: example, the actual parameter may contain parameter bound and even
765: generatively bound stamps, and the realization of the generative
766: stamps in the body of \&\f5G\fP and \&\f5H\fP will themselves be
767: generatively bound stamps.
768: .NH 2
769: Sharing
770: .PP
771: The purpose of sharing constraints is to insure a kind of compatibility
772: between several parameter structures of a functor, as illustrated in
773: Figure 2. The sharing constraints are expressed as sets of equations
774: between paths designating structures or types (there are two kinds of
775: sharing specifications: structure sharing and type sharing) and they
776: determine an equivalence relation amongst the components of the
777: signature. The strategy for incorporating sharing constraints in the
778: representation of a signature is to force all components of an
779: equivalence class to have the same stamp.
780: .PP
781: Two components may be required to share either because they are
782: directly equated in a sharing specification, or because they are
783: corresponding components of structures that are required to share.
784: Thus if
785: .M1
786: X : sig
787: structure C1 : SIGC
788: structure C2 : SIGC
789: sharing C1.CB = C2.CB
790: end
791: .M2
792: then \&\f5X.C1.CB = X.C2.CB\fP is directly specified, and \&\f5X.C1.CB.BA =
793: X.C2.CB.BA\fP is an inferred consequence. This simply says that the
794: complete sharing relation must be a congruence with respect to the
795: operation of selecting a named substructure or type.
796: .PP
797: Under what circumstances may two structures be constrained to share?
798: They must be \fIconsistent\fP, in the sense that it is possible to
799: find a structure that could simultaneously match both of them. In
800: particular, the structures that are forced to share do not necessarily
801: have to share the same signature, and the fact that they share does
802: not have any effect on their signature. The idea is that various
803: thinned versions of a given structure may have different signatures,
804: but they can still share because they are actually restricted views
805: of their common ancestor structure. This approach is supported by the
806: fact that in signature matching, the stamps of the matched structure
807: are inherited by the resultant structure. Note that this is not the
808: approach described in [6], where signatures of sharing
809: structures are forced to agree by formation of a kind of union
810: signature. We do not actually verify that signatures that are
811: specified to share are consistent, but if they are not, the signature
812: containing the sharing specification can never be successfully matched.
813: .PP
814: The processing of the sharing constraints is performed in two stages.
815: First, a union-find algorithm is used to determine all sharing
816: relations, direct and inferred, and to construct the equivalence
817: classes for the sharing relation. At this stage it is also possible
818: to detect certain pathological sharing specifications, such as trying
819: to identify a structure with one of its substructures. Second, the
820: signature is copied and each element of a given equivalence class is
821: given the same representative stamp.
822: .PP
823: There are two ways in which sharing information is used. (1) When a
824: signature with sharing constraints is used as a functor parameter, the
825: identification of stamps in the signature will automatically insure
826: that the sharing has the desired effect during type checking, \fIi.e.\fP
827: types that are specified to share will be seen to be identical by the
828: type checker. (2) During signature matching, any sharing relations
829: specified in the signature must also hold in the matched structure.
830: One way to check this would be to make sure that the realization map
831: was well defined, because a failure of sharing in the target structure
832: would cause a single bound stamp to be mapped to more than one target
833: stamp. However, the realization map is only explicitly constructed in
834: the matching of functor parameters, where it is needed to help
835: instantiate the functor body. Hence it is more convenient to simply
836: save the original sharing constraints as equations in the signature
837: and check them explicitly in the target structure as part of signature
838: matching.
839: .NH 2
840: Relation with type checking
841: .PP
842: What is the relationship between the structures and signatures and the
843: underlying ML type checking mechanism? Obviously signatures and structures
844: are carriers of type information \(em that is one of their principle purposes.
845: When we look up a value component of a structure we get the same sort of bindings
846: as in the top-level environment, except that in some circumstances the
847: type has been relativized to the structure's instance vectors and it
848: contains \&\f5INDtyc\fP type constructors. The basic variable lookup
849: functions have been defined to eliminate these indirections by replacing
850: them with the referenced type constructors from the instance vectors,
851: at the expense of partially copying the type. This would appear to undo
852: some of the savings achieved by the structure sharing representation of
853: structures, but these copies tend to be ephemeral, and they are
854: quickly and efficiently garbage-collected. The type information in
855: structures and signatures is, on the other hand, long-lived, so it is
856: more critical to minimize their space requirements.
857: .NH
858: Conclusions
859: .PP
860: The challenge of implementing the Standard ML module features is to
861: perform the compile-time matchings and instantiations necessary to
862: propagate and check type information with a minimum of duplication of
863: that information. Experience has shown that a naive approach leads to
864: an explosion in the size of the static representations.
865: .PP
866: The implementation strategy described in this paper uses a structure
867: sharing instantiation technique instead of instantiation by copying,
868: and has proved to be reasonably modest in its space requirements. It
869: also has the advantage that it remains quite close in spirit to the
870: formal static semantics.
871: .PP
872: Work on the Standard ML module facilities continues, and current
873: topics of interest include explicit functor signatures and the relation
874: of the module constructs to separate compilation.
875: .SH
876: Acknowledgements
877: .PP
878: This implementation is inspired directly by the work done on the
879: operational semantics of Standard ML by Robin Milner, Mads Tofte, and
880: Bob Harper, and I have benefited from many discussions with them.
881: Bob Harper passed on useful ideas from his prototype implementation
882: of modules. Nick Rothwell helped me explore the use of structure sharing
883: in type checking. Andrew Appel provided valuable advice throughout and
884: had a direct hand in the implementation of sharing specifications, and
885: he has been an equal partner in the creation of Standard ML of New Jersey.
886: .SH
887: References
888: .IP 1.
889: A. Appel and D. MacQueen, \fIA Standard ML compiler\fP, Proceedings of the
890: Conference on Functional Programming and Computer Architecture, Portland,
891: September 1987, G. Kahn, ed., LNCS Vol. 274, Springer-Verlag, 1987.
892: .IP 2.
893: H.-J. Boehm and A. Demers, \fIImplementing Russell\fP,
894: Proceedings of SIGPLAN 86 Symposium on Compiler Construction, Palo Alto,
895: 1986, 186-195.
896: .IP 3.
897: R. S. Boyer and J Moore, \fIThe sharing of structure in theorem-proving
898: programs\fP, Machine Intelligence 7, B. Meltzer and D. Michie, eds., Edinburgh
899: University Press, 1972, 101-116.
900: .IP 4.
901: L. Damas and R. Milner, \fIPrincipal type schemes for functional programs\fP,
902: Proceedings of 9th ACM Symposium on Principles of Programming Languages,
903: Albuquerque, 1982, 207-212.
904: .IP 5.
905: R. Harper, D. MacQueen, and R. Milner, \fIStandard ML\fP, Laboratory for
906: Foundations of Computer Science, Dept. of Computer Science, University of
907: Edinburgh, ECS-LFCS-86-2, 1986. (Also Polymorphism II, 2, October 1985.)
908: .IP 6.
909: R. Harper, R. Milner, and M. Tofte, \fIA type discipline for program modules\fP,
910: Proceedings TAPSOFT 87, LNCS Vol. 250, Springer-Verlag, New York, 1987, 308-319.
911: .IP 7.
912: R. Harper, R. Milner, and M. Tofte, \fIThe semantics of Standard ML,
913: Version I\fP, Laboratory for Foundations of Computer Science, Dept. of
914: Computer Science, University of Edinburgh, ECS-LFCS-87-36, 1986.
915: .IP 8.
916: D. MacQueen, \fIModules for Standard ML\fP, in [5]. (An earlier version
917: appeared in Proceedings ACM Symposium on Lisp and Functional Programming,
918: Austin, 1984.)
919: .IP 9.
920: D. MacQueen, \fIUsing dependent types to express modular structure\fP,
921: Proceedings 13th ACM Symposium on Principles of Programming Languages, St.
922: Petersburg Beach, 1986, 277-286.
923: .IP 10.
924: P. Martin-L\o'o"'f, \fIConstructive mathematics and computer programming\fP,
925: Sixth International Congress for Logic, Methodology, and Philosophy of Science,
926: North Holland, Amsterdam, 1982, 153-175.
927: .IP 11.
928: J. C. Mitchell and R. Harper, \fIThe essence of ML\fP, Proceedings 15th
929: ACM Symposium on Principles of Programming Languages, San Diego, 1988,
930: 28-46.
931: .IP 12.
932: M. Tofte, Operational Semantics and Polymorphic Type Inference, Ph.D.
933: Dissertation, Dept. of Computer Science, University of Edinburgh, 1987.
934: .IP 13.
935: D. H. D. Warren, \fIImplementing PROLOG - Compiling Predicate Logic Programs,
936: Vol. I\fP, Dept. of Artificial Intelligence Report No. 39, University of
937: Edinburgh, 1977.
This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.