FIX: A Design for an Efficient Type/Region/Effect/Kind Checking System or Towards a Portable Scheme Implementation of FX-87

by

Michael Ross Blair

B.S., Massachusetts Institute of Technology (1986)

Submitted to the Department of Electrical Engineering and Computer Science in partial fulfillment of the requirements for the degree of

Master of Science in the field of Computer Science & Engineering

at the

MASSACHUSETTS INSTITUTE OF TECHNOLOGY

September 1990

Copyright \begin{matrix}c \\ ◯ \end{matrix} 1990 by Massachusetts Institute of Technology

Signature of Author . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Department of Electrical Engineering and Computer Science August 30, 1990

Certified by . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

David A. McAllester

Assistant Professor of Electrical Engineering & Computer Science Thesis Supervisor

Accepted by . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Arthur C. Smith

Chairman, Departmental Committee on Graduate Students

ii [This page intentionally left very nearly blank.]

FIX: A Design for an Efficient Type/Region/Effect/Kind Checking System or Towards a Portable Scheme Implementation of FX-87 by Michael Ross Blair

Submitted to the Department of Electrical Engineering and Computer Science on August 30, 1990 in partial fulfillment of the requirements for the degree of Master of Science in the field of Computer Science & Engineering

Abstract

Modern programming languages have adopted increasingly powerful compile-time analysis systems. This added power implies added compile-time complexity. Despite this, powerful static analysis systems can be incorporated into a compiler without adversely affecting its running time. This thesis is demonstrated by examining the algorithmic complexity of three aspects of a powerful compile-time analysis system.

First, a sophisticated system of type compatibility axioms is introduced. Using an implementation technique I call algorithmic complexity slicing, it is shown that the time needed to type check a value expression using these axioms can be made proportional to the inherent difficulty of type checking that particular expression, which is usually not equal to the worst-case computational complexity of the algebraic system of type compatibility axioms, where “type compatibility axioms” refers to axioms about the well-typedness of programs.

Second, the problem of inferring implied projections in applications of polymorphic procedures is examined. The inference of first-order projections is shown to be efficiently decided by a soundness-preserving reverse inference over the type compatibility axioms. This technique I call an abductive inference. All this is developed in the framework of the Type/Region/Effect/Kind system of the programming language FX-87, a statically typed dialect of Lisp.

Finally, the problem of discarding declarations of externally non-observable effects is examined. A semantics of FX-87 effect declarations is developed from which a set of rules for disregarding non-observable effects is derived. The resulting Effect Masking Rules are more effective and efficient than those prescribed by the FX-87 language specification.

Thesis Supervisor: David A. McAllester Title: Assistant Professor of Electrical Engineering & Computer Science iv

[This page intentionally left very nearly blank.]

Acknowledgments

As in any challenging project, I could not have done this thesis without the support and assistance of many dear friends. Although mere words cannot do justice to the appreciation I feel, I would at least like to acknowledge the following people:

First, my sincere thanks to David McAllester, my thesis advisor, for his patience, diligence, honesty, compassion, and his mastery of the foundations of this work. This thesis would be far less than it is had he not guided me in polishing my half-baked ideas. Still, of course, I bear sole responsibility for any errors remaining.

Guy Lewis Steele, Jr. and Gerald Jay Sussman, the two extraordinary persons who created Scheme, the language from which FX-87 was derived. I am continually amazed at the elegance of their creation.

For their funding and funning: Hal Abelson, Gerry Sussman, and Rishiyur Nikhil. They are not only three of the best educators at the Institute, they are also fun guys to hack with.

For their expertise in the design and implementation of FX-87, I thank FX-perts John Lucassen, Pierre Jouvelot, Mark Sheldon, and James O’Toole.

For listening to my half-baked ideas and providing me much constructive feedback on drafts of this thesis: Andy Ayers, Brian Bentz, Andrew Chien, Mark Day, David Gifford, Ricardo Jenez, Tom Knight, John Nguyen, James O’Toole, John Pezaris, Jonathan Rees, Mark Sheldon, and Franklyn Turbak. David Gifford also graciously funded early work on this thesis.

For motivating me to finish and for keeping alive my enthusiasm for the field: Simon L. Peyton-Jones, Philip Wadler, Luca Cardelli, and Paul Hudak.

For creating a wonderful environment in which to hack: the Computer Architecture Group (CAG), Project MAC (Mathematics and Computation), Programming Systems Research Group (PSRG), Project Dataflow, and the LCS/AI Reading Room staff.

For filling my life with music and keeping me company in the wee hours: National Public Radio member stations WGBH (89.7 FM) and WBUR (90.9 FM) Boston University and independent radio stations WERS (88.9 FM) Emerson College, WHRB (95.3 FM) Hahvahd University, WZBC (90.3 FM) Boston College, and WCRB (102.5 FM) Waltham.

Finally, and most importantly, my parents and family for their encouragement and unfailing support, and my extended family members: Sharon Thomas for her strength, Victoria Stettner for her warmth, and Brian and Mary-Anne Bentz for their friendship and understanding.

This thesis was developed primarily on a Texas Instruments Explorer Lisp machine using Jonathan Rees’ PseudoScheme and Donald E. Knuth and Leslie Lamport’s formatters TEX and LaTEX. Consequently, I thank Peter R. Nuth and Stephen Gildea for their LaTEX thesis macros, and John Wolfe, John Nguyen and John Pezaris for their TEX wizardry.

This research was supported in part by the Defense Advanced Research Projects Agency of the Department of Defense and was monitored by the Office of Naval Research under contract number N00014-83-K-0125.

vi [This page intentionally left very nearly blank.]

Contents

0 Thesis Overview 1 0.1 My Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 0.2 The Problem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

0.2.1 The Standard “Non-Standard” Approach . . . . . . . . . . . . . . . 3 0.2.2 A Less Standard “Non-Standard” Approach . . . . . . . . . . . . . . 3 0.2.3 A Non-“Non-Standard” Approach . . . . . . . . . . . . . . . . . . . 9

0.3 Additional Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 0.4 Concretization: Introduction to FIX . . . . . . . . . . . . . . . . . . . . . . 10

0.4.1 Focus and Scope . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 0.4.2 Goal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 0.4.3 Perspective . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 0.4.4 The Plot . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 0.4.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 0.4.6 Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

1 The Evolution and Essence of FX-87 15

1.1 Historical Overview of FX-87 . . . . . . . . . . . . . . . . . . . . . . . . . . 16

1.1.1 ALGOL 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
1.1.2 ALGOL 68 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
1.1.3 Pascal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

1.1.4 Euclid . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.1.5 Ada/CLU . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.1.6 Standard ML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 1.1.7 LS1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 1.1.8 Amber . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 1.1.9 Pebble . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 1.1.10 Scheme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

1.2 Why Static Analysis? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 1.3 Stratified Typing, and Effect Systems . . . . . . . . . . . . . . . . . . . . . 21

2 FX-87 Overview 23 2.1 ^{⟨⟨}Ce que c’est et ce que ce n’est pas^{⟩⟩}^{†} . . . . . . . . . . . . . . . . . . . . . 23 2.2 The FX-87 Language Grammar (Extended BNF) . . . . . . . . . . . . . . . 24 2.2.1 [Kinds] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.2.2 [Descriptions] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.2.3 [Values] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

†“FX-87: What it is and what it isn’t”

2.3 Description Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.3.1 [Basic Equivalence Axioms] . . . . . . . . . . . . . . . . . . . . . . . 26 2.3.2 [Region Equivalence] . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.3.3 [Effect Equivalence] . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.3.4 [Type Equivalence] . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.3.5 [Higher Order Description Equivalence] . . . . . . . . . . . . . . . . 27 2.3.6 [DLETREC Equivalence] . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.3.7 [Completeness of the Equivalence Axioms] . . . . . . . . . . . . . . . 28

2.4 Description Inclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2.4.1 [Basic Inclusion Axioms] . . . . . . . . . . . . . . . . . . . . . . . . . 28 2.4.2 [Inclusion Notational Convention] . . . . . . . . . . . . . . . . . . . . 29 2.4.3 [Region Inclusion] . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2.4.4 [Effect Inclusion] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2.4.5 [Type Inclusion] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2.4.6 [Higher Order Description Inclusion] . . . . . . . . . . . . . . . . . . 31 2.4.7 [DLETREC Inclusion] . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

2.5 Expression Type and Effect Inference . . . . . . . . . . . . . . . . . . . . . . 32 2.5.1 [Value Variable Type & Effect] . . . . . . . . . . . . . . . . . . . . . 32 2.5.2 [Implicit Description Inclusion] . . . . . . . . . . . . . . . . . . . . . 32 2.5.3 [IF Type & Effect] . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2.5.4 [λ Type & Effect] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 2.5.5 [Application Type & Effect] . . . . . . . . . . . . . . . . . . . . . . . 33 2.5.6 [Pλ Type & Effect] . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 2.5.7 [PROJ Type & Effect] . . . . . . . . . . . . . . . . . . . . . . . . . . 34

2.5.8 [Implicit Projection Type & Effect] . . . . . . . . . . . . . . . . . . . 34

2.6 Auxiliary Verification Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2.6.1 [Region Anti-Aliasing] . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2.6.2 [Effect Masking] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

2.7 Soundness of the Type and Effect Inference Rules . . . . . . . . . . . . . . . 35

3 FIX Equivalence/Inclusion Testing 37

3.1 Algorithmic Complexity Slicing in FIX . . . . . . . . . . . . . . . . . . . . 37 3.1.1 Gradual Reduction to Normal Form . . . . . . . . . . . . . . . . . . 37 3.1.2 Description Nodes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.1.3 Description Node Equivalence Testing . . . . . . . . . . . . . . . . . 44 3.1.4 Description Node Inclusion Testing . . . . . . . . . . . . . . . . . . . 45 3.1.5 Data Caching of Inclusion Results . . . . . . . . . . . . . . . . . . . 46

3.2 Re-evaluation of the FIX Equivalence/Inclusion Testing Strategy . . . . . . 47 3.2.1 Design Pressures Revisited . . . . . . . . . . . . . . . . . . . . . . . 47 3.2.2 Efficient Inclusion Testing . . . . . . . . . . . . . . . . . . . . . . . . 47 3.2.3 Efficient Equivalence Testing . . . . . . . . . . . . . . . . . . . . . . 47 3.2.4 Return to Efficient Inclusion Testing . . . . . . . . . . . . . . . . . . 50 3.2.5 Summary of Efficient Equivalence/Inclusion Testing . . . . . . . . . 51 3.2.6 Exploitation of Decorations . . . . . . . . . . . . . . . . . . . . . . . 51

4 Description Inclusion Algorithm 53 4.1 The Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 4.2 Inclusion on Recursive Types . . . . . . . . . . . . . . . . . . . . . . . . . . 54 4.3 Early Termination of Failing Inclusion Tests . . . . . . . . . . . . . . . . . . 57

4.3.1 Tolerable Dissimilarities . . . . . . . . . . . . . . . . . . . . . . . . . 57 4.3.2 Decorations for Early Failure Detection . . . . . . . . . . . . . . . . 57

4.4 Informal Total Correctness Argument . . . . . . . . . . . . . . . . . . . . . 59 4.4.1 Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 4.4.2 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59

5 Implicit Projection via Abductive Inference 61 5.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 5.2 Implicit Projection as Context Resolution . . . . . . . . . . . . . . . . . . . 61 5.3 Abductive Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 5.4 Abduction over Inclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 5.5 Context Resolution via Abduction over Inclusion . . . . . . . . . . . . . . . 69 5.6 Implementing Context Resolution . . . . . . . . . . . . . . . . . . . . . . . . 71 5.7 Abduction over Set Inclusion . . . . . . . . . . . . . . . . . . . . . . . . . . 76 5.8 Context Resolution via Abduction over Set Inclusion . . . . . . . . . . . . . 80 5.9 Implementing Abduction over Set Inclusion . . . . . . . . . . . . . . . . . . 83 5.10 Context Resolution Without Parameter Liberation . . . . . . . . . . . . . . 87 5.11 Summary of Implicit Projection . . . . . . . . . . . . . . . . . . . . . . . . . 89 5.12 Dynamically Bound Description Variables . . . . . . . . . . . . . . . . . . . 91

6 Effects in FX-87 95 6.1 Effects: What They Mean . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 6.2 Observability of READ and WRITE Effects . . . . . . . . . . . . . . . . . . . . 96 6.3 Classes of Region Occurrences . . . . . . . . . . . . . . . . . . . . . . . . . . 97 6.4 The READ and WRITE Effect Masking Rule . . . . . . . . . . . . . . . . . . . 101 6.5 Observability of ALLOC Effects . . . . . . . . . . . . . . . . . . . . . . . . . . 102 6.6 The ALLOC Effect Masking Rule . . . . . . . . . . . . . . . . . . . . . . . . . 107 6.7 The Process of Effect Masking . . . . . . . . . . . . . . . . . . . . . . . . . 108

6.7.1 Implementing ALLOC Effect Masking . . . . . . . . . . . . . . . . . . 108 6.7.2 Implementing READ and WRITE Effect Masking . . . . . . . . . . . . . 109 6.7.3 Consideration of Irreducible Description Applications . . . . . . . . 109

6.8 Summary of Effect Masking . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 6.9 Modulated Type Inclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112

6.9.1 The Problem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 6.9.2 The Solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 6.9.3 The Repercussions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 6.9.4 The Upshot . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 x CONTENTS

[This page intentionally left very nearly blank.]

List of Figures

0-1 A Simple Normalization Lattice . . . . . . . . . . . . . . . . . . . . . . . . . 4 0-2 A Simple Inclusion Lattice . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 0-3 Normalization/Inclusion Cubic Lattice . . . . . . . . . . . . . . . . . . . . . 7

1-1 Evolution of Related Languages . . . . . . . . . . . . . . . . . . . . . . . . . 16

3-1 The FIX Normalization Strategy . . . . . . . . . . . . . . . . . . . . . . . . 38 3-2 Description Node Equivalence Algorithm . . . . . . . . . . . . . . . . . . . . 44 3-3 Description Node Inclusion Algorithm . . . . . . . . . . . . . . . . . . . . . 45 3-4 An Idealized Fully-Connected Normalization Strategy . . . . . . . . . . . . 48

4-1 RECTYPE Inclusion Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . 55

5-1 Context Resolution Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . 71 5-2 Abduces Subroutine Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . 72 5-3 Resolve Subroutine Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . 73 5-4 Flexible Context Resolution Algorithm . . . . . . . . . . . . . . . . . . . . . 84 5-5 FlexUpdateL Subroutine Algorithm . . . . . . . . . . . . . . . . . . . . . . 85 5-6 Flexible Abduces Subroutine Algorithm . . . . . . . . . . . . . . . . . . . . 86 5-7 Equational Axioms Relevant to Set Descriptions . . . . . . . . . . . . . . . 89

6-1 Structured Data Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 6-2 Modulated Application Type and Effect Rule . . . . . . . . . . . . . . . . . 113 6-3 Modulated REF Inclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113

Chapter 0

Thesis Overview

0.1 My Thesis

Powerful static analysis systems can be incorporated into a compiler without adversely affecting its running time. This thesis is demonstrated by examining the algorithmic complexity of three aspects of a powerful compile-time analysis system.

First, a sophisticated system of type compatibility axioms is introduced. Using an implementation technique I call algorithmic complexity slicing, it is shown that the time needed to type check a value expression using these axioms can be made proportional to the inherent difficulty of type checking that particular expression, which is usually not equal to the worst-case computational complexity of the algebraic system of type compatibility axioms, where “type compatibility axioms” refers to axioms about the well-typedness of programs. This should at least partially lay to rest the long-standing “expensive structural compatibility” myth perpetuated by some texts on comparative language design [MacLennan 87] [Pratt 84].

Second, the problem of inferring implied projections in applications of polymorphic procedures is examined. The inference of first-order projections is shown to be efficiently decided by a soundness-preserving reverse inference over the type compatibility axioms. This technique I call an abductive inference. Higher-order inference is not attempted insofar as it is known to be undecidable [Goldfarb 81] [Pfenning 88]. All this is developed in the framework of the Type/Region/Effect/Kind system of the programming language FX-87 [Gifford et al. 87], a statically typed variant of the Scheme [Rees & Clinger 86] dialect of Lisp [Steele 85].

Finally, the problem of discarding declarations of externally non-observable effects is examined. A semantics of FX-87 effect declarations is developed from which a set of rules for disregarding non-observable effects is derived. The resulting Effect Masking Rules are more effective and efficient than those prescribed by the FX-87 language specification [Gifford et al. 87].

In sum, FX-87 can be implemented efficiently and effectively. Pertinent algorithms are presented to support this claim.

0.2 The Problem

Ten-thousand lemmings can’t all be wrong. — graffito

Modern type checking systems for programming languages are normally based on a nonstandard interpretation of the denotational description of the language’s value semantics [Nielson 86] [Nielson 87/88]. Such systems mimic the standard interpretation of value expressions but rather than reducing value expressions to canonicalized value expressions subject to the dynamic semantic constraints of the language, the value expressions are reduced instead to their corresponding types, subject to the static typing restrictions of the language. For example, given the combination (+ 3 4), a type checker would interpret this as the application of a primitive procedure with type INT × INT → INT to two literals of type INT. Given that the argument types are compatible with the parameter components of the operator type, the type of the resulting value of the combination is INT. Thus, a type checker would reduce this combination to the type expression INT. On the other hand, had the argument types not been compatible with the parameter types, the type restriction on applications would have been violated, and so the expression would be ill-typed. The critical point here is that at each intermediate step along a possibly nested interpretation, the typing restrictions of the language must be enforced. In the above example, this was tantamount to a mere textual identity check on component type expressions; however, in a language with a sophisticated algebraic system of type compatibility axioms, these restrictions could be considerably relaxed. Unfortunately, as a consequence the compatibility check could become expensive. In particular, compatibility via structural comparison has long been bemoaned in texts on comparative language design as being expensive, especially when recursive (cyclic) type expressions are permitted [MacLennan 87] [Pratt 84]. I argue that this long-standing “expensive structural compatibility” accusation is overstated.

The crucial observation here is that the expense in type checking comes from enforcing the compatibility restrictions over the compatibility axioms, or rather from verifying that the compatibility restrictions are not violated. In languages allow only name-equivalence, this task is simple: one need check only that the type expressions involved are the same “names”, that is, the same defined type. There are, in effect, no compatibility axioms in such a language, other than the trivial reflexivity axiom. Thus, if an expression type checks without resorting to any other compatibility axioms, we should expect the type checking process for that expression in a system with structural equivalence to be as fast as in a nameequivalence system, regardless of what other compatibility axioms are available and what their computational complexity may be. This is why the issue of verifying compatibility restrictions was emphasized above: the type checker should expend only as much effort as necessary to verify that the compatibility restrictions are satisfied; thus, the cleverness should go into the compatibility verifier and not into the axiom system. Specifically, the verifier should use the compatibility axioms only as needed rather than exploiting them en masse, say to grind a type expression into its normal form. To illustrate more clearly this distinction, consider how such compatibility axiom systems are normally used in the setting of non-standard interpretation.

0.2.1 The Standard “Non-Standard” Approach

The compatibility axioms on type expressions can themselves be viewed as constituting an interpretation for the denotational description of type expressions. To point, if type checking is to be decidable in our language,^{1} then at least those type compatibility axioms corresponding to type equivalence relations can be viewed as reduction rules over type expressions. These reduction rules collectively constitute a strategy for reducing type expressions to a normal form. As such, the type expressions generated through non-standard interpretation of the value expressions are themselves, in turn, subjected to “non-standard” interpretation in the sense that one does not normally view types as being expressions which are themselves interpreted with respect to the type equivalence axioms to yield normal forms that can serve as equivalence class representatives. The remaining axioms (such as structural subtyping axioms or renaming axioms) may be incorporated into the compatibility verifier, where they are applied on-the-fly . This, for instance, is the approach taken in [Jouvelot & Gifford 88]. The problem with such an approach, of course, is that all applicable axioms are actually applied in reducing a type to normal form rather than just that subset of the axioms which are necessary to the particular verification task at hand.

0.2.2 A Less Standard “Non-Standard” Approach

The Ideal

An alternative way to view this is as follows: Indeed, the equivalence axioms generate a normalization strategy, but there may be no need to do full normalization. To point, when two type expressions are being verified compatible, they need be only partially normalized to the extent that they become verifiably compatible.

Restricting the present discussion to type equivalence, we noted that the equivalence axioms generate a normalization strategy, and yet we were non-specific as to what that strategy should be. For instance, if several equivalence axioms apply to the same type expression simultaneously, which one should be applied first? Insofar as the reduction to a normal form is a confluent operation (it has the “diamond” property), it makes no difference. Thus, as exemplified by Figure 0-1, the reduction rules give rise to a normalization lattice, where the source type expression is the top, each branch corresponds to the application of one reduction rule, and the bottom is the normal form of the source type expression.

1Although there are compelling reasons why one might choose to relax this [Cardelli 86] [McAllester 89], I fortuitously assume decidability of the type checker to be a restriction on the class of languages under consideration.

                    ((INT × INT → ((INT → INT) INT)) INT INT)
                                 //   \\
                                //     \\
                ((INT → INT) INT)     ((INT × INT → INT) INT INT)
                                \\     //
                                 \\   //
                                   INT

Figure 0-1: A Simple Normalization Lattice

Now we can view the reduction to normal form as a downward traversal along a reduction lattice. When we compare two type expressions for equivalence, we then need only traverse their respective reduction lattices to their earliest point of intersection. For instance, in the example above if we were comparing the original source type expression with, say, the left type expression on the second reduction level, then we could avoid reducing them both to the bottom normal form. When two type expressions are in fact not equivalent, then that too will be discovered since their reduction lattices will not intersect.

Note that the above is not meant to suggest that the full normalization lattice actually ever be generated; rather, the comparison procedure need only simulate traversal over this lattice. That is, comparison can be viewed as a search problem over a pair of reduction lattices for the first point of intersection of these downward directed lattices, where the search lattices can in effect be generated on-the-fly.

This is an entirely natural way to verify equivalence. Algebraically, all that is necessary is that the two sides of an equation be made textually identical. So long as we are restricted to axioms which do not allow expressions to be transferred from one side of the equation to the other,^{2} then such an algebraic system really is just tantamount to locating the earliest intersection along the reduction lattice, or as lattice theorists call it, the greatest lower bound (glb).

2An example of an axiom which violates this restriction is the α-renaming rule, which states that two function types which differ only in their choice of parameter names can be made equivalent by renaming the parameters of the one type to match the corresponding names of the other’s.

Switching our attention now from equivalence to the more general inclusion, one could imagine a new lattice denoting the lattice of subtypes of a given type expression. For example, the inclusion (powertype) lattice of the type (ONEOF (A a) (B b) (C c)) is depicted in Figure 0-2. For most type expressions, this is just the powertype (powerset) lattice with the source type expression as the top. That is, if we consider types to denote sets of possible values, then subtypes denote subsets of these possible values; hence the set of all subtypes of a type expression denotes the powerset of possible values, assuming the type language to be rich enough to express all such subsets [Cardelli 87] [Cardelli 88].

                           (ONEOF (A a) (B b) (C c))
                                  /    |    \
                                /      |      \
                              /        |        \
                            /          |          \
                          /            |            \
       (ONEOF (A a) (B b))    (ONEOF (A a)(C c))     (ONEOF (B b) (C c))
                       |  \         /     \         /  |
                       |    \     /         \     /    |
                       |      \ /             \ /      |
                       |      / \             / \      |
                       |    /     \         /     \    |
                       |  /         \     /         \  |
             (ONEOF (A a))       (ONEOF (B b))       (ONEOF (C c))
                          \            |            /
                            \          |          /
                              \        |        /
                                \      |      /
                                  \    |    /
                                    (ONEOF)

Figure 0-2: A Simple Inclusion Lattice

For other type expressions (like function types) which do not have an obvious subset-like algebraic textual appearance, the visual analogy is less immediate for the type expressions themselves, yet they represent precisely this sort of powerset over possible values. Conceptually then, verifying inclusion is tantamount to traversing the powertype lattice of the presumed supertype, searching for a node equivalent to the presumed subtype.

Why It’s an Unattainable Ideal

Unfortunately, this ideal is not computationally practical for several reasons. Nevertheless, carefully considering how it fails will provide crucial insight and motivation for the overall control structure of the final design.

First, when checking equivalence, selecting the branch of the reduction lattice which is most efficient to pursue relies on having some reliable distance measure to the glb. This measure, in turn, depends upon the specific two type expressions being compared. Thus, an accurate measure would require at least partial comparison of the two expressions involved. For instance, one might perform a breadth-first search over the two type expressions for the first node where they appear structurally inequivalent. For these two nodes, we could poll the axiom system for those axioms which would reduce their distance, for instance by reducing one of them to a reduct more structurally similar to the other or, in lieu of that, by reducing both of them to more structurally similar type expressions. This would clearly require a great deal of specific knowledge about the axiom system and may indeed involve more computational overhead in computing distances than a straightforward reduction to normal form might take. Nonetheless, this notion of a heuristic distance to a glb will surface again later.

Second, it was not made clear above just how the equivalence lattice would interact with the inclusion lattice. Specifically, casual reference was made to traversing the inclusion lattice in search of a node equivalent to the presumed subtype. This suggests some intermingling of the equivalence and inclusion lattices. Specifically, each node of the equivalence lattice is associated with an entire inclusion lattice for that particular degree of normalization of the expression. For example, consider the oneof/sum type normalization lattice:

                (ONEOF (A ((a → a) a)) (B ((b → b) b)))
                               //       \\
                              //         \\
     (ONEOF (A a) (B ((b → b) b)))   (ONEOF (A ((a → a) a)) (B b))
                              \\         //
                               \\       //
                           (ONEOF (A a) (B b))

Each node of this normalization lattice actually denotes an inclusion lattice consisting of the ONEOF powerset over the fields A and B at that node, as shown in the Figure 0-3. Thus, the intermingling of normalization and inclusion lattices can be viewed, in general, as a three-dimensional lattice with equivalence and inclusion forming independent axes and choice of axiom^{3} forming the third.

3That’s choice of axiom, not Axiom of Choice.

Graphically, we could envision normalization lattices as positioned in the horizontal plane, oriented with their normal form being leftmost. Inclusion lattices would then be vertically positioned with the least element at the bottom. The sketch below is intended to be roughly suggestive of this arrangement, where ∪ is used to abbreviate ONEOF.

      ---------------------------------------------------------------------
     /                                                                    /
    / (∪ (A ((a → a) a)) (B b))⇐=(∪ (A ((a → a) a)) (B ((b → b) b)))/

/  ∥  ∧  ∥  ∧  /

  /  ⇓  / \  ⇓  / \              /
 /     (∪ (A a) (B b))⇐==(∪ (A a) (B ((b → b) b)))/   \            /
/  ∧ /     \   /                \   /     \          /
---------------------------------------------------------------------
     ----------/---/---------\--------------------\---------\------------
    /         /   / \      /  \                  / \         \          /
   /         /   / (∪ (A a))⇐(∪ (A ((a → a) a)))  \         \        /
  /         /   /       :             :              \         \      /

/ (∪ (B b))⇐=================(∪ (B ((b → b) b))) /

/             :          :          :            :                  /
--------------------------------------------------------------------
    --------------:-------:-------:---------:-------------------------
   /                 :     :     :      :                            /
  /                     :   :   :   :                               /
 /                           (∪)                                   /
/                                                                 /
------------------------------------------------------------------

Figure 0-3: Normalization/Inclusion Cubic Lattice

Now, were we to naïvely navigate this cubic lattice upon inclusion testing of two type expressions, inclusion could become quite expensive indeed. For example, were we to traverse the inclusion lattice of the unnormalized presumed supertype expression, at each step testing afresh the equivalence of this new unnormalized type with the unnormalized presumed subtype, then this could become exponentially expensive. Graphically, this corresponds to descending the inclusion lattice of the supertype expression, at each node exhausting the corresponding equivalence lattice at that level. Instead, we could first test the type expressions for mere equivalence. In the case where they cannot be shown equivalent, we can still proceed to reduce both of them to normal form (that is, traverse both reduction lattices to their leftmost extremities). We would then proceed with testing for inclusion by descending the inclusion lattice of the normalized presumed supertype, testing at each step for equivalence with the normalized presumed subtype. Graphically, this corresponds to lockstep traversal of the two source normalization lattices (the topmost faces of the two normalization/inclusion cubic lattices). Upon reaching the leftmost nodes of each normalization lattice without success, the traversal proceeds by descending the inclusion lattice of the now-normalized presumed supertype, “pointwise” testing equivalence by testing each node against its corresponding node in the now-normalized presumed subtype.

Thus, inclusion testing will in the worst case traverse only two faces of the supertype’s normalization/inclusion cubic lattice— namely, the topmost horizontal (equivalence) face and the leftmost vertical (inclusion) face— and one face of the subtype normalization/inclusion lattice— namely, the topmost horizontal (equivalence) face. Many alternative traversal strategies are possible, but this one seems particularly well motivated in view of memoization of normalization and considering that we expect mere equivalence to usually suffice. Moreover, such a strategy maintains the relative inexpense of equivalence with respect to the more general inclusion, as desired: we can test equivalence efficiently independent of the inclusion axioms since, by nature of the normalization/inclusion cubic lattice traversal, we in effect test equivalence first without regard for the inclusion axioms. Thus, the computational complexity of the inclusion axioms does not infiltrate the computational complexity of proving equivalence.

Third, even with the above pre-normalization of inclusion candidates, it is still unclear how to direct the inclusion lattice search when the easier equivalence test has failed. Here, however, a distance metric is more straightforward given that the two expressions will be in normal form. Specifically, the equivalence axioms need no longer be considered. Thus, inclusion testing can be implemented as a structural lockstep traversal of the presumed supertype and subtype, recursively checking for pointwise inclusion of the respective components according to the applicable inclusion axioms. With each subsequent pointwise inclusion test, invoking unnecessary inclusion axioms could be avoided by again testing for equivalence first. This is particularly advantageous in this case since, given that all subexpressions of a normal form will themselves be in normal form, no additional equivalence axioms need be invoked: a trivial reflexivity test suffices.

Fourth, some type expressions (notably record/product types) may have a countably infinite number of subtypes. For example, where a record with two fields is expected, a record with twenty could be passed so long as two of the twenty fields denote compatible components (relative ordering of fields is irrelevant). A record with two hundred fields could similarly be passed for the twenty-field record, and so on to arbitrary depth. Moreover, a record with only one additional field is also a subtype of the record without the extra field, where this extra field could be any of a countably infinite set of choices. Thus, the record inclusion lattice has infinite fan-out as well as infinite depth. Obliviously traversing such an inclusion lattice, exhaustively searching for the occurrence of some expression which may never appear (e.g., when the presumed subtype in fact is not a subtype of the presumed supertype) could result in a divergent type checker. Fortunately, the preceding concession to test inclusion axioms via structurally recursive pointwise testing can accommodate such situations since the inclusion axioms can be implemented as Boolean predicates (inclusion testers) rather than as type rewrite rules. That is, rather than use type rewrite rules which blithely wander the inclusion lattice testing equivalence, we could implement the record inclusion axioms by procedures which direct the search based on the two records being compared, essentially iterating over the fields of the presumed supertype testing for compatible fields in the presumed subtype.

Finally, the strategy as presented so far reeks of redundant computations. Some memoization or hashing techniques would certainly be justified. For instance, computing the normal form of a specific occurrence of some type expression should be done at most once. Similarly, memoization of equivalence/inclusion findings should be done.

0.2.3 A Non-“Non-Standard” Approach

Given that this idea was an unattainable ideal, how can we nonetheless approximate such an ideal with a practical system? Most of the problem discussed above included some concessions for a practical implementation, but the pivotal difficulty remains how to supply a distance measure to guide the equivalence search through the normalization lattice when seeking the glb of two type expressions. Above, I argued that using the two expressions themselves to direct the search is unsavory. Instead, however, we could still use the axiom system itself to direct the normalization. Specifically, we can associate with each equivalence axiom the computational complexity of applying that axiom. This can serve to direct our normalization efforts, as described below.

If we now concentrate on incrementally reducing a type expression to its normal form by making several passes over the expression, each pass more computationally complex than the last, then after each complete pass we will have a type expression closer to normalization and within a given complexity bound. For instance, we could endeavor to exhaust all the linear-time axioms on the first pass, the O(n lg n) axioms on the second, and the O(n^{2}) on the third. Of course, some axioms may be reapplied in subsequent phases if some more expensive axiom gives rise to new redexes of a less expensive axiom, but this will be absorbed into the cost of the more expensive axioms.

Given such an incrementally more expensive normalization strategy, two type expressions could be compared for equivalence by first testing if they already satisfy the trivial reflexivity axiom. If they do not, we could apply the first pass to each one, subsequently checking for convergence to their glb (by again testing reflexivity). So long as the subsequent tests fail, we could continue with the next phase. Note that since each subsequent phase will potentially dominate in running time over the previous phases, any unnecessary application of less expensive axioms in the earlier phases can be absorbed into the expense of the subsequently more expensive axioms. Further, note that the most expensive situation is when type expressions involving the most expensive axioms are found to be, in fact, inequivalent; yet then they will have been fully reduced to normal form, the cost of which can be amortized over subsequent comparisons.

This technique of gradual normalization via increasingly complex partial normalization phases separated by early termination tests I call algorithmic complexity slicing. Of course, this technique should be reminiscent of gradual deepening techniques common in game tree searches.

Naturally, a variety of acceleration techniques can also be applied. For instance, type expressions could be represented via data structures containing the memoized results of successive slice boundaries. Additionally, these memoized intermediates could be hashed/interned to accelerate subsequent reflexivity tests. Moreover, the intermediates could themselves benefit from data structuring and annotation/decoration to facilitate subsequent inclusion axioms and inclusion tests. Finally, the degree to which a type expression has been partially normalized could be annotated along with the intermediates so that whenever two types are proved equivalent, the less normalized type can adopt the intermediates of the more normalized type. This normalization inheritance is a variation on Tarjan’s familiar Union/Find algorithm [Tarjan 83]. An analogous adaptation applies to gradually generating the inclusion lattice relating all top-level defined types.

0.3 Additional Contributions

In addition to the above, the following techniques are developed and employed to admit efficient structural comparison over a sophisticated algebraic axiom system.

• “Inverse” DeBruijn numbers [de Bruijn 72] for βη-stable α-renaming

• Recursive type normalization via DFA minimization and μ-calculus [Park 76] canonicalization

• Generalized and improved ALGOL 68 algorithm for the comparison of recursive type expressions [van Wijngaarden et al. 76]

• Efficient one-way inclusion unification over a set without backtracking via flexibility indexing to find the most general conservative unifier (mgcu)

• Refined effect masking rules based on distinguishing various syntactic classes of REGION occurrences.

Of course, the last one is specific to the axioms of so-called region-based effect systems.

0.4 Concretization: Introduction to FIX

0.4.1 Focus and Scope

To be concrete about the techniques described above, the body of the thesis is an extended case study in how they would be incorporated into an efficient implementation of the verification system for the programming language FX-87. As will be shown [Chapter 2], FX-87 has a sophisticated comparison axiom system, one which in fact subsumes that of practically all other contemporary programming languages with decidable verification. Henceforth, therefore, the presentation will be structured as a case study in implementing the verification phase of an FX-87 interpreter/compiler. This design of an efficient implementation of FX-87 verification I have dubbed FIX. Unfortunately, due to time constraints, generalization of this case study and potential automation of these techniques are left for future research, as are empirical evaluation of its overall effectiveness. My apologies for these shortcomings.

0.4.2 Goal

The immediate goal of this thesis, therefore, is to present a design for an efficient implementation of a verification system for FX-87, a programming language with a rich declaration language. I do this by developing a style of system design that I call algorithmic complexity slicing that allows the running time of verification to depend on the complexity of the specific verification task at hand rather then on the worst-case complexity of the verification axioms. This implementation design I call FIX to suggest that it fixes the problem of implementing efficient verification systems for languages with complex type comparison axiom systems.^{4}

4And to suggest that implementations which do not are BROKEN. Or, to be less inflammatory, note that the three letters in “FIX ” are also a permutation of the first three letters of “FX Implementation”.

0.4. CONCRETIZATION: INTRODUCTION TO FIX 11

Specifically, FIX is an implementation design of the verification phases of an FX-87 interpreter or compiler. Insofar as FX-87 programs can be translated into equivalent Scheme programs, the issue of interpretation and compilation of the verified program is not addressed by this thesis except to motivate why effective effect masking is desirable in Chapter 6. Therefore, the verification phase checks the static correctness of the FX-87 program from which an equivalent Scheme program suitable for Scheme interpretation and compilation could be easily produced. The design of subsequent phases of the FX-87 interpretation and compilation process is therefore not addressed. At the very least, it would be comprised mostly of defining an interface between the FX-87 programmer and the top-level of some underlying native Scheme interpreter upon which FIX could be implemented. This is the same approach as that taken by [Jouvelot & Gifford 88].

0.4.3 Perspective

This thesis is primarily an engineering thesis: it attacks the problem of engineering an efficient implementation of FX-87, a programming which presents several interesting and challenging problems. Often this entails exploring the theoretic foundations of FX-87, either to investigate the interaction between features of the language and their ramifications, or to explain the rationale behind those constraints specified in the language reference manual [Gifford et al. 87]. Along the way, I hope also to bring to light some of the trade-offs made in the design of FX-87 that were left implicit in its specification but which should interest language designers. On occasion, I resort to formalism to justify an algorithm or a design strategy, but I have endeavored to keep this to a minimum. When I present a novel algorithm or an improvement or extension to a well-understood algorithm, it is always accompanied by an informal explanation and design justification. To this extent, the thesis does not offer so much a single salient result as an exploration of a problem space. The result is that FX-87 can be implemented efficiently, but the point of interest is how: FIX offers one possible answer.

0.4.4 The Plot

A program without a loop and a structured variable isn’t worth writing. — ALAN J. PERLIS, Perlis’ Programming Epigrams (1980)

For an efficient implementation of FX-87, the challenge is posed primarily by those programs that create and manipulate aggregate data structures and that frequently conditionalize on the contents of this data. User-defined polymorphic procedures are also important since by polymorphizing a procedure the programmer has suggested that it is of general utility and will therefore be used in many semantically distinct contexts. I dub such programs “interesting” to suggest that those remaining programs, which do straightforward computation, present no pressures on an efficient verification system. They also do not appear to model the behavior of a system which is not inherently modeled already by the primitives of the language [Abelson, Halfant, Katzenelson & Sussman 88] [Halfant & Sussman 87/88] [Roylance 87/88]— which is to say that mere number crunching is not “interesting” in the context of verifying FX-87 programs.

That given, FIX addresses those features of “interesting” FX-87 programs that pose a challenge to efficient verification. Namely:

1. Application of procedures permits actual arguments to have types which are subtypes of the expected types (the declared formal parameter types). Inclusion testing must be efficient.

2. Conditionalization (e.g., via COND, IF, and TAGCASE) requires that all branches of a conditional expression produce a result whose type is comparable to that of every other branch. The largest (with respect to the inclusion axioms) of these branch types is called the maxtype^{5} of the branches’ types. It is not known a priori which branch(es) have this maxtype, but it too must be computed efficiently.

3. Language primitives which create and manipulate aggregate data structures are invariably polymorphic, therefore their use will nearly always employ Implicit Projection. Likewise, user-defined polymorphic procedures will normally be used in conjunction with Implicit Projection. Implicit Projection must be done efficiently.

4. Implicit Projection is specified to be one-way unification by inclusion [Gifford et al. 87, p.41]. Whenever some unification variable (an implicitly projected POLY formal) is matched against several possibly unrelated descriptions, one of them must denote the MAX of the others. Again, it is not known a priori which will be this MAX.

5. Inductively and cyclicly defined data have recursive types. Testing inclusion of such types can be quite expensive. This expense must be avoided when possible.

6. The latent effect declaration inside a SUBR type limits the places the SUBR can be passed; however, discarding annotations of unobservable effects minimizes these latent effects. Doing this well requires Effect Masking Rules which are both powerful and efficient.

In short, the efficient verification of interesting FX-87 programs depends heavily on the ability to efficiently compute the MAX of an unordered collection of descriptions. This is the most expensive aspect of verifying interesting programs. To that end, this thesis presents a design for a verification system that can efficiently compute the MAX of an unordered collection of descriptions given the rich inclusion system of the language FX-87. In addition, it is shown how Implicit Projection can be formalized and, from this, how it can be computed efficiently. Finally, a formal development of the semantics of effect annotations is presented, and from that are derived powerful and efficient new Effect Masking Rules.

0.4.5 Summary

Again, FIX is an exercise in a style of system implementation that I call algorithmic complexity slicing. By that term, I mean to suggest that the strategy is to identify those language features that challenge efficient verification, either in vacuo or in conjunction with other features, then use this knowledge of the intricacies and idiosyncrasies of the language to design a well-informed verification system that performs with an efficiency contingent upon the inherent difficulty of each verification task presented it. Specifically, inexpensive verification is always attempted first; only upon its failure are more expensive attempts at verification performed. This avoids the cost of expensive verification by charging the expense only to those expressions that require it.

5Caveat: this is not the least upper bound (lub) familiar to lattice theorists because the lub does not in general exist for two types in FX-87; for example, INT and BOOLE are incomparable.

0.4.6 Limitations

The result is a system very tightly coupled to the language, where the complexity of the FIX design closely reflects complexities inherent in the language. Although this implies that modest perturbations in the language design could have significant impact on the strong assumptions made throughout the design— strong assumptions which often cascade to have pervasive impact on the design— I consider this fragility acceptable since FX-87 is an experimental language, and as such, it is well worth pursuing a tight design to expose and occasionally exorcise those aspects of the language that thwart efficient verification. Further, it is my hope that much of this design approach could be at least partially automated given the verification rules of the target language definition.

14 CHAPTER 0. THESIS OVERVIEW [This page intentionally left very nearly blank.]

The Evolution and Essence of FX-87

Ontogeny recapitulates phylogeny. — ERNST HEINRICH HÆCKEL, History of Creation (1868)

The primary thrust of FX-87 as an advance in language design lies in its static typing system. Specifically, FX-87 embodies two advances in static typing technology: a stratified (kinded) type system [McCracken 79], and an effect system [Gifford & Lucassen 86] [Lucassen & Gifford 88]. In this chapter, the evolution of these ideas is traced by briefly considering those languages from which FX-87 borrows much of its design. Since detailed descriptions of these languages would be beyond the scope of this thesis, only those features which have influenced the design of FX-87 are mentioned. This approach will hopefully serve two purposes: 1) to reduce the intellectual overhead of becoming fluent in FX-87 by providing a brief evolution of the fundamental ideas on which its design was based, and 2) to alleviate the language designer’s mission of internalizing the salient features of FX-87 by accurately pinpointing it within the ever-increasing spectrum of programming languages. Having established this context, the particulars of FX-87’s distinctive stratification and effect system are discussed.

1.1 Historical Overview of FX-87

(FORTRAN)                   LISP        .---------------------------------.
    :...... ALGOL 60         |          | |   means    direct predecessor |
             /     \          \         | :   means  indirect influence   |
        PASCAL   ALGOL 68      \        | ||  means    theory influence   |
          |         :           \       `---------------------------------'
        EUCLID      :          SCHEME
          :    .    :              \       Reynolds74
       ADA/CLU  .   : SMALLTALK-80  \        //
          :   .  .  :      :         \     LS1
          ML    . ..:    AMBER        \   //
          : `.......:......:...........MFX (Lucassen)
      PEBBLE                            |
                                      FX-87

Figure 1-1: Evolution of Related Languages

1.1.1 ALGOL 60

ALGOL 60 [Naur 63] may be considered a root of FX-87’s ancestral tree. It introduced static typing^{1} and block structure as well coining the now standard Backus Normal Form (BNF) grammar for syntactic specification of programming languages, which is used in the FX-87 Reference Manual [Gifford et al. 87].^{2} I mention ALGOL 60 not because any particular feature of it arises in FX-87 but because it should be contrasted with the Lisp family of languages, which one might naturally infer to be FX-87’s primary ancestry. In fact, FX-87 represents a coupling of the expression domain of the Lisp tradition (spec., Scheme) with the static typing of the ALGOL tradition.

1.1.2 ALGOL 68

ALGOL 68 [van Wijngaarden et al. 76] expanded the typing system of its namesake, adding to it the notion of recursive types and type equivalence via structural equivalence. FX-87 borrows both these features; however, it does not borrow its proliferation of implicit type coercions, its inscrutable terminology, nor its impenetrable context-sensitive grammar specification (using the so-called “W-Grammars” of [Cleaveland & Uzgalis 77]).

1Granted, FORTRAN had already distinguished integers from reals but these distinctions were not enforced by the compiler. For instance, an integer could be passed to a procedure where a real was expected.

2ALGOL 60 also lacked an effective I/O facility, which FX-87 inadvertently shares. This shortcoming in FX-87 is presently being addressed by its designers.

1.1.3 Pascal

Also a successor to ALGOL 60, Pascal [Wirth 71] was the rival sibling of ALGOL 68.^{3} Pascal returned to the simplicity and elegance of ALGOL 60, enriching it with more powerful data structures for enhanced expressibility while restricting other features in order to retrieve efficiency (e.g., Pascal is a fully stack-allocated language). FX-87 does much the same with respect to Scheme.

1.1.4 Euclid

A successor to Pascal, Euclid [Popek, Horning & London 77] offered a few extensions to and restrictions on its forebear. The primary alteration relevant to FX-87 is the restriction on the “aliasing” of formals. Specifically, Euclid forbade two distinct variable instances within the same lexical scope to refer to the same (or overlapping) datum in the store. This not only enhances verifiability of programs but, in conjunction with other restrictions (also present in FX-87), it allows type checking of Euclid programs to be entirely static.^{4} In FX-87 the Region Anti-Aliasing Rule [Gifford et al. 87, p.40] accomplishes the same goal. Euclid also provides a coarse distinction between those subroutines which have side-effects (procedures) and those which do not (functions).^{5} FX-87 uses regions to be more fine-grained (discussed in Section 1.3).

1.1.5 Ada/CLU

Despite their divergent stances on exception handling and the avalanche of features in Ada, Ada [Barnes 80] and CLU [Liskov et al. 79] are very similar languages. Both emphasize abstract data types (ADTs), or modules, for namespace control and information hiding. Although not present in FX-87, this is a primary design objective for its successor language.^{6} This also provides a mechanism for defining a restricted class of polymorphic procedures. In CLU these are called parameterized procedures; in Ada, generic procedures. These forms cannot be locally defined (a syntactic constraint) and cannot be used until instantiated (since they are not considered well typed until instantiated). Of more interest to us, CLUoffers first-class monomorphic procedures; although, these cannot be locally defined. Further, CLU is the first language mentioned that provides user-defined type generators (parameterized clusters) and possibly locally defined user-defined type abbreviations (equates). Alas, neither user-defined type generators nor abbreviations may be of higher order in CLU, nor are the generators first-class within the type language: as with parameterized clusters, only upon instantiation may type generators be used. This persistent restriction to lower-order, instantiated instances effectively requires that polymorphic forms be explicitly coerced into monomorphic forms before being used. FX-87 does not share these restrictions. Finally, CLU makes a coarse distinction between mutable and immutable instances of aggregate data structures, as does FX-87 but CLU considers the two classes to be incomparable. FX-87 is more tolerant: one can often pass a mutable aggregate datum where an immutable one is expected.

3I use the past tense here because ALGOL 68 is generally considered to be obsolete while Pascal still enjoys wide-spread use today. No judgment on the virtue of this situation is intended.

4But Euclid also allows machine-dependent type loopholes, thus it cannot be said that Euclid is strongly typed. FX-87 is.

5Of course, the original Pascal definition attempted to make a similar distinction [Wirth 71] but there it was unenforceable [Habermann 73, §6].

6For details, see [Sheldon 89].

1.1.6 Standard ML

Perhaps the closest approximation to FX-87 of all the languages implemented and in widespread use today is Standard ML [Milner 84] [Harper & Mitchell 87]. Standard ML is the first language considered that offers possibly locally defined polymorphic and monomorphic procedures.^{7} Standard ML also uses a type reconstruction algorithm [Milner 78] to infer the types of formal parameters of procedures, a facility which FX-87 does not provide.^{8} On the other hand, polymorphic procedures in Standard ML are not first-class since they must be fully instantiated before being passed as arguments or returned as values, this precisely by fault of the reconstruction algorithm [Milner 78, pp.353–355] (although monomorphic procedures are first class). FX-87 does not share this limitation. Finally, Standard ML offers a curiosity: destructuring of compound values via pattern matching, a feature more characteristic of the “call by unification” feature of logic programming languages [Hewitt 69] [Kowalski 79]. A future iteration of FX may provide a similar feature.

1.1.7 LS1

Almost a precise match with the stratified type language of FX-87 is Nancy McCracken’s illustrative language LS1 [McCracken 79], an extension of Reynold’s second-order polymorphic λ-calculus [Reynolds 74]. Though not intended for implementation, LS1 (for Language System 1) provided first-class polymorphic procedures, user-defined type abbreviations, first-class user-defined type generators and recursive types, all possibly locally defined and couched in a framework of type equivalence via structural equivalence. To describe the meta-language of types within the stratified typing system of LS1, McCracken coined the term Kind, which FX-87 has adopted. Here also was introduced what McCracken called the “safe” condition on polymorphic types [McCracken 79, p.20f], which I shall call the McCracken Criterion. In a subsequent work of McCracken [McCracken 84] is found the source for our notion of implicit projection, which McCracken calls “implicit type application,” whereby explicit projections of polymorphic procedures in operator position can be omitted when the projection arguments can be inferred from the types of the application arguments. This is discussed in detail in Chapter 5. FX-87 extends this type system into a region-based effect system (discussed in Section 1.3).

1.1.8 Amber

From the Object-Oriented Programming Systems (OOPS) school, FX-87 adopts the notion of type inclusion, or implicit subtyping; however, unlike the class notion used to explicitly control the type inclusion hierarchy in traditional OOPS languages like Smalltalk-80 [XLRG 81], FX-87 follows Amber [Cardelli 84/85/86] in defining inclusion implicitly via structural induction on type expressions.^{9} By making the inclusion implicit and structural, FX-87 provides multiple inheritance without the difficulties currently encountered in the class-based inheritance paradigm.^{10} Of course, it has been noted that inheritance is not just subtyping [Cook, Hill & Canning 90]. This issue will not be addressed in this thesis, although it is a compelling direction for future work. Its impact on the design strategy developed here should not prove problematic.

7Note that I do not consider private procedures of Ada to constitute local definition since this mechanism does not facilitate nesting below one level.

8Although this too is a primary design goal for its successor. For details, see [O’Toole & Gifford 89].

1.1.9 Pebble

Finally in the progression of static typing technology, Pebble [Burstall & Lampson 84/88] [Lampson & Burstall 88] embodies an extreme. It offers dependent types and types as values (i.e., Type:Type), as well as a plethora of other exotic state-of-the-art typing features;^{11} however, this additional expressive power may be overkill since, for example, providing types as values comes at the expense of decidability of the type checker [Cardelli 86] and can give rise to logical paradox within the type domain [Meyer & Reinhold 86] [Reinhold 88], although this situation may not be problematic in practice. Nonetheless, Pebble is still largely an experiment in pushing the frontiers of language design: no full implementation of Pebble is known to me at the time of publication. Thus within the spectrum of statically typed programming languages, the FX-87 type system lies somewhere beyond that of Amber but shy of Pebble’s.^{12} I mention Pebble to more clearly delineate the present limitations on the power of typing systems in programming languages.

9[Lucassen 87, §3.4] The formal details of this method may be found in [Cardelli 84/88].

10For discussion of these difficulties and some attempted resolutions, see [Snyder 86].

11Like first-class bindings and control over “exposing the rep” in Abstract Data Types via implementation passwords.

12Although I am told by Mark Sheldon that the successor to FX-87 will provide static dependent types.

Pebble’s dependent types may not be static.

1.1.10 Scheme

Having located FX-87’s type language within the spectrum of languages that support static analysis, we note in passing that the value domain of FX-87 hails from a different parentage: the Lisp family of languages. The designers of FX-87 consciously endeavored to remain as fully compatible with the Scheme dialect of Lisp as possible, cleaning up what little type incoherence remains in that language.^{13} In fact, the only significant aspect in which FX-87 falls short of being a full-fledged extension of Scheme is in its failure to provide access to continuations; however, recent work toward this extension looks promising [Jouvelot & Gifford 89a].^{14}

1.2 Why Static Analysis?

At this point one might well ask why static analysis is desirable in a programming language. The standard sermon on the virtues of static type checking follows.

Of foremost concern is the run-time efficiency of the object code of our language, both in space and time. With static analysis of side-effects and of the extent of variables, one can implement various compiler optimizations [Lucassen 87] such as automatic storage reclamation, memoization, common subexpression elimination, dead code elimination, code motion, and parallel evaluation [Aho & Ullman 86] [Fischer & LeBlanc 88].

Second, strong type verification ensures code safety by excluding various classes of runtime errors. Moreover, the verification rules provide the framework for an axiomatic inference system by which one can 1) demonstrate the soundness of compiler optimizations (such as the ones cited above) as well as 2) prove the correctness of simple programs [Hoare 69].

Third, static analysis enhances the maintainability and reusability of code by enforcing constraints that may escape the notice of the programmer, such as the interdependencies of procedures. Consequently, this improves the program debugging cycle. In the case where these constraints take the form of explicit declarations within the source code, valuable documentation is provided as well.

Finally, some degree of type reconstruction/completion is desirable to alleviate the burden of the more obvious declarations; however, before an effective inference algorithm can be designed for a language it is vital to first provide a sound and complete static type checking system for that language. Thus, designing FX-87 to support static checking presumably eases the difficulty of extending its successor (ostensibly, FX-90) to provide type reconstruction/completion.

13For example, the disjointness of types is enforced. This eliminates the disconcerting notion, traditional among Lisp dialects, that #f denotes Boolean false while all other values are treated as Boolean true.

14Unfortunately, Gifford has been hesitant to incorporate these results into a successor language of FX-87, perhaps because providing first-class continuations would take FX-87 out of the stratum of Common Lisp [Steele 85], the standardized language atop which the FX-87 run-time environment has to date been implemented but which alas suffers a deficient continuation facility. Consequently, deviating from the Common Lisp standard in the FX-87 value domain could either reduce the portability of FX-87 implementations by requiring Scheme-based implementations or reduce the efficiency of Common Lisp-based FX-87 implementations by requiring a full continuation implementation between the levels of FX-87 and the underlying run-time language. Current efforts toward Scheme standardization [IEEE 90] could alleviate these concerns.

In sum, static analysis serves primarily as a mechanism for improved quality of object code, verifiability of both compiler optimizations and code correctness, maintainability and reusability of code, and realizability of a type reconstruction/completion algorithm.

This is not to suggest that strong typing is always desirable. Indeed, there do exist compelling reasons why one might wish to side-step strong typing. For instance, violation of the typing system is often necessary in systems programming.^{15} Also one may, on rare occasion, choose to defeat the typing system in favor of more efficient aggregate data structure storage and component access. For details, consult [Geschke, Morris & Satterwaite 77],^{16} from which the above points were taken.^{17}

1.3 Stratified Typing, and Effect Systems

In FX-87, we are interested in statically analyzing more than just the types of expressions: we are interested as well in their run-time side effects. It is through this static side-effect analysis that the soundness of compiler optimizations such as those mentioned in the preceding section can be proven. Effect systems extend existing type declarations and inference rules so as to document the side-effects of expressions as well as their types. This is done by extending the type system into a more general kind system, requiring declarations of kind EFFECT as well as those of kind TYPE. Effects, in turn, document the sets of locations in the store that they affect. In FX-87 this is achieved by conceptually coloring the store into distinctly colored REGIONs, thus further extending the kind system to include declarations of kind REGION. Thus, it is said that FX-87 employs a region-based effect system.

That done, those expressions with latent side-effects (e.g., procedures, whose effects are not realized until application) will have, embedded within their types, the declaration of their latent effects.^{18} When these latent effects are realized (e.g., by applying a procedure), the type checker will charge them against the total effect of the realizing expression. Thus, types are used as carriers for latent effects. In this way, Descriptions (generalized declarations) are used as a means of checking the types and effects of value domain expressions while using the meta-language of kinds to check the well-formedness of these descriptions. Similarly, those data structures for which it is desirable to distinguish mutable instances from immutable instances will contain, embedded within their types, the regions in which they are allocated.^{19}

Finally, FX-87 generalizes McCracken’s “type generators” into Dλs, which map among descriptions (including other Dλs). These Description Functions are themselves kinded, thus further extending the kind system with an infinite class of higher order DFUNCs.

15E.g., implementing a space efficient garbage-collected heap in FX-87 requires dropping type tags from the data stored in locations, relying on the meta-level compiler to enforce meta-level strong typing, despite the type loophole: once a datum is garbage collected fresh data of incompatible type can be stored in the freed locations.

16I am indebted to Mark S. Day for calling this paper to my attention.

17They also make a third point about temporary aliasing of user-defined types but this problem does not arise in FX-87 since it does not support Abstract Data Types.

18Which may be the effect PURE, which states that there effectively is no effect.

19There exists a distinguished Immutable Region as well as an axiom which states that any region containing the Immutable Region is itself immutable.

The result: the FX-87 kind system has been extended to include TYPEs, EFFECTs, and REGIONs as well as an infinite class of DFUNCs which map among descriptions. In short:

   <KIND> ::= TYPE | EFFECT | REGION | (DFUNC (<KIND>*) <KIND>)

This last extension may seem excessive since allowing DFUNCs as arguments to DFUNCs provides the description language with the full power of the first-order typed λ-calculus. As shall be seen later, this complicates various aspects of the language implementation. For that reason, perhaps the following restricted KIND grammar would be more desirable:

                   <KIND> ::= <Base KIND> | <Higher KIND>
              <Base KIND> ::= TYPE | EFFECT | REGION
            <Higher KIND> ::= (DFUNC (<Base KIND>*) <KIND>)

Furthermore, insofar as region descriptions never have type or effect descriptions embedded within them, we could further forbid DFUNCs that map types or effects to regions, since such a DFUNC would necessarily ignore the type and effect arguments. Similarly for DFUNCs that map effects to regions. Pictorially, these embedding relations can be represented as a Directed Acyclic Graph (DAG) where a downward directed arrow indicates that the target kind can be embedded within the source kind.

                                  TYPE
                                  /  \
                              EFFECT  |
                                  \  /
                                 REGION

Our restriction on well-formed DFUNCs would then be tantamount to the restriction that DFUNCs be of the form:

   (DFUNC (<K>*) (DFUNC (<K>*) . . . (DFUNC (<K>*) <K_rtn>)))

… where all <K>s must appear below <K rtn> in the Base KIND hierarchy. Note that when the <K>s are not restricted to be base kinds, this characterization is inadequate.

FX-87 Overview

2.1 ^{⟨⟨}Ce que c’est et ce que ce n’est pas^{⟩⟩}^{†}

As in LS1 [McCracken 84], we view FX-87 as a coupling of three distinct languages: the Value Language (which I call FX-87 proper), the Type Language (the meta-language of values), and the Kind Language (the meta-language of types). To be more precise, however, I should substitute the more general term Description for the word “type” in the preceding statement (following [Lucassen 87]) since FX-87 contains declarations of effects and regions as well as types. Thus, FX-87 is stratified into three expression domains: Values, Descriptions, and Kinds.

In short, the FX-87 Value Language is a polymorphic typed programming language with side-effects, implicit structural subtyping, and static control of aliasing.^{1} The FX-87 Description Language is a simply typed (“kinded”) λ-calculus with data recursion (recursive types).^{2} The FX-87 Kind Language is a free algebra.

There are a few features which are not present in FX-87 that have become popular among some of the more recent programming languages. Specifically, FX-87 does not have modules or abstract data types (ADTs), it does not supply an exception handling mechanism (other than the underlying Scheme debugger), it does not provide type re-construction or completion, it has no means for explicitly controlling concurrency, and it does not provide access to continuations. Most of these have been considered, at least intermittently, for incorporation into an FX-87 successor language [Sheldon 89] [O’Toole & Gifford 89] [Lucassen 87, Chapt.6] [Jouvelot & Gifford 89b] [Jouvelot & Gifford 89a]. It is expected that the techniques and algorithms developed here will carry through to such successors with minimal effort.

In the following sections, the description equivalence and inclusion rules are presented as well as the type and effect inference axioms and the auxiliary verification rules. For a detailed enumeration and explanation of the type inference rules and axioms for equivalence and inclusion in FX see [Lucassen 87]. For an encapsulated version of the same work, refer to [Gifford et al. 87, Appendix B]. Following are the grammar, axioms and rules of FX-87.

†“FX-87: What it is and what it isn’t”

1In the notation of [Barendregt 84], it is an extended λ^{π}β-calculus interpreter with side effects.

2I.e., it is a λ_{μ}^{τ}αβη-calculus. Note that I adopt the unconventional notation of specifying the α-conversion here to emphasize that the equivalence relation on Descriptions employs α-conversion, which complicates the implementation.

2.2 The FX-87 Language Grammar (Extended BNF)

2.2.1 [Kinds]

κ ::=  REGION | EFFECT | TYPE | (DFUNC (κ . . .) κ)

2.2.2 [Descriptions]

δ ::= ρ | ϵ | τ | δ_{ψ} | δ _{?}

δ_{ψ} ::= (Dλ (( identifier κ) …) δ) | δ _{?}

δ _{?} ::= (DLETREC (( identifier δ) …) δ) | (δ_{ψ} δ …) | identifier

  ρ ::= @= | @ identifier | (RUNION ρ ρ . . .) | δ _{?}
  ϵ ::= PURE | (READ ρ) | (WRITE ρ) | (ALLOC ρ) | (MAXEFF ϵ . . .) | δ _{?}

τ ::= τ _{base} | τ _{aggr} | τ _{poly} | δ _{?}

    τ _{base} ::= BOOLE | INT | NULL | SYMBOL | UNIT | VOID
    τ _{aggr} ::= (SUBR ϵ ( τ . . .) τ) | (REF τ ρ) | (PAIROF τ τ′ ρ)
           | (RECORDOF (( identifier τ) . . . ) ρ)

| ( ONEOF (( identifier τ) …) ρ) τ _{poly} ::= (POLY (( identifier κ) …) τ)

Note that I do not include the description sugar forms:

(DLET* (( identifier δ′) …) δ) ≡ (DLET (( identifier δ′))

                                       (DLET* (. . . ) δ))
     (DLET* ()  δ) ≡ δ

(DLET (( identifier δ′) …) δ) ≡ δ [δ′/ identifier][…]

… where δ [δ′/i][…] denotes δ with the simultaneous substitution of the δ′… for the free occurrences of the i… within δ, α-renaming as appropriate to avoid capture, with “free occurrences” defined in the obvious way [Lucassen 87, §3.3.5, p.31f].

2.2.3 [Values]

Note that in some of the productions below, I have included type annotations as superscripts for clarity.

υ ::= υ _{base} | υ _{aggr} | υ _{abst} | υ _{ctrl} | υ _{decl}

  υ _{base} ::= #U | #T | #F | '() |  ZZ

υ _{aggr} ::= υ _{sym} | υ _{param} | υ _{ref} | υ _{pair} | υ _{recrd} | υ _{oneof}

υ _{sym} ::= (QUOTE identifier)

υ _{param} ::=  identifier  | (SET! identifier υ)

       υ _{ref} ::= (NEW υ) | (GET υ ^{ref}) | (SET υ ^{ref} υ)
       υ _{pair} ::= (CONS υ υ) | (    CAR υ ^{pair})   | (    CDR υ ^{pair})
                            | (SET-CAR! υ ^{pair} υ) | (SET-CDR! υ ^{pair} υ)
       υ _{recrd} ::= (RECORD (( tag υ) . . . ) ρ) | (SELECT tag υ ^{recrd})
               | (RECORD-SET! υ ^{recrd} tag υ)

υ _{oneof} ::= (ONE τ ^{oneof} tag υ)

               | (ONE-SET! υ ^{oneof} tag υ)

| (TAGCASE identifier ^{oneof} ( tag υ … υ)… (ELSE υ … υ))

tag ::= identifier

υ _{abst} ::= υ_{λ abst} | υ_{π abst}

υ_{λ abst} ::= ( λ (( identifier τ) …) υ) | (υ^{λ abst} υ…) | (υ^{π abst} υ…)

| ( LETREC (( identifier υ) …) υ)

υ_{π abst} ::= (Pλ (( identifier κ) …) υ) | (PROJ υ^{π abst} δ…)

               | (PLETREC (( identifier δ) . . . ) υ)

υ _{ctrl} ::= υ _{brnch} | υ _{sequ}

υ _{brnch} ::= (IF υ ^{Boole} υ υ)

       υ _{sequ} ::= (BEGIN υ. . .)

  υ _{decl} ::= (THE ϵ τ υ)

Note that, analogous to the treatment of descriptions, I do not include the LET/LET* sugar forms, although here the LET desugaring cannot be a straightforward substitution due to the possibility of side effects in the bound value domain expressions. Traditionally, desugaring into λ-applications is used, but this of course requires inferring the types of the righthand sides so they can be used in the procedure’s formal parameter type declarations. This is not problematic but it is also not a mere resyntaxing. Nonetheless, we will henceforth consider them to be simple sugar forms.

2.3 Description Equivalence

2.3.1 [Basic Equivalence Axioms]

The following define ≡ to be a congruence relation over description expressions.

δ ≡ δ
δ ≡ δ′ ∧ δ′ ≡ δ′′ ⟹ δ ≡ δ′′
δ ≡ δ′ ⟹ δ′ ≡ δ
δ_{ψ} ≡ δ′_{ψ} ∧ ∀i . δ_{αi} ≡ δ′_{αi} ⟹ (δ_{ψ} δ_{α1} … δ_{αn}) ≡ (δ′_{ψ} δ′_{α1} … δ′_{αn})
δ ≡ δ′ ⟹ δ′′ ≡ δ′′{δ′/δ}

… where δ′′{δ′/δ} denotes δ′′ with the substitution of δ′ for any or all occurrences of δ within δ′′. Although this last rule (substitutivity) follows from the one just above it (“pointwise” ≡), it is nonetheless included here for perspicuity.

2.3.2 [Region Equivalence]

A region can be viewed as a set of region names, possibly parameterized via either Dλ or POLY abstraction.

                  (RUNION ρ )  ≡ ρ

(RUNION ρ ρ …)  ≡ (RUNION ρ…)
(RUNION (RUNION ρ_{1} … ρ_{n}) ρ_{n+1} …) ≡ (RUNION ρ_{1} … ρ_{n} ρ_{n+1} …)
(RUNION ρ_{1} … ρ_{n})  ≡ (RUNION ρ_{π(1)} … ρ_{π(n)})

… for any permutation function π of the positive integers 1 … n.

2.3.3 [Effect Equivalence]

MAXEFF expresses a set of effects ϵ, so axioms analogous to the RUNION axioms above apply: substitute MAXEFF for RUNION and ϵ for ρ. Effects, however, have additional structure:

                               (MAXEFF) ≡ PURE
                         (MAXEFF PURE ϵ) ≡ (MAXEFF ϵ)
             (MAXEFF (READ ρ) (READ ρ′)) ≡ (READ (RUNION ρ ρ′))
             (MAXEFF (WRITE ρ) (WRITE ρ′)) ≡ (WRITE (RUNION ρ ρ′))
             (MAXEFF (ALLOC ρ) (ALLOC ρ′)) ≡ (ALLOC (RUNION ρ ρ′))

Thus, a MAXEFF can be viewed as a set of READs, WRITEs, ALLOCs (each possibly parameterized), irreducible description applications, and Dλ- or POLY-bound effect parameters.

Moreover, a special restriction holds for WRITE effects on the distinguished immutable region @=:

                               (WRITE @=) ≡ error_{effect}
                      (MAXEFF ϵ error_{effect}) ≡ error_{effect}

If we view an effect as describing a set of expressions which will incur (any subeffect of) that effect on the store when evaluated, then error_{effect} describes all expressions, including those which incur illegal effects. Thus, one can view the forbidden effect (WRITE @=) as the top of the effect lattice (⊤_{effect}) since no valid expression will incur this effect. Similarly, effect PURE is the bottom element (⊥_{effect}).

2.3.4 [Type Equivalence]

Pointwise equivalent descriptions are always equivalent. Pointwise inequivalent type expressions are never equivalent, the sole exception being that occurrences of (tag τ) binding pairs within ONEOFs and RECORDOFs^{3} is not order-specific. That is:

(ONEOF ((tag_{1} τ_{1}) … (tag_{n} τ_{n})) ρ) ≡ (ONEOF ((tag_{π(1)} τ_{π(1)}) … (tag_{π(n)} τ_{π(n)})) ρ)
(RECORDOF ((tag_{1} τ_{1}) … (tag_{n} τ_{n})) ρ) ≡ (RECORDOF ((tag_{π(1)} τ_{π(1)}) … (tag_{π(n)} τ_{π(n)})) ρ)

… for any permutation function π of the positive integers 1 … n. This is tantamount to saying that a RECORDOF/ONEOF form consists of a set of (tag τ) binding pairs, where the set of tags must be an irredundant set of identifiers.

2.3.5 [Higher Order Description Equivalence]

The following constitute the familiar α, β and η rules of the λ-calculus, in that order:

∀dvar′ . dvar′ ∉ FDV(τ_{body}) ∪ {dvar …}
(POLY ((dvar κ) …) τ_{body}) ≡ (POLY ((dvar′ κ) …) τ_{body}[dvar′/dvar][…])
(Dλ ((dvar κ) …) δ_{body}) ≡ (Dλ ((dvar′ κ) …) δ_{body}[dvar′/dvar][…])
((Dλ ((dvar κ) …) δ_{body}) δ…) ≡ δ_{body}[δ/dvar][…] iff ∀δ, κ . δ : : κ
(Dλ ((dvar κ) …) (δ_{ψ} dvar …)) ≡ δ_{ψ} iff ∀dvar . dvar ∉ FDV(δ_{ψ})

… where FDV is the Free Description Variables function, defined in the obvious way.

2.3.6 [DLETREC Equivalence]

A DLETREC form denotes a recursive type.^{4} Therefore a DLETREC form is equivalent to any description which is “pointwise” equivalent to its (possibly) infinite unwinding, that is, if corresponding components of the two descriptions are equivalent. Although this could be stated formally using a suitable minimal fixpoint operator (μ), I feel it to be more lucid to leave the DLETREC equivalence axiom in natural language even though an implementation might naturally reduce DLETREC forms to normal form by μ-calculus [Park 76] minimization. The normalization of DLETREC forms is discussed further in Section 3.1.1 and will be fully detailed in a forthcoming technical report based on this work.

3Although the FX-87 manual specifies otherwise [Gifford et al. 87, p.78], I likewise treat the order of binding pairs within RECORDOF types to be not order-specific. This is because the primary motivation for providing RECORDOF types is to support object-oriented programming, which is impeded by making the fields order-specific.

4Note [Gifford et al. 87, p.25] that FX-87 does not permit recursive REGIONs, EFFECTs, or DFUNCs. Therefore, if a DLETREC form’s body denotes a REGION or EFFECT, then the DLETREC bindings could be reordered so that the DLETREC form could be rewritten as an equivalent DLET* form. Likewise if the DLETREC body denotes a non-recursive type. If the DLETREC form’s body denotes a DFUNC form, then it can be rewritten as a Dλ with the DLETREC form contained wholly within the body of the Dλ. These rewritings confine DLETREC forms to denote only recursive types.

2.3.7 [Completeness of the Equivalence Axioms]

Description expressions which cannot be proved equivalent by the above equivalence axioms are by definition not equivalent. Thus, descriptions which are distinct modulo the above equivalence axioms are not equivalent.

2.4 Description Inclusion

2.4.1 [Basic Inclusion Axioms]

The following define ⊑ to be an inclusion/partial-order relation over description expressions.

δ ⊑ δ
δ ⊑ δ′ ∧ δ′ ⊑ δ′′ ⟹ δ ⊑ δ′′
δ ⊑ δ′ ∧ δ′ ⊑ δ ⟺ δ ≡ δ′

The final rule stipulates that inclusion respects equivalence. From these axioms one can deduce the following two substitutivity lemmas, which are useful in practice since they prove the soundness of the “fully connected” lazy normalization strategy proposed in Section 3.2.3:

\frac{δ ≡ δ′}{δ ⊑ δ′′ ⟹ δ′ ⊑ δ′′}  \frac{δ ≡ δ′}{δ′′ ⊑ δ ⟹ δ′′ ⊑ δ′}

2.4.2 [Inclusion Notational Convention]

For the following inclusion rules, I use a non-traditional notational convention that a term with a subscript ‘↓’ is constrained to be in ⊑ relation to the corresponding term with a subscript ‘↑’ on the other side of the inequation. For instance:

(SUBR ϵ_{↓} (τ_{1↑} … τ_{n↑}) τ_{rtn↓}) ⊑ (SUBR ϵ_{↑} (τ_{1↓} … τ_{n↓}) τ_{rtn↑})

is shorthand for the more verbose

ϵ_{↓} ⊑ ϵ_{↑}
τ_{i↓} ⊑ τ_{i↑} ∀i . 1 ≤ i ≤ n
τ_{rtn↓} ⊑ τ_{rtn↑}
(SUBR ϵ_{↓} (τ_{1↑} … τ_{n↑}) τ_{rtn↓}) ⊑ (SUBR ϵ_{↑} (τ_{1↓} … τ_{n↓}) τ_{rtn↑})

Notice the anti-monotonicity in the argument lists. This makes the SUBR rule the most subtle of all the inclusion rules. Intuitively, if we view types as describing values and subtypes as subsets, and if we view a SUBR type τ as denoting a set of procedures which map from a domain to a range with some effect on the store, then the set of procedures which are defined on a possibly larger domain but which always map to a possibly smaller range with a possibly smaller set of side effects on the store will be a subset of the denoted procedures. Thus, any SUBR type τ′ which denotes only elements of this subset is a subtype of τ. The remaining inclusion rules are more straightforward.

2.4.3 [Region Inclusion]

(RUNION ρ_{1↓} … ρ_{n↓}) ⊑ (RUNION ρ_{1↑} … ρ_{n↑})
ρ_{↓} ⊑ (RUNION ρ_{↑} ρ′)

2.4.4 [Effect Inclusion]

(READ ρ_{↓}) ⊑ (READ ρ_{↑})

                          (WRITE ρ_{↓}) ⊑ (WRITE ρ_{↑})
                          (ALLOC ρ_{↓}) ⊑ (ALLOC ρ_{↑})

(MAXEFF ϵ_{1↓} … ϵ_{n↓}) ⊑ (MAXEFF ϵ_{1↑} … ϵ_{n↑})
ϵ_{↓} ⊑ (MAXEFF ϵ_{↑} ϵ′)

2.4.5 [Type Inclusion]

                               VOID ⊑ τ ∀τ

(REF τ_{↓} ρ_{↓}) ⊑ (REF τ_{↑} ρ_{↑})
NULL ⊑ (PAIROF τ τ′ ρ ) ∀τ, τ′, ρ
(PAIROF τ_{↓} τ′_{↓} ρ_{↓}) ⊑ (PAIROF τ_{↑} τ′_{↑} ρ_{↑})
(SUBR ϵ_{↓} (τ_{1↑} ... τ_{n↑}) τ_{rtn↓}) ⊑ (SUBR ϵ_{↑} (τ_{1↓} ... τ_{n↓}) τ_{rtn↑})
(ONEOF ((tag_{1} τ_{1↓}) … (tag_{n} τ_{n↓})) ρ_{↓}) ⊑ (ONEOF ((tag_{1} τ_{1↑}) … (tag_{n} τ_{n↑})) ρ_{↑})
(RECORDOF ((tag_{1} τ_{1↓}) … (tag_{n} τ_{n↓})) ρ_{↓}) ⊑ (RECORDOF ((tag_{1} τ_{1↑}) … (tag_{n} τ_{n↑})) ρ_{↑})
(ONEOF ((tag_{1} τ_{1↓}) … (tag_{n} τ_{n↓})) ρ_{↓}) ⊑ (ONEOF ((tag_{1} τ_{1↑}) … (tag_{n} τ_{n↑})
(tag′ τ′ ) … (tag′′ τ′′ )) ρ_{↑})
(RECORDOF ((tag_{1} τ_{1↓}) … (tag_{n} τ_{n↓})  ⊑ (RECORDOF ((tag_{1} τ_{1↑}) … (tag_{n} τ_{n↑})) ρ_{↑})
(tag′ τ′ ) … (tag′′ τ′′ )) ρ_{↓})

Notice the peculiar rules for VOID and NULL. These state that VOID is the bottom of the TYPE partial order defined by ⊑ and that NULL is the bottom of the PAIROF partial order. There are no values of type VOID and there is a single value of type NULL, namely '(). This treatment of NULL enables us to define the traditional Lisp notion of a list as a null-terminated pair. For instance, the type constructor LISTOF describing homogeneous^{5} lists could be defined as [Gifford et al. 87, p.66]:

     LISTOF  =  (Dλ ((τ TYPE) (ρ REGION))
                   (DLETREC ((listof-τ-in-ρ (PAIROF τ listof-τ-in-ρ)))
                      listof-τ-in-ρ))
For example, (PAIROF INT (PAIROF INT NULL @=) @=) ⊑ (LISTOF INT @=), so one can
say that (CONS 4 (CONS 2 '())) is an instance of a (LISTOF INT @=).

The asymmetry in the latter RECORDOF and ONEOF rules deserves comment. RECORDOF forms describe vectors of data which are accessed by tag. Therefore, viewing types as sets and subtypes as subsets, the set of objects with tag fields in excess of a description is a subset of all objects having at least those tag fields. This is why the subtype RECORDOF is permitted to have more tag/type pairs than the supertype RECORDOF, so long as corresponding fields are in inclusion relation as usual. The ONEOF rule is just the reverse. A ONEOF form describes a single tagged value which may vary in value within the limits of the tag/type pairs stipulated. Therefore, again adopting the subtypes as subsets view, the set of values which are restricted from varying outside a set of tag/type pairs are a subset of those values which are restricted from varying outside a larger set of tag/type pairs, with the usual correspondence inclusion stipulation.

5A heterogeneous list can then be described as a homogeneous list comprised of ONEOF (tagged variant)

elements. E.g., (LISTOF (ONEOF ((i INT)(b BOOLE)) @=) @=) describes an immutable list of immutable elements each of which is tagged with either i or b indicating whether it is of type INT or BOOLE, respectively.

2.4.6 [Higher Order Description Inclusion]

The first two rules below permit POLY and Dλ inclusion in the obvious way. The last rule, by contrast, stipulates that non-β-reducible description application inclusion is by equivalence: because kind information carries no information about whether a DFUNC is monotonic or anti-monotonic in any particular description argument, it is not safe to allow the δ_{ψ} to be in inclusion relation. Moreover, since the operator “tonicity” information is unavailable, inclusion on the operands would likewise be unsafe. This last rule could be deduced from the axioms which constrain inclusion to respect equivalence; it is included here only to draw attention to this tonicity issue. Finally, note [§ 2.2.2] that any δ_{ψ} in normal form will be either a Dvar or will itself be of the form (δ_{ψ} δ …).

(POLY ((dvar κ) …) τ_{body↓}) ⊑ (POLY ((dvar κ) …) τ_{body↑})
(Dλ ((dvar κ) …) δ_{body↓}) ⊑ (Dλ ((dvar κ) …) δ_{body↑})
(δ_{ψ} δ …) ⊑ (δ_{ψ} δ …)

2.4.7 [DLETREC Inclusion]

As noted in the BNF Grammar section, DLET and DLET* may be desugared into underlying forms presented above. Not so for DLETREC. As with equivalence, a DLETREC form is included in another description iff it’s (possibly) infinitely unwound body is “pointwise” included in the description, that is, if corresponding components are in the appropriate (monotonic or anti-monotonic) inclusion relation. Similarly if the inclusion is reversed. The subtleties of DLETREC form inclusion are discussed in excruciating detail in Section 4.2.

2.5 Expression Type and Effect Inference

The following inference rules use a value/description/kind environment (VDKenv) which maps value variables to their values and types and which maps description variables to their descriptions and kinds. If a value variable is an uninstantiated parameter, then this maps only to its type (there being no value). Similarly, uninstantiated description parameters are mapped only to a kind.

Following are a select few type/effect rules intended to convey the interesting features of FX-87 type and effect checking. Note that “:” means “has type”, that “!” means “has effect”, that “::” means “has kind”, that VDKenv[x:y][x::y] denotes environment extension, that δ[δ′/dvar] denotes δ with the substitution of δ′ for all free occurrences of dvar within δ, that FDV(x) selects the free description variables of a description or value expression, and that FV(υ) selects the free value variables of a value expression, where free variables is defined in the obvious way. The subsequent section clarifies some of the less traditional conditions stipulated in some of these rules and mentions a couple subtle issues which these rules suppress.

2.5.1 [Value Variable Type & Effect]

                      VDKenv[var:τ] ⊢ var : τ ! PURE

2.5.2 [Implicit Description Inclusion]

VDKenv ⊢ υ : τ_{υ} ! ϵ_{υ}
τ_{υ} ⊑ τ_{↑}
ϵ_{υ} ⊑ ϵ_{↑}
VDKenv ⊢ υ : τ_{↑} ! ϵ_{↑}

This rule tacitly permeates all the following rules. For instance, in the IF rule below it permits us to write simply ϵ rather than (MAXEFF ϵ_{tst} ϵ_{con} ϵ_{alt}) and simply τ rather than (MAXTYPE τ_{con} τ_{alt}) where:

(MAXTYPE τ_{1} τ_{2}) = \{ \begin{matrix}τ_{1} & if τ_{2} ⊑ τ_{1} \\ τ_{2} & if τ_{1} ⊑ τ_{2} \\ fail & otherwise. \end{matrix}

In the case where (MAXTYPE τ_{con} τ_{alt}) = fail, the IF rule would not apply since the result would not be a proper instance of the type meta-variable τ.

2.5.3 [IF Type & Effect]

VDKenv ⊢ υ_{tst} :  BOOLE  ! ϵ
VDKenv ⊢ υ_{con} :  τ  ! ϵ
VDKenv ⊢ υ_{alt} :  τ  ! ϵ
VDKenv ⊢ (IF υ_{tst} υ_{con} υ_{alt} ) : τ ! ϵ

2.5.4 [λ Type & Effect]

\frac{VDKenv[var_{i}:τ_{i}] ⊢ υ : τ ! ϵ}{VDKenv ⊢ (λ ((var_{1} τ_{1})… (var_{n} τ_{n})) υ) : (SUBR ϵ (τ_{1} … τ_{n}) τ) ! PURE}

2.5.5 [Application Type & Effect]

VDKenv ⊢ υ_{ψ} : (SUBR ϵ_{ψ} (τ_{1} … τ_{n}) τ) ! ϵ
VDKenv ⊢ υ_{i} : τ_{i} ! ϵ
VDKenv ⊢ (υ_{ψ} υ_{1} … υ_{n}) : τ ! (MAXEFF ϵ ϵ_{ψ})

Note that rather than actually allow implicit inclusion of the argument types as the above rule suggests, we must stipulate inclusion modulated by the latent effect ϵ_{ψ} of the operator. This is developed in [§ 6.9]. In this regard, my development differs from the FX-87 Reference Manual. I have chosen to base inclusion on the intuitive notion that types denote sets of values so subtypes should naturally denote subsets. When faced with the safety issue of allowing subtyping on arguments to applications which incur WRITE effects, I prefer to address that concern squarely in the application type checking rule by introducing modulated inclusion there. By contrast, the FX-87 Reference Manual chooses to make the application type checking rule straightforward (as above) while allowing this safety concern to spill over into the inclusion axioms for aggregate types. In that context, the intuitive notion of subtype is burdened with the additional overhead of denoting a subset of values which can safely replace their supertypes in all contexts, consequently requiring each aggregate description inclusion axiom to be conditionalized on the mutability of the region component of the supertype. To repeat, this issue is addressed in detail in [§ 6.9].

2.5.6 [Pλ Type & Effect]

∀var ∈ FV(υ) ¬∃1≤i≤n . dvar_{i} ∈ FDV(VDKenv(var))
VDKenv[dvar_{i} :: κ_{i}] ⊢ υ : τ ! PURE
VDKenv ⊢ (Pλ ((dvar_{1} κ_{1})… (dvar_{n} κ_{n})) υ)

                          : (POLY ((dvar_{1} κ_{1}). . . (dvar_{n} κ_{n})) τ)
                          ! PURE

Consider the quantified conditional in the first clause of this rule. This stipulation avoids capture of description variables appearing within the types of the free variables of a polymorphic expression. This concern was discovered by McCracken and was dubbed the “safe” condition on polymorphic types [McCracken 79, p.20f], hereafter referred to in the text as the McCracken Criterion. Operationally, forward substituting locally defined description variables and systematically α-renaming all locally defined description parameters to avoid collision with globally defined description variables achieves the same effect. Note further the stipulation that the body of the Pλ be PURE. This ensures that projection will incur no run-time expense: projection is entirely static in FX-87. To do otherwise would require an embedded (latent) effect in POLY (like in SUBR) which would be realized upon projecting with PROJ (analogous to the way the application rule realizes latent SUBR effects).^{6}

6In fact, MFX did precisely that [Lucassen 87, Chapt.3] but the designers of FX-87 chose to adopt the

2.5.7 [PROJ Type & Effect]

            VDKenv ⊢ υ : (POLY ((dvar_{1} κ_{1}). . . (dvar_{n} κ_{n})) τ) ! ϵ

VDKenv ⊢ δ_{i} :: κ_{i}
VDKenv ⊢ (PROJ υ δ_{1} … δ_{n}) : τ[δ_{i}/dvar_{i}] ! ϵ

2.5.8 [Implicit Projection Type & Effect]^{7}

∃{δ_{μj}} . ∀dvar_{j} ∈ ⋃_{1≤i≤n}FDV(τ_{χi}) . ∀1≤i≤n . τ_{αi} ⊑ τ_{χi}[δ_{μj}/dvar_{j}]

∀dvar_{k} ∈ FDV(τ) − ⋃_{1≤i≤n}FDV(τ_{χi}) . κ_{k} = REGION

VDKenv ⊢ υ_{ψ} : (POLY ((dvar_{1} κ_{1})...(dvar_{n} κ_{n})) (SUBR ϵ_{ψ} (τ_{χ1} ... τ_{χn}) τ)) ! ϵ
VDKenv ⊢ υ_{αi} : τ_{αi} ! ϵ
VDKenv ⊢ (υ_{ψ} υ_{α1} … υ_{αn}) : τ[δ_{μj}/dvar_{j}][VDKenv(default-region)/dvar_{k}]

                             ! (MAXEFF ϵ ϵ_{ψ})

This rather elaborate quantification over polymorphic parameters (dvar_{j}) in the first clause of this rule formalizes the goal of deducing missing polymorphic projections upon the application of polymorphic procedures by unifying the expected argument types (τ_{χi}) with the types of the application arguments (τ_{αi}) to find a set of of match descriptions (δ_{μj}) which satisfy the implicit inclusion constraints on applications. This issue is addressed in detail in Chapter 5. The stipulation in the second clause that all polymorphic parameters occurring free within the polymorphic procedure’s return type (τ) but not occurring free within the expected argument types be of kind REGION makes it possible for polymorphic procedures to allocate structure in regions independent of the regions spanned by the arguments. FX-87 provides the programmer a mechanism whereby a default-region can be locally re-defined about which these missing region projections should be inferred. This is why the current region description associated with default-region is looked up in the VDKenv and substituted in lieu of these missing inferences. This too is addressed in detail in Chapter 5.

2.6 Auxiliary Verification Rules

2.6.1 [Region Anti-Aliasing]

The projection rule, as stated above [§ 2.5.7], does not allow parallelization of polymorphic procedures about their polymorphization parameters. This is because the FX-87 compiler does compile-time parallelism scheduling/synchronization of a polymorphic procedure’s body upon evaluating its definition, so it must anticipate all possible interference patterns which projection may introduce. Thus, since no information can be assumed about how the polymorphized parameters will eventually be projected, if the compiler actually used the rule as stated above then it would have to compile a Pλ with the assumption of maximal interference/sharing regarding these parameters. To combat this sequentializing pessimistic assumption, the FX-87 Reference Manual stipulates that it be considered a static error for any projection to take place which might actually introduce interference/sharing patterns about these polymorphization parameters [Gifford et al. 87, p.40]. This allows the compiler to recover parallelism in the compiled Pλ body by entitling it to assume instead that there need be no sequentialization with respect to the parameters, but this comes at the cost of a static restriction. This restriction can be relaxed: it is excessively conservative to forbid all interference/sharing with respect to these parameters when all that is necessary is to forbid any new interference/sharing. Consequently, the Region Anti-Aliasing Rule on which this restriction is based can be made more effective than its definition in the FX-87 manual. This issue of interference/sharing will be explored in detail in a forthcoming technical report based on this work.

more conservative approach proposed in [Ibid., Chapt.7].

7This inference rule is based strongly on one presented to me by James O’Toole.

2.6.2 [Effect Masking]

The final subtlety lurking within the type and effect inference rules is the notion that side effects to the store which are locally visible within a block induce local synchronization on the processes which execute the procedure. However, side effects which are not observable outside of some lexical contour should not induce synchronization outside of that contour. The rule which approximates this goal is called the Effect Masking Rule [Gifford et al. 87, p.30]. This rule was formalized and its soundness was proposed by Lucassen in [Gifford et al. 87, Appendix B: FX Semantics]. This issue is addressed in Chapter 6, where again the groundwork established in [Gifford et al. 87] is refined.

2.7 Soundness of the Type and Effect Inference Rules

Lucassen [Lucassen 87] conjectured the soundness of the Type and Effect Inference Rules for FX-87. This means, in short, that the type and effect of an expression, as inferred by these rules, is a conservative estimate of the actual type and effect of the expression. As a consequence, the compiler writer can use these rules as a basis for various optimizations of the object code. As mentioned in Section 1.2, these include automatic storage reclamation (e.g., via stack allocation) of variables and formals whose values are not returned out of the scope of their definition (i.e., those of local extent), memoization (software caching) of pure expressions, common subexpression elimination of pure expressions, dead code elimination of expressions of type VOID, code motion within side-effect boundaries, and parallelization of non-interfering expressions. Again, the inference soundness further entitles us to avoid type checking at run time, along with its associated potential time and space inefficiencies.

36 CHAPTER 2. FX-87 OVERVIEW [This page intentionally left very nearly blank.]

FIX Equivalence/Inclusion Testing

In the overview section, I introduced a strategy for equivalence/inclusion testing which I dubbed algorithmic complexity slicing. Here I detail the specifics of how this technique is used in the FIX implementation design of FX-87. Afterward, I justify this approach on an operational basis rather than appealing to the more abstract justification presented in the overview.

3.1 Algorithmic Complexity Slicing in FIX

As stated in the overview, our approach to inclusion testing is first to try equivalence testing, lazily reducing the compared terms to their normal forms but only so far as is necessary. This gradual normalization is memoized and the results are hashed so that subsequent equivalence tests may be performed in constant time. Moreover, when more general inclusion testing is warranted, these inclusion results too are software-cached. An introduction to the details of this approach follow. Subsequent chapters elaborate.

3.1.1 Gradual Reduction to Normal Form

The idea behind algorithmic complexity slicing is to perform normalization in several phases, each phase performing as much reduction as possible within a (gradually increased) time bound. It is desirable that no phase require repeating subsequent to a later phase. In FX-87 this happens to be the case, but this may not hold for more intricate axiom systems. In FIX there happen to be four phases. They are briefly mentioned in the following table along with their time bounds. A more detailed description of each phase is presented in the subsequent sections to make plausible the claimed running times and to explain the rationale behind this particular choice of phases, as well as to informally suggest the correctness of this normalization strategy. Algorithms for each phase will be presented in excruciating

38 CHAPTER 3. FIX EQUIVALENCE/INCLUSION TESTING

/ ↘
/  ↘/  /\

                         /  ↘/  /\         /  \
                        /  /\         /  \       /    \
                       /\         /  \       /    \     /      \
                      /  \       /    \     /      \   /        \
                     /    \     /      \   /        \ /          \
                    /      \   /        \ /          \            \
                   /        \ /          \            \------------
                  /          \            \------------ RECTYPE-Norm
                 /            \------------    Order  O(α n lg n)
                 --------------- αβη-Norm O(n lg n)
                    Retract  O(n)

O(n)

Figure 3-1: The FIX Normalization Strategy

detail in a forthcoming technical report.

[Phase 0]: Grammar Retraction....... O(n) .............. Rewrites input descriptions to eliminate syntactic sugar forms, to explicate omitted optional syntax, and to normalize other variant syntactic forms.^{1} This phase also flattens the namespace to avoid lexical scoping concerns and to separate the value and description namespaces.

[Phase 1]: αβη-Normalization.......... O(n) ............. Normalizes descriptions with respect to the familiar λ-calculus reduction axioms of Section 2.3.5.

[Phase 2]: Order Normalization....... O(n lg n) ......... Normalizes those descriptions whose components constitute a set. This involves normalization with respect to those axioms in Section 2.3.2–2.3.4.

[Phase 3]: RECTYPE Normalization... O(α n lg n) ... Normalizes descriptions containing recursive type expressions. Rather than axiomatize this normalization phase, a detailed discussion of the process will appear in a forthcoming technical report.^{2}

Phase 0: Grammar Retraction

The source grammar of descriptions is flexible, allowing omission of default terms and various sugar forms and other convenient variant syntaxes. The first phase of processing any input expression is to simplify these terms to a minimal subset of the input language grammar. This, in effect, implements a linear-time transformation of programs into a retracted grammar. In addition, lexical scoping is obviated by eliminating shadowing within expressions.

1See [Gifford et al. 87] for details.

2See [Cardelli 89] for the axiomatization, the correctness and possibly completeness of which are to be addressed in a forthcoming publication by Luca Cardelli and Roberto Amadio [Cardelli 90em].

3.1. ALGORITHMIC COMPLEXITY SLICING IN FIX 39

This is done by subscripting locally introduced parameters according to the lexical contour of their introduction. This I call α-flattening to distinguish it from α-normalization, done in the next phase, which completely renames local parameters to conform to a position-based nomenclature. Although not a phase specific to the normalization process, this performs a crude first step toward normalization, a step which greatly simplifies subsequent processing of all expressions. Details of this retraction will be presented in a forthcoming technical report.

Phase 1: αβη-Normalization

The first phase of the normalization process proper is to normalize the descriptions with respect to the familiar λ-calculus axioms of α-, β-, and η-conversion. The β-reduction is performed as a straightforward forward-substitution where the arguments are normalized before being substituted (so-called “applicative order” reduction). At each stage of the bottom-up return from this top-down forward substitution, any remaining Dλ expression is η-reduced as appropriate. This requires testing if any of the formal parameters occur free in the operator of the Dλ-body, which can be accelerated by returning, along with the β-reduced description, the set of free Dvars of the body operator. Finally, as the top-down substitution is performed, Dλ and POLY lexical contour height information is propagated down to enable bottom-up normalization of parameter names in a fashion similar to deBruijn’s “nameless parameter” normalization [de Bruijn 72].^{3} This threefold normalization phase is therefore accomplished in a single linear-time top-down/bottom-up pass over the description.^{4} After this phase, all non-ordering, non-RECTYPE-containing (sub)descriptions will have been fully normalized. For them, the following phases implement the identity function.

Phase 2: Ordering

As noted in the equivalence axioms [§ 2.3.2–2.3.4], RUNIONs and MAXEFFs correspond to sets; RECORDOF and ONEOF forms have order independent fields. Each such construct can be normalized by sorting the components according to a lexicographical ordering. For RECORDOF and ONEOF forms this is a simple alphabetical ordering on fieldnames (which are SYMBOLs). RUNIONs and MAXEFFs are slightly more complicated.

For RUNIONs, we must consider that aside from the easily sorted region identifiers (SYMBOLs) an RUNION may contain α-normalized POLY or Dλ region parameters or even β-irreducible description applications (of resultant kind REGION), all of which are represented in the underlying Scheme implementation as structured data (LISTs). For example, consider the region component of the REF in:

3Of course, deBruijn numbers must be recomputed upon subsequent β- or η-reduction arising from projection of POLY parameterized Dλs. To avoid this complication, I use “inverse” deBruijn numbers, which are βη-insensitive. This is detailed in a forthcoming technical report.

4Due to testing for free Dvar intersection at each step and to possible renumbering of some parameters upon normalizing a non-reduced Dλ-form, this is something like 3n in time and n in space. Note that I ignore the possible O(n^{2}) blow up arising from multiple β-reductions of a single Dλ argument: each application of a Dλ results in a fresh copy of its body with the appropriate β-substitutions. The graph sharing techniques of Lévy’s so-called “optimal” λ-calculus reductions could alleviate this [Levy 80] [Kathail 89].

                 (POLY ((r  REGION))
                        (rf (DFUNC (REGION) REGION))
                   (REF INT (RUNION r (rf @RED))))

It contains two POLY-bound region parameters (r and rf), one of which is the operator of a β-irreducible description application ((rf @RED)).

In sorting RUNIONs, each of the aforementioned four classes of object— literal, POLYbound parameter, Dλ-bound parameter, and description application— are separated into a separate subset, which are sorted separately. This sorting is performed as a single bottom-up linear pass over the description expression. As a bottom-up process, β-irreducible description applications can safely be sorted based on their textual appearance.^{5}

MAXEFF forms are treated similarly: READ, WRITE and ALLOC effects are sorted into separate subsets,^{6} as are the POLY and Dλ effect parameters and the β-irreducible description applications of kind EFFECT. Note that again the bottom-up sorting process assures a unique normal form for each distinguishable description.

Insofar as each of these sorts is a comparison-based sort, the running time of this phase is O(n lg n).^{7} The space is O(n) since in general an entire new copy of the description will be constructed. This copy space could be alleviated by tagging each subexpression that contains (or is itself) a description which is to be sorted, enabling the Ordering phase to avoid traversal (and hence copying) of any subdescription that is not so tagged. This tagging decoration can be performed by the preceding αβη-Normalization phase without violating its O(n) time or space.

After the Ordering phase, all non-RECTYPE-containing (sub)descriptions will have been fully normalized. For them, the following phases implement the identity function.

Phase 3: RECTYPE-Normalization

The recursive-type normalization phase proceeds in three sub-phases (presented here out of order for pedagogical reasons). The underpinnings of these sub-phases is substantially more complicated than the previous phases. For that reason, a forthcoming technical report will be dedicated to a full treatment of this RECTYPE-Normalization phase.

[μ]. RECTYPE-Minimization— Recursive type expressions denote directed cyclic type structures. As such, they correspond to directed cyclic graphs, which in turn correspond to deterministic finite automata (DFAs) [Coucelle 83].^{8} As a consequence of the Mihill-Nerode theorem, a DFA has a unique normal form (modulo state renaming) [Hopcroft & Ullman 79, Theorem 3.10, p.67f]. Thus, as a DFA, a RECTYPE can be normalized via DFA minimization.^{9} The current algorithm of choice for such DFA minimization runs in time O(α n lg n) where α is the size of the input alphabet [Aho & Ullman 86, §3.9, pp.141–144] [Aho, Hopcroft & Ullman 74, §4.13 Partitioning, pp.157–162] [Hopcroft 71]. For our encoding, α is the arity of the highest arity subexpression, which in practice can be assumed to be a constant probably less than about 8. Note that the correctness of this minimization process relies on the fact that non-RECTYPE subdescriptions will have been fully normalized before this sub-phase is initiated. It is therefore crucial that recursive types not appear within RUNION or MAXEFF forms since otherwise the minimization would not necessarily preserve the ordering done in the pre-RECTYPE-normalization phase. Fortunately, RECTYPEs can appear there only as arguments to description functions which return a region or effect, hence they are irrelevant to the application result. Heretofore unmentioned, the αβηphase recognizes these irrelevant RECTYPE occurrences and replaces them with the distinguished description IRRELEVANT. This desensitizes the RECTYPE-Minimization sub-phase to their occurrence, thus preserving correctness.

5For instance, this can be accomplished by constructing a STRING textually identical to the application then sorting the applications by these associated strings.

6This corresponds to left-to-right application of the EFFECT/RUNION homomorphism axioms [§ 2.3.3].

7This assumes a constant cost for each comparison operation. Since symbol names are usually less than say twenty characters long and since programmers tend to choose naming conventions which exhibit good Hamming distances anyway, this is probably a reasonable assumption. Moreover, hashing could be employed to improve the comparison performance should it prove problematic in practice by say sorting on hash index rather than on textual appearance. Unfortunately, such a strategy would require re-sorting of normalized descriptions stored in “compiled” FX-87 files which are re-loaded into a fresh run-time environment. Fortunately, though, the subsequent RECTYPE-normalization phase is not sensitive to the particular total order used.

8As noted in [Lucassen 87, §7.3.1 Recursive Descriptions, p.109ff].

[χ]. RECTYPE-to-DFA— The DFA-minimization sub-phase presupposes a RECTYPE-to-DFA transformation sub-phase. The linear-time transformation of a RECTYPE-containing description into a DFA is the μ-calculus [Park 76] analog of supercombinator λ-lifting in the λ-calculus, a technique developed for graph reduction implementations of functional programming languages [Peyton-Jones 87]. This transformation can be folded into the αβη-normalization phase since it does not violate the linear running time of that phase and since the resulting supercombinator is not violated by the subsequent Ordering phase. Furthermore, the local information needed for correct λ-lifting is naturally collected already within the αβη-normalization phase so it is natural to perform it it there.

[α]. RECTYPE α-Normalization— Once the RECTYPE-DFA has been minimized, it is in a unique normal form modulo the naming of states. The final step, therefore, is to normalize the state names of the now-minimized RECTYPE-DFAs (i.e., α-normalize the DLETREC formal parameters). This can be accomplished by an O(n) numbering of states as per their distance from the distinguished start state (the encoding of the DLETREC body). This is followed by an O(n) distribution sort of the DLETREC binding list as per these numberings. No β-reduction phase to re-reduce lifted forms is necessary, but may be convenient. Again, this would be O(n).^{10}

In sum, the RECTYPE-Normalization phase is an O(α n lg n) phase. Finally, note that the RECTYPE-Normalization phase applies only to RECTYPEs and descriptions which contain RECTYPEs. Thus, just as with ordering forms in the previous phase, the αβη-Normalization 42 CHAPTER 3. FIX EQUIVALENCE/INCLUSION TESTING phase can tag descriptions accordingly to avoid unnecessary traversal and copying. Again, more detail on these phases will be provided in a forthcoming technical report.

9This fact, as well as the algorithm for translating RECTYPE notation into DFAs, were brought to my attention by Prof. David McAllester

10Again, actually O(n^{2}) worst case, which is unlikely to occur in practice. See the similar comments regarding β-reduction in footnote 4 on page 39.

3.1.2 Description Nodes

Data caching of normalization is performed as follows: whenever the type/effect checker generates a description for a value expression, what is actually generated is a description node. A description node is a 5-tuple where the zero^{th} element records the current degree of normalization of the node, the first element is the result of applying Phase 0 to the source description, and each subsequent element is the delayed result of applying the next phase of partial normalization to the previous phase’s result.^{11} Assuming the result of each phase to be hashed, corresponding memoized phases of two descriptions can be compared for equivalence at unit cost (the cost of a hash table lookup) while allowing subsequent phases to be lazily computed from the preceding phases.

In subsequent sections, I will use the following notation:

node[i] — the i^{th} element of the description node Φ_{i}(descr) — the result of performing Phase i of normalization on a description; assume that the Φ_{i} are memoizing procedures

N_{0}(node) — node[1] = the result of applying Φ_{0} to the source description N_{i}(node) — Φ_{i}(node[i]) for 1 ≤ i ≤ MaxPhase N^{o}(node) — the current degree of normalization of the description node, i.e., the current maximum normalization phase which has been performed (and hence memoized) on that node; a pretty alias for node[0]

MaxPhase — the maximum phase of normalization performed (in FIX, this is 3)

11In a functional programming style implementation, one would use a hashing-CONS [Field & Harrison 88] to maximize sharing and to memoize the normalization phase computations with respect to these hashed structures. In portable Scheme, which alas does not provide hashing-CONS [Rees & Clinger 86], this could be approximated efficiently by making each “result” be a pair comprised of the actual LIST structure result and an interned SYMBOL whose print name is a string constructed to look textually identical to that LIST structure. In this way, description equivalence tests could be reduced to testing pointer equality on the interned SYMBOLs, while the subsequent phases could memoize on this SYMBOL, resorting to structure traversal only as necessary. The difficulty with these approaches comes from maintaining the memoization table and the hashing table. A native hashing-CONS would maintain the hash table, just as interning relies on the native Scheme symbol table being maintained. The problem of maintaining the memoization could be achieved through data-caching in the hashing-CONS approach by making each subnode of a description node be itself a full description node, thus relying on the maximal sharing among hash-CONSes and on the lazy normalization within each node. Unfortunately, no such efficient memoization strategy can be concocted in portable Scheme since no mechanism is provided for mutating interned objects. That is, no OBJECT-HASH is provided nor is it portably implementable in a way appropriately informative to the garbage collector. The same garbage collection problem arises if one tries to implement the normalization phases as memoizing procedures. This garbage collection issue will be further considered below in Section 3.1.5. For the sake of the above discussion, however, I will assume a hashing-CONS implementation.

3.1.3 Description Node Equivalence Testing

TO TEST node1 ≡^{?} _{node} node2 DO
   FOR i FROM 0 TO MaxPhase DO
     WHEN N_{i}( node1) ≡^{?} N_{i}( node2)
        RETURN TRUE
   FALSE

where ≡^{?} tests for hash equality (i.e., EQ?)

TO COMPUTE N_{i}(node) DO
   WHEN i ≰ N^{o}( node) ;; Data not cached in node?

node[i + 1] := Φ_{i}( N_{i−1}( node))

         N^{o}( node) := N^{o}( node) + 1

   node[i + 1]

Figure 3-2: Description Node Equivalence Algorithm

Testing the equivalence of two description nodes is done by comparing corresponding elements of the description nodes until a match is discovered. This lazily forces normalization of the two descriptions only so far as necessary, in worst case resulting in full normalization of both descriptions.^{12}

Note that any effort to detect early ultimate failure of equivalence is not fruitful since if equivalence ultimately fails, inclusion will usually be attempted. Thus, proceeding with the gradual reduction to normal form will not be for naught since the more general inclusion testing process cannot proceed on non-normalized descriptions anyway.

12Note that if hash-CONSing is used with memoizing Φ_{i}, then nodes which become noticeably equivalent at some phase will become pointer equal at that element of the node. Thus subsequent incremental normalization of one of the nodes will eventually be shared by the other node. An alternative to memoizing the Φ_{i} is to manually inherit normalization whenever a less normalized node is proven equivalent to a more normalized node: the less normalized node can copy the elements from the more normalized one. This allows inheritance to spread despite the lack of memoization. Such manual inheritance of normalization is reminiscent of Tarjan’s Union/Find algorithm for computing equivalence classes [Tarjan 83]. Finally, note that manual inheritance could be useful even in the memoized case if the memo table is fixed in size so that some memo entries are eventually discarded. Again, more on this in Section 3.1.5.

3.1.4 Description Node Inclusion Testing

TO TEST node_{↓} ⊑^{?} _{node} node_{↑} DO
     IF node_{↓} ≡^{?} _{node} node_{↑}
        THEN TRUE
        ELSE TEST N _{MaxPhase}(node_{↓}) ⊑^{?} N _{MaxPhase}(node_{↑})

where ⊑^{?} is detailed in Chapter 4

Figure 3-3: Description Node Inclusion Algorithm

As mentioned above, we will resort to the general inclusion test only once equivalence testing has failed, even then invoking it only on fully normalized descriptions. This general inclusion testing process consists of a straightforward data-directed dispatch to recursive inclusiontesting handlers,^{13} one such handler for each distinct description inclusion axiom [§ 2.4]. This dispatch, of course, terminates early when it is discovered that the two compared descriptions are incompatible, particularly when no handler exists for the present pair of subdescriptions. This early detection of failure is well-motivated since, as noted in the introduction to FIX [§ 0.4.4], computing the MAX over a collection of descriptions will in general require several inclusion tests, many of which will fail because it is not known a priori which description is in fact the maximum of the others.

Inclusion of RECTYPEs is somewhat more complicated. It involves a generalization of the RECTYPE equivalence algorithm of ALGOL 68 [van Wijngaarden et al. 76] to handle the more general inclusion. This is discussed in more detail in a Section 4.2. The only other complication in inclusion testing involves Implicit Projection, which is discussed at length in Chapter 5.

For now, suffice it to say that most inclusion axioms are O(n), the few subset tests over ordered forms is O(n lg n), and the inclusion over RECTYPEs can be as bad as lcm(n, m) for two descriptions of size n and m, respectively, which in worst case can be O(n^{2}). The concern over Implicit Projection within inclusion testing does not further aggravate this running time since the discovery of an implied projection of a parameter will be roughly tantamount to an inclusion test against each of its occurrences within its binding description. Again, excruciating detail is postponed. The upshot is that inclusion testing can be as bad as O(n^{2}), so avoiding inclusion tests and bailing out early from failing inclusion tests is probably well worth the trouble if the bookkeeping overhead is not excessive, which it is not in the strategy proposed here.

13This data-directed dispatch style is described in [Abelson & Sussmans 85, §2.3.3].

3.1.5 Data Caching of Inclusion Results

Finally, a word about memoization of inclusion results is in order. As with equivalence memoization, inclusion tests can software-cache their results within the description nodes themselves. Specifically, as with Union/Find over equivalence classes, description nodes can maintain a set of heretofore known inclusion relations, both successful ones and nonsuccessful ones. Such a caching in effect lazily constructs a complete inclusion lattice for each description by caching pointers to known inclusion-reachable nodes as well as maintaining a roster of known inaccessible ones to accelerate inclusion failures. For heavily traveled regions of the global inclusion lattice, this may well be a worthwhile pursuit. However, less traveled regions will likely not justify the space consumption of their memoized neighbor-pointers. Probably some form of fixed-size cache of description inclusion relations should be distributed throughout the description nodes using a “least recently used” (LRU) replacement strategy [Ward & Halstead 89]. A similar technique should be used within the memoizing procedures used during normalization (viz., the Φ_{i}) to fix the size of the memoization table maintained by each procedure.

Further, since description expressions are associated with the specific value expression for which they are a description, short-lived value expressions will have descriptions with comparably short-lived immediate utility. Thus, pointers to descriptions of non-global value expressions should perhaps not be indefinitely cached within other description nodes’ caches. Perhaps it would be worthwhile pursuing a generational-style garbage collection algorithm [Lieberman & Hewitt 83] to reclaim space occupied by pointers to effectively defunct descriptions. Globally defined descriptions would naturally be immune to this purging since, by globally defining a description or globally defining a value for which this is a description, the programmer has in effect declared a desire for the description to be considered permanent. Note that this concern is not as critical for fixed-sized memoization tables using a Least Recently Used (LRU) replacement strategy since the garbage collectible entries will presumably eventually be discarded from the cache naturally.

Clearly, consideration of inclusion memoization is far more involved than mere equivalence inheritance, suggesting issues of resource management and dynamic utility measurement characteristic of large complex systems competing over fixed resources. Investigating how these systems issues can interplay in the setting of static program analysis is a compelling area for future research.^{14} 3.2. RE-EVALUATION OF THE FIX EQUIVALENCE/INCLUSION TESTING STRATEGY47

14I graciously acknowledge [Field & Harrison 88, Chapt.19 Memoization] for inspiring this perspective.

3.2 Re-evaluation of the FIX Equivalence/Inclusion Testing Strategy

In the remainder of this chapter, I re-evaluate the effectiveness of the algorithmic complexity slicing strategy from an operational viewpoint. To point, I focus on what pressures FX-87 exerts on an efficient inclusion procedure and reconsider how well the FIX strategy satisfies these pressures. I do this by contrasting the strategy in FIX against a more idealized fullyconnected inclusion strategy which will be described below.

3.2.1 Design Pressures Revisited

Below I re-evaluate the effectiveness of the design strategy of FIX. First, as argued in the introduction to FIX, our major efficiency concern is with computing the MAX of two (possibly recursive) descriptions. Recall [§ 0.4.4] that computing a MAX is tantamount to deciding which of two descriptions includes the other, so the MAX problem is really just the inclusion problem in disguise … but with a twist: in computing a MAX, it is not known a priori which of the two descriptions is the MAX. Therefore, in the worst case two inclusion tests must be performed to find the MAX, meaning that there is pressure to do early detection of failing inclusion tests. This is a secondary pressure in the design, which is to say that it should not direct the design but when convenient the design should relieve this pressure somewhat. Another primary concern is with Implicit Projection. As stated earlier, Implicit Projection entails one-way unification by inclusion. This reinforces the concern for efficient inclusion, but it also introduces a new concern: how to do efficient inclusion matching over sets. (Recall from the description equivalence axioms [§ 2.3.2– 2.3.4] that regions and effects are essentially just sets.) This new concern is addressed in Chapter 5. For now, let us pursue the issue of efficient description inclusion testing.

3.2.2 Efficient Inclusion Testing

First, notice that when testing inclusion of descriptions in practice, actually testing general inclusion is usually overkill— that is, usually mere equivalence testing suffices. This is fortunate since equivalence is often much more efficient to verify than inclusion.^{15} Therefore, our first step toward efficient inclusion is to first try equivalence; only when that fails do we then try the more expensive strict inclusion. Note that this motivates early detection of failing equivalence tests, just as MAX testing encouraged early detection of failing inclusion. Again, this is a secondary design goal. The main point is that the problem of efficient inclusion in this way motivates the problem of efficient equivalence. This is the topic of the next section, after which I return to the specifics of the more general efficient inclusion testing per se.

3.2.3 Efficient Equivalence Testing

Testing the equivalence of two description expressions involves gradual normalization of the expressions. This normalization can be done on the fly or in a prepass. The advantage of on-the-fly normalization is that the normalization need happen only on demand; the disadvantage is that it need happen with every comparison. The prepass alternative is more clearly memoizable, which has the advantage of being done once only but the disadvantage of always having to be done once. A hybrid of the two is desirable: a mixture which performs on-the-fly memoized normalization. Specifically, only at the point where two non-normalized descriptions fail to appear to be equivalent need the equivalence traversal perform normalization. This seems to advocate a more fully-connected description normalization tree as depicted below, where each △ is meant to depict an entire subdescription of the description tree:

15See Section 0.2.2 for a detailed discussion.

/ ↘
/  ↘/  /\

                         /  ↘/  /\         /  \
                        /  /\         / /\       /\ \
                       /\         / /\       /↘/ \     / | \
                      / /\       /↘/ \     / △ \/ / \|  \

                     / / \     / △ \   /  /\ /  ↓  \
                    / △ \   /  /\ /  ↘/ \  △  \
                   /  /\ /  ↘/ \  △ \------------
                  /  / \  △ \------------ RECTYPE-Norm
                 /  △ \------------    Order
                --------------- αβη-Norm
                    Retract

Figure 3-4: An Idealized Fully-Connected Normalization Strategy

This could be implemented by internally representing description expressions as trees of description nodes, each subtree itself being a description node. For brevity, I will hereafter assume these nodes to contain only the Phase 0 flattened version and the (delayed, memoized) fully normalized version, which I will simply call the normalized version.

To take advantage of this more fully connected configuration, the comparison code could “pointwise” compare source descriptions by comparing their corresponding components. Only upon failure of equivalence at some internal pair of nodes would it compare, and hence force, the delayed normalized elements. Unfortunately, this requires a complicated traversal. In sum, it minimizes traversal and normalization but at the expense of a highly conditionalized comparison traversal.

3.2. RE-EVALUATION OF THE FIX EQUIVALENCE/INCLUSION STRATEGY 49

In effect, then, in a fully connected implementation the normalization process will have infiltrated and permeated the equivalence comparison process. This is probably not a good trade-off: perhaps it is overkill. It seems to presume that even though some late normalization phase (e.g., RECTYPE normalization) may be required on some internal nodes, there is no motive to proceed with normalizing the entire tree with respect to that phase. This may well be true, but fully normalizing with respect to a phase is easily amortized over the lifetime of the tree, so I suspect it to be worthwhile. That is, I suspect there will be temporal locality on the normalization axiom calls. Unfortunately, too little code has actually been written in FX-87 to provide conclusive data on the actual complexity of comparisons needed in FX-87 programs. Thus to pursue a design strategy which so aggressively tries to do as little normalization as is absolutely necessary seems unwarranted. Further, since the conditionalized traversal and the delay/memoization mechanisms are always employed regardless of their necessity, this style of comparison permits the cost of trying to avoid the more expensive comparisons to spill over into the cost of performing easier ones. Expending energy to avoid work is bad economics.

I therefore opt to back off from this aggressively lazy style to a more casually frugal style. The idea is that some amount of normalization will be done early— that amount which can be trivially amortized into the cost of kind checking— but full normalization of descriptions will be done only when necessary. Further, by using hash-CONSing, we need not traverse two descriptions to establish equivalence: we need only check for top-level confluence (i.e., pointer equality). As above, making each description be a linkage of each successive phase of (delayed) normalization permits hashing and memoization of separate phases of normalization without resorting to memoizing procedures. By contrast, however, note this carefully: in this frugal approach it is the entire description that will be normalized when the comparison test initiates a top-level normalization traversal; in the aggressively lazy approach only those subcomponents which needed be, were normalized. Let us consider the trade-offs between these two competing strategies.

Before proceeding, it is useful to ease the mind of the imperative-minded programmer by considering an additional alternative: normalization via repeated mutation of the flattened description. The argument goes something like this: “Why not normalize descriptions as needed but do it by mutation (i.e., in-place) rather than by memoization of several versions? After all, in this way only one copy of a description need be maintained. Moreover, the normalized components could be tagged to avoid trying to re-normalize.” Unfortunately, this would complicate the normalization traversal by making it conditionalize upon whether to try a mutation normalization: it would require tagging each subnode with what normalization phases have yet to be (mutationally) applied to that subtree. Further, mutation would eliminate the possibility of accessing the old version once the normalization has occurred. This would forfeit all the advantages of maintaining the less normalized versions; namely, we would lose the confluence property of hash-CONSed forms resulting from hash-CONSing a Phase i normalized form by invoking the Phase i normalization process on the Phase i − 1 hash-CONSed result. Consequently, we would lose the desirable constant time equivalence test. Moreover, the idea of mutation is a dangerous one: were a FIX implementation to be translated into FX-87 itself, mutation of this sort could severely limit potential parallelism in the verifier. It also would force descriptions to be allocated in mutable regions, which may not be as efficient as immutable storage. We therefore restrict consideration to aggressively lazy and casually frugal approaches, discounting the mutation approach.^{16}

Having restricted the discussion to lazy versus casual, let’s consider their relative merits to see what trade-offs FIX makes by adopting the casual stance. Foremost, the casual approach facilitates coarse grain monitoring of the extent to which each normalization phase is actually needed, providing useful data about the potential economics of competing designs. With the lazy approach, it is unclear what to conclude from the more fine grained monitoring information that would result. Thus, the casual approach is perhaps more suitable for an early experimental implementation. Second, unlike the non-hashing lazy approach, the casual traversal process needn’t continually conditionalize on the components of an aggregate description representation. Instead, this sort of conditionalization occurs only at the topmost level: if source versions fail to be equivalent, the flattened versions are compared, then the normalized version but only as a last resort. Performing this conditionalization at the topmost level only, rather than throughout the structure, significantly reduces the conditionalization in the traversal, albeit at the expense of possibly doing three separate traversals to establish equivalence. Thus, the casual approach performs more normalization than may be necessary, amortizing this extra effort over the lifetime of the description nodes, while the lazy approach performs a more heavily conditionalized, comparison-based normalization. The bottom line then is that the casual approach trades normalization time (maybe) for simplified traversal, delayed full normalization, and the ability to easily monitor the statistical need for full normalization of descriptions in FX-87 programs. This sounds like a good trade-off for an early experimental implementation.

16Of course, there can be benefits from benevolent side-effects. For instance, mutation is the basis of the Tarjan Union/Find algorithm [Tarjan 83]. Other less obvious benefits of benevolent mutation are considered in [Eastman & Laird 87, p.21–23].

Let’s pause here to characterize the apparent presumptions of this casual style of traversal without resorting to an operational/implementational description. First, it seems to presume that comparison of source versions is usually sufficient to prove equivalence. Second, when this trivial comparison fails, it seems to presume that minimal normalization (like substitution of locals for their occurrences) will suffice. Finally, only when necessary are the more expensive operations performed, for instance full flattening and ordering of forms like RUNION. Moreover, it presumes that once a normalization phase is needed at one node, it is likely to be required elsewhere in the description as well. Finally, it presumes that a single description will be used in several different contexts; thus memoizing this work so that any undue normalization which may be performed as a consequence of this full phase normalization can nonetheless be amortized over the lifetime of the description concerned. These are probably an accurate set of presumptions given that programmers usually develop coherent programming habits such as globally defining commonly occurring descriptions and pre-normalizing their descriptions or at least presenting them in internally consistent ways that readily facilitate the trivial equivalence test. That is, programmers present code which they themselves can easily verify, which implies easy verification by machine, which in turn implies avoiding the need for complicated mechanisms such as flattening and ordering.

3.2.4 Return to Efficient Inclusion Testing

Having meticulously considered the issue of equivalence, how then does inclusion testing proceed when the easier equivalence test has failed? Recall [§ 3.1.4] that the equivalence test trades the cost of doing possibly several comparison traversals against the cost of doing full normalization, the assumption being that the comparison will rarely progress that far; however, once equivalence has failed, one must resort to inclusion traversal. Three phases of that traversal could likewise be done, but the motivation (viz., avoiding full normalization) is by then defunct. Is there any reason to suspect then that trying source traversal first will win? Possibly. Again, there is too little experience writing FX-87 programs to justify a committal answer, so it is useful to implement the traversal to provide this missing information. By the same token, given that by the time equivalence has been ruled out the descriptions have already been traversed three times, it seems ill-advised to compound this with possibly three more traversals, especially since hashing will not accelerate inclusion testing. A compromise can be struck by trying the source versions first, then upon failure trying the normalized versions. This provides the desired information while avoiding illmotivated traversal. Unfortunately, inclusion traversal is the most expensive aspect of FX-87 type-checking. Thus, FIX currently resists doing even the source traversal. An implementation flag to selectively enable/disable this feature would probably be beneficial for information gathering.

3.2.5 Summary of Efficient Equivalence/Inclusion Testing

To summarize this involved design derivation: implicit subtyping makes efficient inclusion testing a primary concern. This, in turn, makes efficient equivalence testing a concern since mere equivalence is usually sufficient to demonstrate inclusion and since equivalence is less expensive to test. Beyond these criteria there is little statistical data to pressure the design in any specific direction. Therefore, as an experimental design, FIX stratifies the description environment into frames that map description variables to increasingly normalized versions of their associated descriptions. The cost of these gradual-normalization stages range monotonically from O(n) to O(n lg n). Insofar as equivalence testing can, in worst case, force full normalization, equivalence testing therefore costs O(n lg n). Strict inclusion testing costs O(n^{2}), but is attempted only after equivalence has failed. Thus, the cost of inclusion testing gracefully degrades from O(n) to O(n^{2}) depending on the axioms needed to establish an answer. Such is the objective of algorithmic complexity slicing. This O(n^{2}) worst case cost could have noticeable impact for sufficiently large n, which will likely be the case for large, hierarchically structured software systems based on wide-spread structural inclusion. For instance, object-oriented programming systems (OOPS) should be sensitive to these bounds. Many implementation alternatives exist but at least this approach offers a means for acquiring the statistical information necessary to qualitatively argue their relative merit. In the absence of such information, the most we can hope for is an experimental implementation that readily avails us to it so that subsequent implementations can benefit accordingly. I now proceed with consideration of a few of the secondary design pressures mentioned above since the strategies for relieving these secondary pressures naturally build on the ones already illustrated.

3.2.6 Exploitation of Decorations

Recall [§ 3.1.1 & 3.1.1] that tagging of descriptions was encouraged to accelerate the normalization process. So long as we go to the trouble of installing these decorations, we may as well capitalize on their presence to optimize other operations as well. There are two situations where FIX does precisely that: early termination of futile inclusion comparisons and efficient instantiation of parameterized descriptions. First, tagging can provide coarse grain structural information about a description. This allows early termination of a doomed inclusion test. For example, if a description expression containing two free description parameters is tested for inclusion in one which contains only one free parameter, the test clearly fails: only their normalized versions have a prayer of demonstrating equivalence (for example, the extraneous parameter could be discarded as a result of a β-reduction). In short, the Free Dvar status needed for η-reduction could be exploited by the inclusion process since such information can be sufficient for an early negative decision without necessarily exploring a detailed justification. Thus, if this openness status were embedded within the descriptions as a local decoration, then we will have annotated the openness status of each branch of an aggregate description. Consequently, when performing substitution such as β-reduction or projection, this information can be further exploited to avoid pointlessly traversing closed paths (or, more aggressively, paths which are open but which contain no free references to the specific parameters currently being instantiated). By avoiding this gratuitous traversal we thereby avoid the copying which it entails.^{17} Note finally that this optimization requires no additional computation beyond what is already needed by the normalization phases: FIX simply exploits the information that is latent in the openness status by preserving it within the description, thereby improving the efficiency of the implementation with minimal increase in code complexity. This decoration in effect elevates descriptions into being annotated parse trees, an implementation strategy common in conventional compiler design [Aho & Ullman 86, §5.1, pp.280–287]. In a sense then, we may view the normalization of descriptions not as being a denotational abstract interpretation but as being a denotational abstract compilation, or in more common parlance, as being a partial evaluation of descriptions. This brings us full circle, back to the perspective in the introduction: that type checking value expressions is an abstract interpretation process with respect to the type inference axioms. Similarly, description normalization is an abstract interpretation of descriptions with respect to the description equivalence axioms. This interpretation can be lazily performed as necessary while applying the description inclusion axioms to two descriptions.

17Recall [§ 3.1.1] that the β-reduction phase of FIX performs copy substitution since a parameterized description will in general be instantiated several times in several distinct contexts, discounting instantiation via mutation. An alternative approach, traditional in compilers’ treatment of parameterized value domain expressions, is to treat the expression as a closure consisting of the parameterized body and an environment template in which to place values for the parameters upon instantiation. The parameter references within the body are then treated as references into this environment template. A new copy of this template is generated for each instantiation so the instantiation can proceed via mutation of this template. This is fine for value expressions since they do not admit strong equivalence tests, but it is unsatisfactory for description expressions. That is, this strategy makes instantiation more efficient but it complicates strong equivalence testing. For example, a parameterized description which has been instantiated must be indistinguishable from the substituted equivalent that it denotes; however, by implementing parameterized forms as closures, the two would structurally differ. Thus, the equivalence test would need to either collapse the closure via substitution or accumulate local state for the bindings and resolve the references on the fly. FIX implements instantiation via substitution to emphasize efficient comparison at the expense of efficient instantiation. This is a good trade-off since the overhead of parameterization should not be charged against non-parameterized expressions. Further, by eagerly substituting, FIX amortizes the cost of substitution across all subsequent comparisons made against the instantiated form. I conjecture that most parameterized descriptions will be instantiated before used, making this too is a good trade-off. Interestingly, this approach is suggestive of the graph reduction implementation techniques popular among functional programming language implementations [Peyton-Jones 87] [Field & Harrison 88].

Description Inclusion Algorithm

4.1 The Problems

Determining if two normalized descriptions are in inclusion relation involves the inclusion axioms of Section 2.4. Most of these axioms are straightforward “pointwise” inclusion axioms, meaning that if corresponding components of two aggregate descriptions are in the appropriate inclusion relation (monotonic or anti-monotonic) then the aggregate descriptions are in recursion relation. It is the non-pointwise axioms which give rise to a sophisticated inclusion system. Specifically, the pointwise-subset inclusion axioms over RECORDOF/ONEOF fieldnames and RUNION/MAXEFF components lead to inclusion axioms over structurally dissimilar descriptions. This tolerance for structural dissimilarity in inclusion is further enhanced by the NULL and VOID types, the respective bottom elements of the PAIROF type sub-lattice and the whole type lattice. In addition, recursive types denote infinite trees of varying degrees of unrolling, which can be (finitely) tested for pointwise inclusion. Finally, SUBR types exhibit anti-monotonic^{1} inclusion in the argument types, further complicating the inclusion test.

Why is this a problem? After all, inclusion testing can be implemented as a data-directed pointwise test of the inclusion axioms. There are two complications. First, inclusion testing over recursive types is a bit subtle. This is a complication inherent in the inclusion axioms themselves. As will be shown, this is not excessively difficult, its just a bit non-obvious. Second, and more important, is to consider in what situations inclusion testing is performed by a type checking system. Were it the case that every inclusion test must succeed in a well-typed program, then there would be no complication. Unfortunately, this is not the case in FX-87, nor in any other flexibly typed programming language. The difficulty arises from two sources: Implicit Subtyping and Implicit Projection.

First, FX-87 supports Implicit Subtyping. This means, among other things, that the various branches of a conditional expression need not produce values of equivalent type. Rather, it only need be the case that one of the branches produces a value whose type includes the types of the other branches. This type is called the maxtype of the branch types. It is not known a priori which branch produces this maxtype so in general many inclusion tests are required to find the maxtype. On average, one would expect half these inclusion tests to fail. This encourages early detection of failing inclusion tests, which straightforward pointwise inclusion testing does not provide.

1Here I follow the terminology of [Lucassen 87]. The usage is that the expected pointwise inclusion relations are “monotonic” whereas the reverse-inclusion with respect to argument components of SUBR types is “anti-monotonic”.

Second, FX-87 supports Implicit Projection. This means that when a polymorphic procedure is applied, it need not first be explicitly projected to yield a non-polymorphic procedure if the missing projection arguments are unambiguously inferable from the types of the application arguments. In general, then, in the process of inferring these missing projection, a projection parameter may be subjected to numerous simultaneous inclusion constraints, some bounding from above and some from below. To determine the satisfiability of these constraints one must determine the tightest upper and lower bound, then verify their satisfiability. The difficulty again is in finding the tightest (max or min) of several unrelated inclusion constraints. This reinforces our concern for early termination of failing inclusion tests since again it is not known a priori which will be the max/min.^{2}

To summarize this second point of concern then, we are pressured to provide early termination for failing inclusion tests. This pressure is asserted by the Implicit Subtyping and Implicit Projection features of FX-87 which will presumably be pervasively exploited in FX-87 programs. Of course, this is not surprising since these are the very features that make the FX-87 typing system an interesting backdrop for this thesis.

In the following sections then, I return to the more sedate issue of recursive type inclusion, after which I address the concern for early termination of failing inclusion tests. Remember throughout that the general inclusion test is initiated only on fully normalized descriptions which have been shown to be inequivalent.

4.2 Inclusion on Recursive Types

The algorithm for testing inclusion over recursive types is an adaptation of a similar algorithm for equivalence over recursive types used in ALGOL 68 [van Wijngaarden et al. 76, §7.3, pp.103–107] and more recently presented in [Aho & Ullman 86, §6.7, pp.376–380]. To simplify the discussion in this section, I will suppress all region and effect components of type expressions and ignore the possibility of DFUNC forms: their appearance would have no significant bearing on what follows. With that, consider the two recursive type expressions:

τ _{example↑} = (PAIROF INT (PAIROF INT (RECTYPE t (PAIROF INT t))))
τ _{example↓} = (PAIROF INT (RECTYPE t' (PAIROF INT (PAIROF VOID t'))))

where (RECTYPE t τ) is a shorthand for (DLETREC ((t τ)) t).^{3} Now imagine that each type expression denotes a graph, where this graph is cyclic for recursive types. It is not difficult to show that τ_{example↓} ⊑ τ_{example↑} noting that ∀τ . VOID ⊑ τ [§ 2.4]. The following algorithm outlines the strategy. Essentially, it does a data-directed dispatch [Abelson & Sussmans 85, §2.3.3] on the two descriptions being compared, maintaining a trail of assumptions and a local binding stack.

2This problem becomes particularly sticky when one considers the subset axioms, since the inference is via ACI-unification. Careful consideration of how to perform this in reasonable time without backtracking is a hard problem in its own right. It will be presented in Section 5.8. For now, our interest is only in the pressure that Implicit Projection asserts on rapid inclusion failure detection.

3The general DLETREC-to-RECTYPE linear transformation algorithm will be presented in a forthcoming technical report.

TO COMPUTE τ_{↓} ⊑^{?} τ_{↑} WRT μ-env_{↓} assumed-⊑ μ-env_{↑} assumed-⊒
   WHERE μ-env_{↓} maps RECTYPE formals in τ_{↓} to their RECTYPE bindings
         μ-env_{↑}  "  τ_{↑}  "
     assumed-⊑ is a set of formulæ: RECTYPE formal μ_{↓} ⊑ δ_{↑}
     assumed-⊒  "     RECTYPE formal μ_{↑} ⊒ δ_{↓}
DO
  [τ_{⊥}]. IF τ_{↓} ≡ VOID THEN TRUE
  [τ_{∅}].  IF τ_{↓} ≡ NULL AND τ_{↑} = (PAIROF τ τ′) THEN TRUE
  [τ _{base}]. IF τ_{↓} ≡ τ_{↑} THEN TRUE
  [REF]. IF τ_{↓} = (REF τ′_{↓}) AND τ_{↑} = (REF τ′_{↑})

         THEN τ′_{↓} ⊑^{?} τ′_{↑} WRT μ-env_{↓} assumed-⊑ μ-env_{↑} assumed-⊒

    ⋮  Similarly for PAIROF, RECORDOF, ONEOF, SUBR, and POLY ("tonicity")
  [RECTYPE_{↓}]. IF τ_{↓} = (RECTYPE μ_{↓} τ_{μ↓})

THEN τ_{μ↓} ⊑^{?} τ_{↑} WRT μ-env_{↓}[μ_{↓} ↦ τ_{μ↓}] assumed-⊑ ∪ {μ_{↓} ⊑ τ_{↑}}^{‡}

                               μ-env_{↑}  assumed-⊒
  [RECTYPE_{↑}]. IF τ_{↑} = (RECTYPE μ_{↑} τ_{μ↑}) THEN <dual case to [RECTYPE_{↓}]>
  [μ_{↓}]. IF τ_{↓} IS A RECTYPE FORMAL μ_{↓}
        THEN IF μ_{↓} ⊑ τ_{↑} ∈ assumed-⊑ THEN TRUE
             ELSE μ-env_{↓}(μ_{↓}) ⊑^{?} τ_{↑} WRT μ-env_{↓} assumed-⊑ μ-env_{↑} assumed-⊒
  [μ_{↑}]. IF τ_{↑} IS A RECTYPE FORMAL μ_{↑} THEN <dual case to [μ_{↓}]>
  OTHERWISE FALSE
‡Or just assumed-⊑ if τ_{↑} contains no free RECTYPE formals

Figure 4-1: RECTYPE Inclusion Algorithm

The basic strategy is as follows: To test if two types are in inclusion relation, assume that they are. Now traverse them in lockstep testing for pointwise inclusion. If a point inclusion fails, then the inclusion assumption has been contradicted, so return FALSE. If one can successfully traverse the types up to a point where an inclusion assumption has already been made, then the types are indeed in inclusion relation (by lack of contradiction), so return TRUE. The traversal will always halt since either a failure will be encountered or else the traversal will eventually loop to an already assumed inclusion point. For a more careful informal argument of total correctness see the last section of this chapter.

Note two points of interest: First, two distinct inclusion assumption trails are maintained, viz., assumed-⊑ and assumed-⊒. This is necessary to avoid crosstalk between the description expressions— that is, a rectype formal μ_{1} in type 1 may not correspond to rectype formal μ_{1} in type 2. Rather than maintain a trail of correspondences, I opt to gather two separate inclusion trails. This has the added advantage of reducing the size of each trail by, on average, half, which in turn accelerates lookups (or insertion if done by hashing). Second, note in [RECTYPE_{↓}] the (footnoted) conditionalization of extending the assumption set on whether τ_{↑} contains free RECTYPE formals (i.e., is in the lexical scope of a RECTYPE). This is done to avoid making inclusion assumptions until both descriptions being traversed have entered into a RECTYPE body [hereafter called a looping configuration since both expression are elements of a cyclic subgraph]. Note further that, in contrast to the ALGOL 68 algorithm, the only time we make an assumption is when a RECTYPE formal has been encountered [hereafter called an entry-point configuration since it denotes an entry into a looping configuration]. This is because configurations achieved subsequent to the entry point that are not themselves entry-point configurations within a loop cannot assist in early exit from that loop since we terminate at the very first configuration that has already been achieved once. This will be precisely at an entry-point configuration since any subsequent configuration can be achieved only by first looping back to an entry point then proceeding. One could accumulate all configurations in order to memoize the inclusion of common subexpressions within type expressions but this makes the assumption list grow linearly with the least common multiple (LCM) of the loop-lengths of the two type expressions (rather than the LCM of the number of RECTYPE formals bound in each loop, as in our algorithm), whereas occasions for successful early termination by virtue of this rampant memoization are presumably unlikely and would be attributed to pure coincidence. If not due to pure coincidence, then a local name should have been introduced.^{4} Note that for non-recursive common subexpressions, inclusion memoization within the description nodes could provide this acceleration without burdening the (lexical) assumption trails. At any rate, since assumptions in our algorithm involve only RECTYPE formals and are used only locally within the recursion, we should expect a significant performance improvement in practice over the ALGOL 68 algorithm.

Both these points were independently discovered by Luca Cardelli in his implementation of Amber [Cardelli 90em]. The type checking rules corresponding to this appear in [Cardelli 89]. Cardelli is currently working on a paper to prove the soundness (and maybe completeness) of this approach [Cardelli 90em].

4Indeed, RECTYPE normalization performs this common subexpression elimination. This will be detailed in a forthcoming technical report.

4.3 Early Termination of Failing Inclusion Tests

In this section I consider how early termination of failing inclusion tests might be supported by decorating normalized descriptions with structural information which the inclusion checker could use. This decoration would constitute an early warning system for structure yet to be traversed by the inclusion procedure. Note that our motivation is to detect when we are trying say ⊑ over two types when it is actually ⊒ that succeeds. We have no interest in accelerating failures which occur in both directions since this invariably indicates a programmer error. Thus, we are interested only in decorating facts about tolerable structural dissimilarities between types. Intolerable ones are irrelevant with regards to early failure detection.

4.3.1 Tolerable Dissimilarities

To point, the non-trivial inclusion axioms mentioned at the head of this chapter depict three distinct possibilities for structural dissimilarity between included forms. These are:

1) the RUNION/MAXEFF and RECORDOF/ONEOF subset axioms, 2) the VOID/NULL bottom axioms, and 3) the RECTYPE unwinding traversal (not actually axiomatized in this thesis). One final consideration rounds out the concerns for structural dissimilarity: occurrences of Implicit Projection unification variables [hereafter called matchvars] during Implicit Projection inference can match against potentially any description expression.

This information could be used to terminate inclusion testing when, for instance, a node is encountered in the presumed supertype which is known to contain a RECTYPE in a monotonic position which cannot be ignored (i.e., it does not occur within a ONEOF field). If the presumed subtype cannot account for this non-ignorable RECTYPE by supplying a RECTYPE or a bottom element, then the inclusion will clearly fail, so it can terminate early. This reduces the turn-around time on testing inclusion in the other direction, which should presumably succeed. Although this will at best make maxtype computations run only a factor of two faster (by quickly homing in on the correct direction of inclusion to test), this could be important: consider that the slowest computation performed by the entire FX-87 type checking system is to determine inclusion in the presence of subset and rectype axioms. The subset testing is O(n lg n) and the rectype inclusion traversal is worst case LCM(n, m) which is O(n^{2}) where n and m are the sizes of the two compared types. Reducing the constants in these phases of type checking could prove crucial.

4.3.2 Decorations for Early Failure Detection

As suggested by the above hypothetical instance, what needs to be annotated within type expressions to facilitate early failure detection includes: 1) occurrences of RECTYPE forms, 2) occurrences of bottom forms, 3) occurrences of matchvars, 4) whether these RECTYPE forms may potentially be ignored, and 5) the tonicity of these occurrences. The ignorability of a RECTYPE (case 4) arises from the subset axioms on field occurrences within RECORDOF and ONEOF forms, which actually spawns two separate subcases: i) occurrences within RECORDOF fields, and ii) occurrences within ONEOF fields. This can be further extended to facilitate early failure detection on RUNION/MAXEFF occurrences by annotating say 6) the maximum size of any RUNION and MAXEFF subexpression within a type and 7) any occurrences of matchvars within any RUNION and MAXEFF occurrences, again distinguishing the tonicity of any occurrences and noting their ignorability. All these internal annotations correspond to non-standard evaluations of descriptions, just as descriptions themselves correspond to non-standard evaluations of value expressions. Naturally, these annotations could be axiomatized but I will not pursue that level of detail here.

Alas, this seems to be a large amount of information to annotate within a type. In general, it could more than double the size of each type expression, offsetting the benefit we aim to achieve. However, all this information could be carefully packed into bitvectors and Boolean flags so the the overhead of annotation could be substantially reduced. This presumes that the precision of such information be reduced to mere presence annotation rather than actual profiles of say which field tag of a RECORDOF/ONEOF form contains a RECTYPE. For such minimal information to be of value, it should probably be sprinkled throughout the type expression rather than merely being wrapped at the outermost level. Perhaps sprinkling it at say every third branching level would suffice rather than decorating every level within the type. No experiments have been explored for such an acceleration technique for inclusion testing— indeed, I believe this to be an original idea— but similar crude structural information is put to good use for equivalence checking in many modern languages such as C [Aho & Ullman 86, §6.3, pp.352–359].

Finally, some of this information is already provided by the normalization process, for instance to annotate if the ordering or rectype normalization phases need to be performed. The decorations which provide this information are rough annotations of occurrences of RUNION/MAXEFF, RECORDOF/ONEOF, and RECTYPE occurrences within a type as well as its free variables (potential matchvars). To annotate these decorations a wee bit more precisely to contain information about tonicity, size, and RECORDOF/ONEOF-containment is a small additional amount to pay which could reap respectable rewards. Unfortunately, without this additional information the existing annotations would be useless for accelerating inclusion failure.

Clearly, this issue of decorations to accelerate failing inclusion is a topic for future exploration.

4.4 Informal Total Correctness Argument^{5}

4.4.1 Termination

The program always terminates because each successive recursive call to ⊑^{?} makes progress towards termination by further lockstep-traversing the input expressions, augmenting the assumption lists if this is a looping entry-point configuration. Each element of the assumptions list is a pair of subexpressions of the two input expressions. No such pair can ever occur more than once in the assumptions list since the routine returns immediately before it gets a chance to add a duplicate entry. There is a finite number of such pairs, so this process cannot go on forever.

4.4.2 Correctness

A recursive type expression approximates an unbounded class of structurally recursive values. Syntactically, a recursive type expression like (RECTYPE τ (PAIROF INT τ @R)) is equivalent to an infinite “unwinding” produced by repeatedly substituting the RECTYPE form for occurrences of the RECTYPE formal in the RECTYPE body. For example,

  (RECTYPE τ (PAIROF INT τ @R))
     ≡ (PAIROF INT (RECTYPE τ (PAIROF INT τ @R)) @R)
     ≡ (PAIROF INT (PAIROF INT (RECTYPE τ (PAIROF INT τ @R)) @R) @R)

⋮

     ≡ (PAIROF INT (PAIROF INT (PAIROF INT (PAIROF INT . . . @R) @R) @R) @R)

Type inclusion is similarly defined in terms of these unwindings. Because of the way our algorithm treats variables and RECTYPE-expressions, the effect of the case analysis (ignoring the way it terminates by using assumptions) is to traverse the infinite unwindings, checking for appropriate inclusion (monotonic or anti-monotonic) at corresponding component subexpressions. There are two cases in this pointwise comparison:

1. The Types are in Inclusion Relation, that is, the infinite trees are in inclusion relation. In this case, we must show that the program returns true. It was shown above that it terminates, and it is clear by inspecting the various termination conditions that it can only return false if the infinite trees are not in inclusion relation at some node, for example, by there being a BOOLE in one tree at a point where in the other tree there is a (PAIROF t1 t2). Therefore the program can return true only when the trees are in inclusion relation.

5The following argument is adapted from Jonathan Rees’ presentation of the recursive-type equivalence algorithm correctness proof in [van Wijngaarden et al. 76, §7.3, pp.103–107].

2. The Types are not in Inclusion Relation, that is, there exists an inclusion mismatch in the infinite trees. When the algorithm terminates it will have traversed certain finite subtrees of the two trees. Call the nodes the traversal was examining when it exited X and X′. Assume that there exists a mismatch between the infinite trees which is not in the subtrees that the program examined, and consider the paths from the roots down to these mismatch subtrees. Call the highest mismatch between these two subtrees on this path nodes M and M′. We argue that the termination at X and X′ must have returned false.

     Dexp1             Dexp2
       /\                /\
      /  \ B            /  \ B'
     .   /\            .   /\
    .   /  .          .   /  .
       /\   .            /\   .
      /  \              /  \
     /\   M            /\   M'
    /  .              /  .
   X    .            X'   .

The program followed some initial segment of the paths to M and M′ but decided to terminate the comparison at nodes X and X′, apparently before considering the mismatch at M and M′. The only way it could have terminated is to have reached either another mismatch (thus returning false, which would be correct) or to have encountered a pair of nodes which it has already seen and thus already assumed to be in inclusion relation (returning true, which would be incorrect), where these two nodes appear above the M/M′-containing paths (else it would not have terminated the entire comparison). Call these already-encountered nodes B and B′. We show that this latter case leads to a contradiction as follows: Imagine it were possible. Then, the type expression for B is in inclusion relation with that for B′ (by assumption with lack of contradiction), so the infinite trees under these nodes must also be in inclusion relation. On the other hand, since the trees at M and M′ have a mismatch, so do the trees at B and B′. Thus, either B was not in inclusion relation with B′ (so X is not in inclusion relation with X′, a contradiction) or else the mismatch paths leading to M and M′ appear higher on the trees than B and B′ (contradicting our assumption that we could terminate already). Thus either there exists no such mismatch nodes M and M′ or else the program will find them and return false.

This completes the two subcases, and hence the argument.

Note that the program will consider a type like (RECTYPE t t) to be in inclusion relation with any other type since no contradiction to this assumption will be discovered. This, in effect, equates (RECTYPE t t) with the bottom of the description partial order.

Implicit Projection via Abductive Inference

In mathematics, the greatest degree of self-evidence

is usually not to be found quite at the beginning, but at some later point;

hence the early deductions, until they reach this point,

give reasons rather for believing the premises because true consequences follow from them,

than for believing the consequences because they follow from the premises. — BERTRAND RUSSELL, Preface to Principia Mathematica (1910)

5.1 Overview

In this chapter I detail the problem of Implicit Projection. In short, Implicit Projection involves pattern matching over algebraic sets, where the match test is by description inclusion. Viewing this matching problem as a match over an equational theory [Yelick 85], the matching involved has been called C-pattern subsumption for RECORDOF/ONEOF forms, ACIpattern subsumption for RUNIONs and ACIUZH-pattern subsumption for MAXEFFs. I present an original algorithm for solving these problems without backtracking that runs in time linear in the number of match variable occurrences within the pattern match. Specifically, the Implicit Projection matching problem is formalized as a soundness preserving reverse induction over the axioms of description equivalence [§ 2.3] and inclusion [§ 2.4]. This reverse induction I call abductive inference. The algorithm which implements it achieves a linear running time through a bookkeeping strategy I call flexibility indexing.^{1}

5.2 Implicit Projection as Context Resolution

A polymorphic procedure is one that can be applied to arguments of varied types. For example, the LENGTH primitive polymorphic procedure of FX-87 takes as argument a (homogeneous) list of objects of some type t and returns an integer describing the length of that list. The type of the LENGTH primitive (ignoring regions and effects) is therefore

(POLY ((t TYPE)) (SUBR ((LISTOF t)) INT)).

1Prof. David McAllester has noted that this is tantamount to an algorithm for testing the satisfiability of Horn clauses in time linear in the number of terms.

To apply a polymorphic procedure to values, one must first project the POLY onto appropriate descriptions. For example, to apply the LENGTH primitive to a list of Booleans, one would first do (PROJ LENGTH BOOLE). Of course, this makes for verbose code:

((PROJ LENGTH BOOLE) '(#T #T #F #T))
==> 4 : INT      ;; Note that ": <type>" means "has type <type>"

Instead, one would like to rely on an inference algorithm^{2} to infer these projections. Thus, rather than explicitly projecting each polymorphic procedure upon application, the projections could be left implicit, to be inferred from the types of the arguments supplied. In FX-87 this is an important feature since nearly every primitive FX-87 procedure either creates or manipulates structured data allocated in some region. Thus, nearly every primitive procedure in FX-87 is polymorphic in a region description, and often also polymorphic in the component types of these structured arguments [Gifford et al. 87]. Insofar as every user-defined procedure in any language ultimately derives from the language primitives, this means that nearly every user defined procedure will likewise be polymorphic, at least if the programmer respects the abstract spirit of the language by promoting program sharing through polymorphization. It is therefore expected that FX-87 programs will make ample use of implied projections to avoid the distracting verbosity of explicit projections that can be easily inferred by both the program writer and, hence, the type checker. An application involving implied projection is said to be an Implicitly Projected Application, or just an Implicit Projection.

FX-87 supports Implicit Projection. This means that when a polymorphic procedure is applied, it need not first be explicitly projected to yield a non-polymorphic procedure if the missing projection arguments are unambiguously inferable from the types of the application arguments. For example, consider (again ignoring regions and effects):

(DEFINE duplicate (Pλ ((t TYPE))  ; A user-defined polymorphic duplicator
                    (λ ((x t))
                      (CONS x x))))
==> duplicate : (POLY ((t TYPE)) (SUBR (t) (PAIROF t t)))
(duplicate 0)
==> (0 . 0) : (PAIROF INT INT)

Here it was not necessary to explicitly project duplicate onto INT since this projection is easily inferred by noting that a (SUBR (t) …) was being applied to a value of type INT. Thus, Implicit Projection is tantamount to inferring a substitution for the implicitly projected POLY parameters. This substitution must satisfy all those typing constraints imposed on the projection parameters by their appearance within the declared types of the formal parameters of the polymorphic procedure being applied.

The necessary inference is more general than the above simple example suggests. For example, the procedure application rule permits the type of the application arguments to be subtypes of the declared expected types. Therefore, our inference is performed over the inclusion axioms. Consider:

2For example, something analogous to the Robinson unification algorithm used in Hindley-Milner type inference systems for inferring types of value expressions [Milner 78].

(DEFINE apply-twice (Pλ ((t TYPE))  ; The polymorphic APPLY-TWICE procedure
                      (λ ((f (SUBR (t) t))
                          (x t))
                        (f (f x)))))
==> apply-twice : (POLY ((t TYPE)) (SUBR ((SUBR (t) t) t) t))
(apply-twice SQUARE 2)   ;; where  SQUARE : (SUBR (INT) INT)
==>  16 : INT

The difficulty here arises from two sources: first, a projection parameter may occur multiple times within the declared formals’ types so it will in general be simultaneously constrained by many descriptions, and second these constraints can vary from monotone to anti-monotone occurrences.^{3} Specifically, within the declared type of f, t appears in both a monotonic and an anti-monotonic position. It also appears in a monotonic position in the declaration for x. Thus, when resolving these occurrences against the actual argument types, three constraints are imposed on the projection parameter t: two from above and one from below.

In general, whenever an application of the form:

(f e_{1} … e_{n}) where f : (POLY ((ν_{μ 1} κ_{μ 1}) … (ν_{μ m} κ_{μ m}))

(SUBR (τ_{χ 1} … τ_{χ n}) τ _{rtn}))

e_{1} : τ_{α 1}
⋮
e_{n} : τ_{α n}

is encountered, the goal of the implicit projection procedure is to find description bindings for the parameters ν_{μi} satisfying τ_{αi} ⊑ τ_{χi}— that is, to find bindings for the match variables [hereafter called simply matchvars] satisfying the constraints that the argument types be included in the expected types. Henceforth, M will denote a fixed but arbitrary set of matching constraints imposed by an implicit projection problem. These matching constraints will be of the form τ_{αi} ⊑ τ_{χi} where the matchvars ν_{μj} occur only within the expected types τ_{χi}.

3Here I follow the terminology of [Lucassen 87]. The usage is that if δ[ν] is a description containing ν, the occurrence of ν within δ is monotone if ω ⊑ ν ⊢ δ[ω] ⊑ δ[ν]. It is anti-monotone if ν ⊑ ω ⊢ δ[ω] ⊑ δ[ν].

In general, M might be a complex set of simultaneous inequations. For example (again, ignoring regions and effects):

((Pλ ((ν_{μ 1} TYPE) (ν_{μ 2} TYPE))
   (λ ((filter (SUBR (ν_{μ 1} ν_{μ 2}) ν_{μ 1}))
       (header ν_{μ 1})
       (signal ν_{μ 2}))
     (filter header signal)))
 (λ ((ctxt-str STRING)
     (irritant (ONEOF (b BOOLE) (i INT))))
   (LET ((err-str (TAGCASE irritant
                    ((b) "BOOLE")
                    ((i) "INT"  ))))
     (ERROR (STRING-APPEND ctxt-str " encountered an unexpected " err-str)
            irritant)))
 "Example"
 (ONE (ONEOF (i INT)) 42))

produces the following match constraints:

(SUBR (STRING (ONEOF (b BOOLE) (i INT))) VOID) ⊑ (SUBR (ν_{μ 1} ν_{μ 2}) ν_{μ 1})
                                        STRING ⊑ ν_{μ 1}

                               (ONEOF (i INT)) ⊑ ν_{μ 2}

Notice that the matchvars ν_{μj} occur only on the righthand sides of the inequations. Any choice of matchvar bindings satisfying these constraints must likewise satisfy the constraints.

         STRING ⊑ ν_{μ 1} ⊑ STRING

(ONEOF (i INT)) ⊑ ν_{μ 2} ⊑ (ONEOF (b BOOLE) (i INT))

Notice here that there are bounds on both sides of the matchvars.

For maximal generality the implicit projection match procedure returns not just a single substitution, but rather a set of bounds. This we call a resolution context since it delineates a context within which any choice of substitution would resolve the constraints in the matching problem M. More formally,

Definition 5.2.1 A resolution context is a set of inclusion formulæ of the form:

\{ \begin{matrix}δ_{↓1} ⊑ ν_{μ1} & ν_{μ1} ⊑ δ_{↑1} \\ ⋮ & ⋮ \\ δ_{↓m} ⊑ ν_{μm} & ν_{μm} ⊑ δ_{↑m} \end{matrix} \} such that for all i, \{\} ⊢_{⊑} δ_{↓i} ⊑ δ_{↑i}

Henceforth, C will denote a fixed but arbitrary context.

The process of solving an implied projection, then, is the process of finding such a context C given a set of matching constraints M. Formally, a solution to M is defined to be a context C such that C ⊢_{⊑} M, where ⊢_{⊑} is the inference relation generated by the inclusion axioms of [§ 2.4].

More precisely, the goal of the context resolution process is to find the most general such context in the sense that any other context will be “more confining”. Formally, a solution C of M is most general if for all other solutions C′ we have C′ ⊢_{⊑} C.^{4}

This is summarized by the following definitions:

Definition 5.2.2 The resolution context C is a solution of the constraints M if C is a context satisfying:

• C ⊢_{⊑} M

Definition 5.2.3 The resolution context C is the most general solution of M if C is a solution of M satisfying:

• For any resolution context C′, if C′ ⊢_{⊑} M then C′ ⊢_{⊑} C

5.3 Abductive Inference

One question remains: precisely how are the bounds in C induced by the inclusion axioms from the matching constraints M? Specifically, how does one transform the constraints in M into bounds on the matchvars ν_{μj}? The intuition is that if we are to prove that the constraints M are satisfied for some instantiation, then we can deduce this only by inference over the inclusion axioms. Thus, when trying to infer the set of possible instantiations which would prove M, we “run the inclusion axioms backward” to infer those premises which must be satisfied if we are to deduce M. Whenever a premise of the form ν_{μi} ⊑ δ_{↑i} or δ_{↓i} ⊑ ν_{μi} is reached, then these inclusion goals are added to the set of induced constraints.

This reverse inference over the inclusion axioms might be called abductive inference. It can be defined as inference over the axioms induced from the inclusion axioms by the following abductive transform:

Definition 5.3.1

The abductive transform of an inference rule \frac{α_{i} ; ⋮ ; α_{n}}{β}  is the set of rules \frac{β}{α_{1}} … \frac{β}{α_{n}}

4Viewing ⊢_{⊑} as a partial order on contexts, we note that the space of contexts C_{i} inferred from M over the description inclusion axioms forms a complete partial order (cpo) with least upper bound C_{∞}. That is, ∀C_{i} ∈ {C | C ⊢_{⊑} M} . ⨆ C_{i} = C_{∞}. Thus, the implicit projection problem reduces to finding this least upper bound of the contexts induced from the matching constraints M with respect to the inclusion axioms.

For example, consider the inclusion axiom for REF types:

\begin{matrix}τ_{↓} & ⊑ & τ_{↑} \\ ρ_{↓} & ⊑ & ρ_{↑} \\ (REF τ_{↓} ρ_{↓}) & ⊑ & (REF τ_{↑} ρ_{↑}) \end{matrix}

The abductive transform of this inclusion rule is the pair of inference rules:

      (REF τ_{↓} ρ_{↓}) ⊑ (REF τ_{↑} ρ_{↑})              (REF τ_{↓} ρ_{↓}) ⊑ (REF τ_{↑} ρ_{↑})

τ_{↓} ⊑ τ_{↑}  ρ_{↓} ⊑ ρ_{↑}

Now we define ⇝ (read “abduces”) to be the inference relation generated by the abductive transforms of certain inference rules given in Section 2.4. For instance, from the above REF example, one might write:

(REF τ_{↓} ρ_{↓}) ⊑ (REF τ_{↑} ρ_{↑}) ⇝ τ_{↓} ⊑ τ_{↑}

From this ⇝ relation we can derive constraints from sets of constraints in the obvious way.

Of course, such abductive inference is not in general sound since the conclusion of an abduction axiom is not “proved” by the premises. However, the relation ⇝ satisfies the following Abduction Soundness Condition:

Definition 5.3.2 An abduction relation ⇝ is abductively sound when:

If M ⇝ ψ then for any context C, if C ⊢_{⊑} M then C ⊢_{⊑} ψ.

In other words, if M ⇝ ψ then ψ must follow from any solution to M.

5.4 Abduction over Inclusion

The abduces relation ⇝ includes the abductive transformations of the tonicity description inclusion axioms [§ 2.4], that is, all the inclusion axioms except^{5} for the inclusion axioms for regions [§ 2.4.3] and MAXEFF [§ 2.4.4] and the latter axioms of RECORDOF/ONEOF forms [§ 2.4.5]. For example, in addition to the above REF rules, the abduces relation ⇝ includes the abduction rules:

(SUBR ϵ_{↓} (τ_{↑ 1} … τ_{↑ n}) τ_{↓}) ⊑ (SUBR ϵ_{↑} (τ_{↓ 1} … τ_{↓ n}) τ_{↑}) ⇝ ϵ_{↓} ⊑ ϵ_{↑} ⇝ τ_{↓ 1} ⊑ τ_{↑ 1}

⋮
⇝ τ_{↓ n} ⊑ τ_{↑ n}
⇝ τ_{↓} ⊑ τ_{↑}.

All tonicity axioms have this basic form.

5These axioms are excluded for now because they are axioms on set-like structures. Incorporating them into Implicit Projection is discussed below in Section 5.7.

Note that ⇝ also includes the anti-symmetry axiom (viz., δ ⊑ δ′ ∧ δ′ ⊑ δ ⟹ δ ≡ δ′). Thus, the ⇝ relation includes the following abduction axiom:

δ ≡ δ′ ⇝ δ ⊑ δ′
⇝ δ′ ⊑ δ

This axiom is important for performing abduction over description applications. Specifically, consider the following abductive transform of the description application axiom [§ 2.4.6]:

(δ_{ψ} δ_{1} … δ_{n}) ⊑ (δ′_{ψ} δ′_{1} … δ′_{n}) ⇝ δ_{ψ} ≡ δ′_{ψ}
⇝ δ_{1} ≡ δ′_{1}
⋮
⇝ δ_{n} ≡ δ′_{n}

This set of abduction inference rules therefore generates equivalence from inclusion. By admitting equivalence through anti-symmetry, tonicity equivalence abduction rules are in effect generated from the tonicity inclusion abduction rules. In so doing, equivalence constraints can be induced on matchvars (υ_{μj}) appearing within any of the application components.

For example, from this abduction, the following can be derived:

(ν_{μ 1} ν_{μ 2}) ⊑ (g BOOLE) ⇝ ν_{μ 1} ≡ g

                       ⇝ ν_{μ 2} ≡ BOOLE

Note, however, that the β-rule [§ 2.3.5] has intentionally not been incorporated into the ⇝ relation.^{6} For instance,

(f a) ⊑ (PAIROF BOOLE BOOLE @R) ⇝̸ f ≡ (Dλ ((τ TYPE)) (PAIROF τ τ @R))
                                  ⇝̸ a ≡ BOOLE

Thus, no attempt is made to perform higher order inclusion matching. Indeed, it has been shown that higher order unification is in general undecidable [Goldfarb 81] [Pfenning 88].

To summarize, then, the process of solving implied projections may induce numerous simultaneous inclusion constraints on the projection parameters, some bounding from above and some from below. To determine the satisfiability of these constraints one must determine the tightest upper and lower bound on each matchvar, then verify their consistency. The difficulty is in finding the tightest (max or min) of several independent inclusion constraints. To use the terminology developed in this section, this is the problem of abductively inferring the most general consistent resolution context for the match constraints imposed by an implicit projection, using the abduction relation ⇝.

Finally, the ⇝ relation also incorporates inclusion over recursive types. Recall [§ 2.4.7] that we left recursive type inclusion unaxiomatized, just as we left recursive type equivalence unaxiomatized [§ 2.3.6]. This situation does not admit considering DLETREC abduction rules since there are no DLETREC axioms from which to take the abductive transform. For that reason, we now present the DLETREC fixpoint equivalence axiom and the DLETREC fixpoint induction axioms. As in Section 4.2, without loss of generality, we choose to use the more convenient shorthand (RECTYPE t τ) for (DLETREC ((t τ)) t).^{7} In the following, R denotes a set of inclusion constraints on RECTYPE formals.

6If only fully normalized descriptions are inclusion matched, then the αη-rules are immaterial.

                     (RECTYPE t τ) ≡ τ[(RECTYPE t τ)/t]

R ∪ {t ⊑ τ_{↑}} ⊢_{⊑} τ_{↓} ⊑ τ_{↑}

                             R ⊢_{⊑} (RECTYPE t τ_{↓}) ⊑ τ_{↑}

R ∪ {τ_{↓} ⊑ t} ⊢_{⊑} τ_{↓} ⊑ τ_{↑}

                             R ⊢_{⊑} τ_{↓} ⊑ (RECTYPE t τ_{↑})

We are now prepared to extend ⇝ with the following abduction rules over rectypes:

              (RECTYPE t τ_{↓}) ⊑ τ_{↑} ⇝ τ_{↓}[(RECTYPE t τ_{↓})/t] ⊑ τ_{↑}
              τ_{↓} ⊑ (RECTYPE t τ_{↑}) ⇝ τ_{↓} ⊑ τ_{↑}[(RECTYPE t τ_{↑})/t]

For example:

                  (REF VOID) ⊑ (RECTYPE t_{↑} (REF t_{↑}))

⇝

                  (REF VOID) ⊑ (REF (RECTYPE t_{↑} (REF t_{↑})))

The termination of the resolution process over these recursive type expressions will be addressed in Section 5.6.

7Again, the general DLETREC-to-RECTYPE linear transformation algorithm will be presented in a forthcoming technical report.

5.5 Context Resolution via Abduction over Inclusion

Abduction over inclusion does not, in general, yield a set of constraints against the matchvars that can properly be called a resolution context. This is because many upper and lower constraints may be abduced for each matchvar, whereas a resolution context proper has precisely one upper and one lower constraint for each matchvar.

Thus, the set of constraints abduced via abductive inclusion we call A(M) where, as usual, M denotes the set of match constraints imposed on the matchvars ν_{μi} by the implicit projection. To reduce A(M) to a resolution context, we coin the following notation:

• Let A(M) denote the set of constraints abduced from M via abductive inclusion, i.e., A(M) = {ψ | M ⇝ ψ}.

• Let L(ν_{μi}, M) denote the set of closed lower bounds δ_{↓} on matchvar ν_{μi} within the abduced constraints A(M), i.e., {δ_{↓} | M ⇝ δ_{↓} ⊑ ν_{μi} where δ_{↓} closed}.

• Let U(ν_{μi}, M) denote the set of closed upper bounds δ_{↑} on matchvar ν_{μi} within the abduced constraints A(M), i.e., {δ_{↑} | M ⇝ ν_{μi} ⊑ δ_{↑} where δ_{↑} closed}.

• Let B(M) denote the set of closed bounding constraints ψ on matchvars abduced from M, i.e., {ψ | M ⇝ ψ where ψ = ν_{μi} ⊑ δ_{↑} or ψ = δ_{↓} ⊑ ν_{μi} where δ_{↓} and δ_{↑} closed}.

• Let T (M) denote the set of constraints within the abduced constraints A(M) which are not bounding constraints and for which no abduction rule applies, i.e., T (M) = A(M) − B(M) − {ψ | M ⇝ ψ and ∃ψ′ ≠ ψ . ψ ⇝ ψ′}. These are called the terminal constraints of M.

Examples of terminal constraints abduced from a set of match constraints include provable constraints (e.g., INT ⊑ INT and VOID ⊑ (REF INT)), inconsistent constraints (e.g., INT ⊑ BOOLE and (REF INT) ⊑ (LISTOF INT)), unprovable constraints (e.g., τ ⊑ INT for POLY-bound description variable τ), and structurally “stuck” constraints from which abduction cannot proceed (e.g., (REF ν_{μi}) ⊑ (LISTOF INT)). As we shall see, only provable terminal constraints will be abduced from a successful match.

Now recall [§ 0.4.4] that a maximum of a set of descriptions is defined to be a description δ within the set such that for all other descriptions δ′ within the set, δ′ ⊑ δ. A maximum is a least upper bound (lub) that is also a member of the set. A maximum does not always exist for arbitrary sets of descriptions, but when it does exist it is unique modulo equivalence. A minimum is similarly defined as a greatest lower bound (glb) of a set of descriptions that is also a member of the set. A minimum does not always exist for arbitrary sets of descriptions, but note that it does exist for any set containing a bottom element, viz., a set of types containing VOID or a set of effects containing PURE. The minimum, when it exists, is unique modulo equivalence. By convention, we define the maximum of an empty set of elements of kind κ to be ⊥_{κ} (since any element which might be introduced would be higher than it); similarly, the minimum is ⊤_{κ}.

We now define reduction of a set of match constraints M into a resolution context C:

Definition 5.5.1 M is consistent iff every terminal constraint abduced from M can be proved from the inclusion axioms, and L(ν_{μi}, M) and U(ν_{μi}, M) coalesce for all matchvars— i.e., {} ⊢_{⊑} T (M) and for all matchvars ν_{μi} in M, if δ_{↓} ∈ L(ν_{μi}, M) and δ_{↑} ∈ U(ν_{μi}, M) then {} ⊢_{⊑} δ_{↓} ⊑ δ_{↑}.

Definition 5.5.2 M is convergent iff for all matchvars ν_{μi} occurring in M, there exist both MAX(L(ν_{μi}, M)) and MIN(U(ν_{μi}, M)).

Definition 5.5.3 M is unambiguous iff it is convergent and, moreover, for each matchvar ν_{μi} in M, MAX(L(ν_{μi}, M)) ≡ MIN(U(ν_{μi}, M)).

Definition 5.5.4 If M is convergent, then Reduce(M) is defined to be the resolution context consisting of the 2i constraints MAX(L(ν_{μi}, M)) ⊑ ν_{μi} and ν_{μi} ⊑ MIN(U(ν_{μi}, M)) for matchvars ν_{μi} in M.

Lemma 5.5.1 If M is convergent, then M ⇝ Reduce(M)

Proof: By the definitions of MAX/MIN, U(ν_{μi}, M), and L(ν_{μi}, M).

Corollary 5.5.1 If Reduce(M) is a solution to M, then it is in fact the most general solution [Definition 5.2.3].

Proof: By uniqueness of MAX/MIN and by abductive soundness of ⇝ in Lemma 5.5.1.

The domain of match constraints over which Reduce is defined can be expanded by relaxing the above definitions to compute the general lub/glb rather than the more confining MAX/MIN. This is more general than computing the MAX/MIN of a set of descriptions since the lub/glb of a set is not restricted to be an element of the set. The abduces relation would therefore have to be extended to maintain the truth of the above Lemma. With that, however, the remainder of the results derived here extend without difficulty. This strictly increases the number of cases for which implicit projection through context resolution via abductive inference succeeds. For instance, it would improve the instances of successful implicit projection in the instances of object-oriented programming styles (OOPS) involving multiple inheritance.^{8} Unfortunately, lub/glb can be more expensive to compute than MAX/MIN: MAX/MIN can be computed by mere ⊑ testing over the set elements whereas the more flexible lub/glb in general requires a procedure to compute lub/glb per se. Should this more general lub/glb prove substantially more expensive to implement than MAX/MIN, an implementation might first attempt MAX/MIN, resorting to the more general lub/glb only when that fails. That is to say, algorithmic complexity slicing might well be applicable in relaxing the context resolution algorithm without detriment to its running time. We have heretofore restricted ourselves to MAX/MIN in accordance with the FX-87 language specification [Gifford et al. 87, p.45,85].

8For example, consider the situation where the abduction has produced the simultaneous constraints ν_{μi} ⊑ (RECORDOF (age INT)(friends INT) @=) and ν_{μi} ⊑ (RECORDOF (age INT)(specialty SYMBOL) @=)

for which no MIN exists, but the glb is (RECORDOF (age INT)(friends INT)(specialty SYMBOL) @=).

Lemma 5.5.2 If M is consistent and convergent, then Reduce(M) is a solution [Definition 5.2.2] to the matching problem M.

The restriction that M be consistent is crucial for soundness since, for example, an abduction producing the constraint:

(SUBR ((ONEOF (i INT) (b BOOLE))) VOID) ⊑ (SUBR ((ONEOF (b BOOLE))) INT)

could succeed, whereas an abduction producing either of the two constraints:

      INT ⊑ BOOLE
(REF ν_{μ i} ) ⊑ (ONEOF (i INT) (r (REF INT)))

would fail. Any match problem M leading to the former situation might have a solution depending on the other abduced constraints, but a match problem leading to the latter situation has no solution, even if M is convergent.

The next section addresses how to implement this reduction with an efficient algorithm. The two subsequent sections address how to expand the range of match problems for which we can compute a solution by further extending ⇝ to encompass the set inclusion axioms.

5.6 Implementing Context Resolution

One method for deciding if M is consistent and convergent and for computing Reduce(M) is to simply enumerate A(M), the constraints abducible from M, then determine consistency, convergence, and Reduce from the definitions in the previous section. Since A(M) is finite for finite M (proof: by induction over the abduction axioms), this process must terminate.

A more perspicacious alternative is to implement the context resolution process as a modest extension to the description inclusion algorithm [§ 4.2] as detailed below. The strat-

TO COMPUTE Reduce( M) DO
   INITIALIZE U-env SUCH THAT U-env(ν_{μ i}) = {}
               L-env SUCH THAT L-env(ν_{μ i}) = {}
        WHERE U-env maps MATCHVARs in M to their upper bounds sets {δ_{↑}. . .}
               L-env       "                       lower bounds sets {δ_{↓}. . .}
   FOR EACH CONSTRAINT τ_{↓} ⊑ τ_{↑} IN M DO
       UPDATE U-env AND L-env BY PERFORMING Abduces(τ_{↓} ⊑ τ_{↑})
   IF Abduces FAILS ON ANY CONSTRAINT IN M
   THEN FAIL "Inconsistent terminal constraint"
   ELSE COLLAPSE U-env AND L-env BY PERFORMING Resolve( U-env, L-env)
        RETURN  ;; A Resolution Context Solution
              {τ ⊑ τ′ | either <τ,{τ′}> ∈ U-env  or  <τ′,{τ}> ∈ L-env}

Figure 5-1: Context Resolution Algorithm

egy is to run a modestly extended inclusion testing algorithm (viz., Abduce) on each match constraint of M, noticing when an inclusion test ultimately matches a description against

TO PERFORM Abduces(τ_{↓} ⊑ τ_{↑}) WRT U-env AND L-env DO
         Abduce (τ_{↓} ⊑ τ_{↑}) WRT EMPTY μ-env_{↓} assumed-⊑ μ-env_{↑} assumed-⊒
                         UPDATING U-env AND L-env
TO PERFORM Abduce(τ_{↓} ⊑ τ_{↑}) WRT μ-env_{↓} assumed-⊑ μ-env_{↑} assumed-⊒
 WHERE μ-env_{↓} maps RECTYPE formals in τ_{↓} to their RECTYPE bindings
       μ-env_{↑}  "  τ_{↑}  "
   assumed-⊑ is a set of formulæ: RECTYPE formal μ_{↓} ⊑ δ_{↑}
   assumed-⊒  "     RECTYPE formal μ_{↑} ⊒ δ_{↓}
DO
[τ_{⊥}]. IF τ_{↓} ≡ VOID THEN RETURN
[τ_{∅}].  IF τ_{↓} ≡ NULL AND τ_{↑} = (PAIROF τ τ′) THEN RETURN
[τ _{base}]. IF τ_{↓} ≡ τ_{↑} THEN RETURN
[REF]. IF τ_{↓} = (REF τ′_{↓}) AND τ_{↑} = (REF τ′_{↑})
       THEN Abduce(τ′_{↓} ⊑ τ′_{↑}) WRT μ-env_{↓} assumed-⊑ μ-env_{↑} assumed-⊒
  ⋮  Similarly for PAIROF, RECORDOF, ONEOF, SUBR, and POLY as per
  ⋮    the abductive transforms of the "tonicity" inclusion axioms
[RECTYPE_{↓}]. IF τ_{↓} = (RECTYPE μ_{↓} τ_{μ↓})

THEN Abduce(τ_{μ↓} ⊑ τ_{↑}) WRT μ-env_{↓}[μ_{↓} ↦ τ_{μ↓}] assumed-⊑ ∪ {μ_{↓} ⊑ τ_{↑}}^{‡}

                                     μ-env_{↑}  assumed-⊒

[RECTYPE_{↑}]. IF τ_{↑} = (RECTYPE μ_{↑} τ_{μ↑}) THEN <dual case to [RECTYPE_{↓}]>
[μ_{↓}]. IF τ_{↓} IS A RECTYPE FORMAL μ_{↓}
      THEN IF μ_{↓} ⊑ τ_{↑} ∈ assumed-⊑ THEN RETURN

           ELSE Abduce(μ-env_{↓}(μ_{↓}) ⊑ τ_{↑}) WRT μ-env_{↓} assumed-⊑
                                           μ-env_{↑} assumed-⊒

[μ_{↑}]. IF τ_{↑} IS A RECTYPE FORMAL μ_{↑} THEN <dual case to [μ_{↓}]>
[ν_{μ↓}]. IF τ_{↓} IS A MATCHVAR ν_{μ↓}
       THEN UPDATE <ν_{μ↓},{δ_{↑}. . .}> IN U-env TO <ν_{μ↓},{δ_{↑}. . . τ_{↑}}>
            RETURN    ;; will verify convergence after Abduces
[ν_{μ↑}]. IF τ_{↑} IS A MATCHVAR ν_{μ↑} THEN <dual case to [ν_{μ↓}]>
OTHERWISE FAIL "Inconsistent terminal constraint"
‡Or just assumed-⊑ if τ_{↑} contains no free RECTYPE formals

Figure 5-2: Abduces Subroutine Algorithm

TO COMPUTE Resolve( U-env, L-env)
     WHERE U-env maps MATCHVARs in M to their upper bounds sets {δ_{↑}. . .}
            L-env       "                       lower bounds sets {δ_{↓}. . .}
DO
   FOR EACH ν_{μ i} IN M DO

UPDATE <ν_{μ i},{δ_{↑}…}> IN U-env TO <ν_{μ i}, MIN({δ_{↑}…})> UPDATE <ν_{μ i},{δ_{↓}…}> IN L-env TO <ν_{μ i}, MAX({δ_{↓}…})>

       IF MIN OR MAX FAILS TO EXIST
       THEN FAIL "Non-convergent match problem M"
       IF {} ⊬_{⊑} MIN ⊑ MAX
       THEN FAIL "Inconsistent match problem M"

Figure 5-3: Resolve Subroutine Algorithm

a matchvar, accumulating these match inclusion tests into either L(ν_{μi}, M) or U(ν_{μi}, M) as appropriate. We prepare for this by associating with each matchvar an initial binding in an L-env and U-env. These environments map each matchvar to its accumulated set of constraints L(ν_{μi}, M) and U(ν_{μi}, M), respectively. Each initial binding is totally unconstrained other than being of a fixed KIND, as declared when the matchvar was introduced. (For brevity, this kind constraint is not shown in the Reduce algorithm.) To model these initial bindings, we introduce ⊥_{κ} and ⊤_{κ} to denote respectively the top and bottom of the fragments of the description partial ordering of KIND κ.^{9}

Specifically, we maintain two sets (initially containing the bottom/top of the appropriately kinded description partial order) for each matchvar, one for currently encountered upper bounds, one for lower bounds. Inclusion matching then proceeds by gradually raising the lower bound set on a matchvar with each successive monotonic inclusion match (ν_{μi} ⊑ δ_{↑}), similarly lowering the upper bound set with each anti-monotonic inclusion match (δ_{↓} ⊑ ν_{μi}). This implements an incremental constraining of each matchvar ν_{μi}, where the number of inclusion tests is linear in the number of match constraints in M.^{10}

Abduction is simulated by performing an inclusion-directed recursive descent of the match constraints in M. Upon each newly abduced upper bound constraint on a matchvar we could compare the current set of upper bounds of the matchvar against the new bound, either keeping the old bounds if they already subsume the new bound or updating the current bounds to include the new bound then deleting any old bounds which this new bound subsumes. Newly abduced lower bounds can be treated similarly. Given this, U-env and L-env would map each matchvar to an irredundant set of current upper/lower bounds. This detail is not shown in the algorithm of Figure 5-1. Moreover, when a new upper bound is added to the current upper bounds set, we could check that the new bound is above each element of the current lower bounds set. Similarly, newly added lower bounds could be checked for consistency with the current upper bounds set. This too is not shown in the algorithm of Figure 5-1.

9Actually, with this extension, each distinctly kinded fragment of the description partial order now properly comprises a pointed complete partial order (pcpo), but this extension is not visible outside the implementation. Specifically, to the FX-87 programmer, descriptions still comprise just a partial order, incomplete and unpointed.

10This raising/lowering of running bounds was inspired by the version spaces technique [Mitchell 81] for learning a pattern from successive positive and negative instances of the intended pattern. A similar technique was presented in [Fuh & Mishra 88], but its soundness was left open and a certain anomaly in its use was noted. The basis of this anomaly has been explained by [Wand & O’Keefe 89]. I avoid this problem by inclusion matching only over fully normalized descriptions, thus obviating any subtleties introduced by the equivalence axioms. By fortunate happenstance, this constraint is presupposed in FIX since the inclusion test itself is invoked only on fully normalized descriptions. Similarly generalizing the equivalence testing algorithm to attempt non-inclusive context resolution should be relatively straightforward since failure at the equivalence stage would ultimately result in more general inclusion-based resolution anyway.

Assuming irredundant sets are maintained, upon processing all match instances in M the resulting upper and lower bounds sets should be singleton sets for each matchvar. Any non-singleton set would indicate the non-existence of a MAX/MIN for that set of bounds, implying that the resolution is non-convergent [Definition 5.5.2]. Moreover, each upper bound inferred for a matchvar should be above (⊑) each lower bound inferred for that matchvar, otherwise the resolution is inconsistent [Definition 5.5.1]. Notice that consistency can be checked either upon each successive incorporation of a newly abduced constraint (as already suggested) or, instead, consistency can be checked only against the final MAX/MIN of each matchvar after all abduction has completed (as shown in the Resolve algorithm [Figure 5-3]). Soundness is maintained in either case since upper/lower bounds are strictly lowered/raised, but postponing the test until after completion can involve fewer comparisons. Similarly, rather than maintain irredundant sets of bounds as suggested, this convergence testing can be postponed until after abduction has completed (as shown in Resolve). No particular performance advantage is gleaned from postponing convergence testing but postponing it allows us to separate convergence concerns from the abduction algorithm.

Upon complete processing of the match instances, if the match is consistent and convergent but their exists some matchvar for which the computed MAX lower bound and MIN upper bound are not equivalent, then there is flexibility in the choice of projection for that matchvar since no constraint will be violated by any choice of projection within the abduced bounds. Of course, subsequent use of whatever choice is made may cause resolution failures outside the scope of the current implicit projection, but such difficulties reflect an ambiguity in the programmer-intended projection anyway. In such cases, the context resolution process can proceed with a capricious choice of projection,^{11} but a warning should be issued to the programmer to announce this perchance unintended ambiguity. This reflects the case where no single choice of projection arguments is forced in the implicit projection, but a range of feasible choices of projection arguments does exist— that is, M is ambiguous [Definition 5.5.3]. It therefore could be said that the implied projection itself is ambiguous.

Finally, should any step in the inclusion-based abduction simulation fail, then that inclusion test identifies a terminal constraint which cannot be proved from the inclusion axioms. That is, it indicates a constraint for which no abduction rule applies (else the inclusion-based simulation would not have failed) and for which satisfiability cannot be proved from the inclusion axioms (else the simulation would have returned TRUE, possibly after extending L-env and/or U-env). Such a situation indicates a failed resolution.

11Well, within the bounds of observing the Region Anti-Aliasing Rule. This issue will be more apparent after we have clarified the semantics of REGION and EFFECT descriptions [Chapter 6]. It will be discussed in detail in a forthcoming technical report.

Termination of this algorithm follows from the termination of the RECTYPE Inclusion Algorithm [Figure 4-1] since the generalization of the RECTYPE inclusion decision algorithm into Abduces [Figure 5-2] introduces no new opportunities for divergence— that is, the termination argument in Section 4.4 carries through immediately. The termination of Resolve is clear by inspection. Similarly, correctness should be clear by inspection that the resolution context produced by Reduce, when fed as initial assumed-⊑/assumed-⊒ to the RECTYPE inclusion algorithm, is indeed a solution of M since, by nature of the inclusionbased abduction simulation, C ⊢_{⊑} M. Moreover, it is likewise immediate that the simulated abduction satisfies the abductive soundness condition [Definition 5.3.2] since ⊢_{⊑} was used directly in computing the abduced constraints A(M) from which the resolution context C was computed, so these abduced constraints must follow from the solution C. To summarize formally, C ⊢_{⊑} M and C ⊢_{⊑} A(M), where A(M) = {ψ | M ⇝ ψ}. This is precisely the abductive soundness condition.

This strategy works fine for non-set-structured descriptions. For set-structured patterns, the task becomes appreciably more involved. How to generalize it accordingly is the topic of the next section.

5.7 Abduction over Set Inclusion

Recall that region RUNIONs, effect MAXEFFs, and RECORDOF/ONEOF fieldname/type pairs all constitute sets. Our implicit projection context resolution therefore should handle inclusion over set-like structures. This section addresses how the Abduction over Inclusion must be extended to accommodate these sets.

For example, consider the following matching problem over two RUNIONs, where for now lower case letters denote matchvars.

(RUNION @A  x  y) ⊑ (RUNION @A @B @C)                                 [0]
(RUNION @A @B @C) ⊑ (RUNION @A  y  z @D)                              [1]

Now consider the abductive transform of the tonicity axiom for RUNION [§ 2.4.3]. If incorporated into the abduces relation ⇝, this would abduce from match constraint [0] that x ⊑ @B and y ⊑ @C, but it would fail to abduce anything from constraint [1] since the two RUNIONs do not have the same number of elements. Neither result is desirable since even the abduction from the first case is not abductively sound [Definition 5.3.2] so it does not yield the most general solution.

To avoid this difficulty, we were careful to exclude from the abduction relation ⇝ the abductive transforms of the tonicity axioms for pure set forms (viz., RUNION and MAXEFF)^{12}. We now derive a set of more sophisticated abduction rules for RUNION in the remainder of this section. The derivation for MAXEFF rules is analogous.

First, recall [§ 2.3.2] that RUNION denotes a set union over region descriptions. Thus, constraint [0] induces an upper bound on x and y, namely:

x ⊑ (RUNION @A @B @C)
y ⊑ (RUNION @A @B @C)

Constraint [1] is less confining. Specifically, y and z can range as low as they like so long as they are collectively responsible for covering @B and @C. Notice that, in constraint [1], the occurrences of @A on both sides of the inequation cancel and that all other literals on the righthand side of the inequation (in this case, @D) impose no constraints on y or z, and hence may also be dropped. That is:

@B ⊑ (RUNION y z)
@C ⊑ (RUNION y z)

Consider what this means in terms of an incrementally maintained resolution context. Initially, x, y, and z are unconstrained. After constraint [0], we have precisely the two simple upper bound constraints expressed earlier. The problem is how to express, within the resolution context, the new lower bound constraints resulting from constraint [1]. Two obvious choices present themselves, with increasing degrees of flexibility and complexity.

First, we could take a conservative stance and constrain both y and z to cover the set containing @B and @C. This could be justified on the basis that if this conservativism results in a subsequent failure in the context resolution, then the programmer should have made the intended projection explicit. Of course, such a system will clearly fail in cases where a less conservative approach would succeed. Thus, this approach does not always find the most general solution (mgs) [Definition 5.2.3] of the simultaneous constraints when such an mgs exists, however, if it claims to find a solution, then it indeed does. In short, this conservative stance is not abductively sound, but it is nonetheless safe.

12The tonicity axiom for RECORDOF and ONEOF forms is non-problematic since there is no flattening of fieldname/type pairs in FX-87.

To relax this conservatism, we extend the ⇝ relation with the following abductively sound set-inclusion abduction rules:

(RUNION ρ_{1} … ρ_{n}) ⊑ ρ′ ⇝ ρ_{1} ⊑ ρ′
⋮
⇝ ρ_{n} ⊑ ρ′
ρ ⊑ (RUNION ρ′) ⇝ ρ ⊑ ρ′

Intuitively, the first one reduces RUNION/RUNION comparisons to base-REGION/RUNION comparisons. The second notes that unitary RUNIONs are equivalent to their single components. These flattening axioms could easily have been incorporated into ⇝ earlier without incident. By contrast, the following two cancellation abduction rules would have been more problematic, as we shall see.

78 CHAPTER 5. IMPLICIT PROJECTION VIA ABDUCTIVE INFERENCE

In the following two cancellation abduction rules, R denotes region descriptions containing no matchvars (so-called “μ-closed” regions):^{13}

R ⊑ (RUNION R′ ρ_{1} … ρ_{n}) ⇝ R ⊑ (RUNION ρ_{1} … ρ_{n}) for R ≢ R′

R_{i} ⊑ (RUNION ν_{μ1} … ν_{μm})
ν_{μj} ⊑ (RUNION R_{1} … R_{n}) for 1 ≤ j ≤ m and R_{i} ∉ {R_{1} … R_{n}}
R_{i} ⊑ (RUNION ν_{μ1} … ν_{μj−1} ν_{μj+1} … ν_{μm})

The first permits cancellation of non-constraining μ-closed region descriptions. The second and most powerful new abduction rule provides cancellation of matchvars according to the observation that if a set of matchvars of kind REGION is responsible for covering some region constant R_{i} but it is known that one of the matchvars ν_{μj} cannot contain R_{i}, then the other matchvars are responsible for covering it.

Notice that this formulation of the matchvar cancellation axiom disregards non-β-reducible description applications which contain matchvars, either in the operator or in an operand. Indeed, the FX-87 manual forbids polymorphizing over description functions whose eventual return description is not of kind TYPE [Gifford et al. 87, p.39], which obviates occurrences of matchvar operators. This is not unreasonable since, regions and effects being sets, any description function whose eventual return kind is REGION or EFFECT can merely perform a union, for which the predefined description operators RUNION and MAXEFF could have been used. It, however, does not forbid Dλ abstraction over higher order descriptions whose return kind is not TYPE, so we can still encounter matchvars in operands

13These are derived from the more general set inclusion cancellation axiom:

S_{1} ⊑ S_{2}
S_{3} ⊑ S_{4} where S_{4} is variable free
S_{1} − S_{4} ⊑ S_{2} − S_{3}

Consider those elements that are in S_{1} but not in S_{4}. These can be covered only by those elements of S_{2} which are not otherwise disqualified by being elements of S_{3}.

Specializing this more general axiom to the matchvar cancellation axiom requires only a couple of observations. First, each match constraint admits matchvars on only one side of an inequation. Thus, we can assume S_{1} to be variable free, that is, S_{1} contains only μ-closed descriptions. That being the case, we can always reduce S_{1} ⊑ S_{2} to a set of constraints {s_{1i}} ⊑ S_{2}. Now, recall from the discussion at the beginning of this chapter that we can likewise reduce S_{3} ⊑ S_{4} to the set of constraints {s_{3i}} ⊑ S_{4} since each matchvar on the lefthand side of an inequation must be covered by the righthand side. Note that a set containing a single matchvar is equivalent to that matchvar and that an RUNION over a single region literal is equivalent to that region literal, so we have successfully reduced to the premises of the matchvar cancellation axiom (except that S_{2} is not yet constrained to be a set of matchvars). Now to reduce the conclusion, notice that R_{i} ∉ {R_{1} … R_{n}}. In the notation of our reduced more general axioms, this is the restriction that {s_{1i}} ∉ S_{4}. Thus, the conclusion that S_{1} −S_{4} ⊑ S_{2} −S_{3} reduces to {s_{1i}} ⊑ S_{2} −{s_{3i}}, which is precisely the conclusion in the matchvar cancellation axiom.

Two lemmas to this general set cancellation axiom are directly verifiable: 1) constants appearing in both S_{1} and S_{2} can be canceled, and 2) constants appearing in S_{2} but not in S_{1} may be canceled. The abductive transform of this second lemma over RUNIONs is precisely the abduction rule in the text for cancellation of non-constraining μ-closed region descriptions. This allows us to reduce S_{2} to be just a set of matchvars as in the premise to the matchvar cancellation abduction rule, concluding the reduction of the more general axiom to the two cancellation axioms in the text.

(and hence in operators which are themselves description applications containing matchvar operands). Thus, the manual does not really uniformly assist in this difficulty. Fortunately, the restriction that bounds on matchvars be closed, coupled with the description application abduction axiom, can be used to obviate the entire issue since non-reducible description applications must have an effective operator which is either a POLY-formal or a Dλ-formal. In short, the manual’s syntactic restriction on higher order POLY-formals is unnecessary.

For instance, our disregard for flexible constraints containing a mixture of matchvars and μ-open description applications is justified since such match instances must fail. Unfortunately, failure on more sophisticated instances are not so easily justified. For instance, consider the following match constraint for which DF is a Dλ-bound formal: (DF @A) ⊑ (RUNION (DF x) (DF y)). By the description application abduction rule, this should be equivalent to @A ≡ (RUNION x y). Unfortunately, the abduction axioms presented above do not handle such situations, although at no loss of abductive soundness: they merely fail to produce a solution. This is of no consequence since we perform context resolution only on fully normalized descriptions, thus description normalization can include the canonicalization of such forms by the reduction schema:

 (RUNION (DF ρ_{1} . . . ρ_{n}) (DF ρ′_{1} . . . ρ′_{n})) ⟹ (DF (RUNION ρ_{1} ρ′_{1}). . . (RUNION ρ_{n} ρ′_{n}))

Similarly for distributing MAXEFF over coalescent description application arguments of kind EFFECT. Here, however, corresponding arguments of kind REGION are implicitly RUNIONd.

This introduces a set of exotic new homomorphism equivalence axioms regarding distribution of RUNION/MAXEFF over description applications, axioms which were justifiably omitted from the FX-87 manual. Depending on the FX-87 programmer’s style, they may prove inconsequential in practice. They are presented here nonetheless to more precisely characterize the domain of solvable match problems. Furthermore, they should prove invaluable to formulating a precise semantic model of regions and effects, an arduous task which has heretofore not been tackled.

The sole remaining question regarding this set extension to the context resolution process is how to incorporate this axiom into the algorithm without loss of efficiency. This is the topic of the next section. In short, a bookkeeping strategy called flexibility indexing is developed to allow this new axiom to be incorporated into the context resolution process while maintaining its present time bound of requiring a number of inclusion tests linear in the number matchvar instances within the match constraints M.

5.8 Context Resolution via Abduction over Set Inclusion

The context resolution sub-algorithm Abduces [Figure 5-2] is conservative regarding abduction over sets. The goal of this section is to now relax the context resolution algorithm by incorporating the set-inclusion axioms of the previous section into the algorithm. As noted before, this extension preserves abductive soundness.

Algorithmically, there are two natural ways to extend the context resolution algorithm to incorporate the set inclusion abduction axioms. The first involves altering the control structure of the algorithm to perform backtracking. Specifically, one might alter the algorithm to attempt an initially conservative abduction that, upon subsequently failing, could backtrack to the point within the resolution process where the failing abduction was induced then try a less constraining alternative. With this control structure, one might interpret a constraint such as

@B ⊑ (RUNION y z)

from the previous section to be equivalent to

[@B ⊑ y  AND  @B ⊑ z]  OR  [@B ⊑ y]  OR  [@B ⊑ z] ,

where each disjunct indicates an implied potential backtrack point. Such an approach would ultimately result in a successful choice or in detection that all alternatives have been exhausted so no consistent resolution is possible. Of course, such a backtracking strategy would also result in a dismally inefficient context resolution algorithm.^{14} Also, the specific order in which choices are attempted would have to respect a monotonically increasing retreat from the most general solution. This is potentially precarious to implement correctly.

Fortunately, there is a way to achieve the same effect with no loss of efficiency. The solution is, rather than altering the control structure of the algorithm, to generalize the bookkeeping data structures of the algorithm to maintain information about what matchvars are responsible for covering each region literal. This generalization I call flexibility indexing since the number of matchvars presently responsible for a given region literal indexes the degree of flexibility in potentially satisfying the present resolution constraints.

Specifically, what is needed is a way to maintain within the resolution process the fact that there may be some flexibility in the way certain lower bounds are satisfied. Recall, for instance, that it is desirable to express constraints such as:

@B ⊑ (RUNION y z)
@C ⊑ (RUNION y z)

Such constraints are not directly expressible in the L-env if we are limited to binding matchvars to their running lower-bounding descriptions. What is needed is generalization of the lower-bounding descriptions to express the flexibility in the righthand side RUNION in the above inequality.

14Specifically, trying all possibilities of m matchvars covering p pattern constants would require, for each of the m matchvars, a possible number of matches proportional to the powerset of a set of p elements. This is O(2^{mp}) , which is clearly intolerable.

We need a way to acknowledge that y and z are collectively responsible for covering the elements of the bounding set, but that neither is wholly responsible for the entire set. The insight is to maintain, within the resolution process, the information that @B and @C may separately be covered by one of y or z. Should a later constraint, say, disqualify y from covering @B, then z must assume sole responsibility for covering it. If z is itself eventually disqualified then the resolution is unsatisfiable. If not, and the resolution completes, then any element which may still be potentially covered by a number of matchvars can be capriciously assigned to any one of them, again with the caveat that such a situation reflects an ambiguity which should be brought to the attention of the programmer.^{15} Perhaps, in such a situation, a conservative assignment is appropriate, namely assigning the element to all potential candidates. Again, the soundness of such an approach is incrementally maintained in any case.

Formally, we generalize our context resolution strategy by first incorporating into ⇝ the two new flattening axioms and the two new cancellation axioms. That done, we coin the following new notation for flexible lower bounds on matchvars:

• Let B_{F}(M) denote the set of closed flexible lower-bound constraints abducible from M i) for which no abduction axioms apply and ii) which are not subsumed by any inflexible lower-bound constraints abducible from M, i.e., {ψ | M ⇝ ψ where ψ = δ_{F} ⊑ (RUNION ν_{μ1}...ν_{μn}) and δ_{F} closed, but

i) there exists no {ν_{μi}...ν_{μj}} ⊂ {ν_{μ1}...ν_{μn}} such that M ⇝ δ_{F} ⊑ (RUNION ν_{μi}...ν_{μj}), and ii) B(M) ⊬_{⊑} ψ }.

• Let L_{F}(ν_{μi}, M) denote the set of closed flexible lower bounds on matchvar ν_{μi} within the flexible lower-bound constraints B_{F}(M), i.e., {δ_{F} | δ_{F} ⊑ (RUNION ν_{μ1}...ν_{μn}) ∈ B_{F}(M) where δ_{F} closed }.

We now define extended notions of consistency, convergence, and so on to take flexible constraints into account:

Definition 5.8.1 M is f-consistent iff every inflexible terminal constraint abduced from M can be proved from the inclusion axioms, and L(ν_{μi}, M) and U(ν_{μi}, M) coalesce for all matchvars— i.e., {} ⊢_{⊑} T (M) − B_{F}(M) and for all matchvars ν_{μi} in M, if δ_{↓} ∈ L(ν_{μi}, M) and δ_{↑} ∈ U(ν_{μi}, M) then {} ⊢_{⊑} δ_{↓} ⊑ δ_{↑}.

Lemma 5.8.1 If δ_{F} ∈ L_{F}(ν_{μi}, M) then δ_{F} ⊑ U(ν_{μi}, M).

Proof: By having incorporated the matchvar cancellation abduction axiom into ⇝ and by the definitions of L_{F}(ν_{μi}, M) and U(ν_{μi}, M).

15Again with the caveat that our choice must ultimately respect the Region Anti-Aliasing Rule.

Theorem 5.8.1 If δ_{F} ⊑ (RUNION ν_{μ1}...ν_{μn}) ∈ B_{F}(M) but there exists no ν_{μi} ∈ {ν_{μ1}...ν_{μn}} such that for all δ_{↑} ∈ U(ν_{μi}, M) {} ⊢_{⊑} δ_{F} ⊑ δ_{↑}, then M is not f-consistent.

Proof: By contradiction: Assume M to be f-consistent. Then, by definition, for all matchvars ν_{μi} in M, if δ_{↓} ∈ L(ν_{μi}, M) and δ_{↑} ∈ U(ν_{μi}, M) then {} ⊢_{⊑} δ_{↓} ⊑ δ_{↑}. Now, from the premises, repeated application of the matchvar cancellation abduction axiom of the previous section will eventually yield the abduction δ_{F} ⊑ (RUNION ν_{μj}). From this, the flattening abduction axiom of the previous section abduces that δ_{F} ⊑ ν_{μj}. Thus, δ_{F} ∈ L(ν_{μj}, M). This is a contradiction since, from the premises, it cannot be the case that for all δ_{↑} ∈ U(ν_{μj}, M) {} ⊢_{⊑} δ_{F} ⊑ δ_{↑}. Thus, M cannot be f-consistent.

Definition 5.8.2 M is f-unambiguous iff each flexible terminal lower-bound constraint abduced from M is subsumed by some inflexible lower-bound constraint— i.e., B_{F}(M) = {}.

Lemma 5.8.2 If M is unambiguous [Definition 5.5.3] then M is f-unambiguous, but not vice versa.

Definition 5.8.3 M is f-convergent iff it is both convergent and f-unambiguous— i.e., for all matchvars ν_{μi} in M, both MAX(L(ν_{μi}, M)) and MIN(U(ν_{μi}, M)) exist and, moreover, B_{F}(M) = {}.

Lemma 5.8.3 If M is f-consistent and unambiguous then M is f-convergent.

By substituting the terms f-convergent for convergent and f-consistent for consistent in the definition of Reduce [Definition 5.5.4] and the subsequent lemmas and corollary of Section 5.5, all proofs carry through. Namely:

Definition 5.8.4 If M is f-convergent, then f-Reduce(M) is defined to be the resolution context consisting of the 2i constraints MAX(L(ν_{μi}, M)) ⊑ ν_{μi} and ν_{μi} ⊑ MIN(U(ν_{μi}, M)).

Lemma 5.8.4 If M is f-convergent, then M ⇝ f-Reduce(M)

Proof: By the definitions of MAX/MIN, U(ν_{μi}, M), and L(ν_{μi}, M).

Corollary 5.8.1 If f-Reduce(M) is a solution to M, then it is in fact the most general solution [Definition 5.2.3].

Proof: By uniqueness of MAX/MIN and by abductive soundness of ⇝ in Lemma 5.8.4.

Lemma 5.8.5 If M is f-consistent and f-convergent, then f-Reduce(M) is a solution [Definition 5.2.2] to the matching problem M.

Unfortunately, f-Reduce(M) is undefined when any flexible constraint is actually irredundant, that is when B_{F}(M) ≠ {}. Such a situation signifies an ambiguity in how to resolve the flexible lower-bound among several matchvars. Such an M we defined to be f-ambiguous [Definition 5.8.2]. No most general solution exists for such a predicament; however, a number of solutions may exist. As alluded to in the prelude to this formalization [p. 81], it is desirable to return a conservative solution which assigns this flexible lower bound to each candidate matchvar. Such a solution might be called the most general conservative solution. We might formalize such a notion as follows:

Definition 5.8.5 If M is convergent, then FlexReduce(M) is defined to be the resolution context consisting of the i upper bounding constraints constraints ν_{μi} ⊑ MIN(U(ν_{μi}, M)) and the i lower bounding constraints:

FlexMAX(L(ν_{μi}, M) ∪ L_{F}(ν_{μi}, M) , MIN(U(ν_{μi}, M))) ⊑ ν_{μi}

where

FlexMAX(\{δ…\}, δ_{↑}) = \{ \begin{matrix}MAX(\{δ…\}) & if the MAX exists, \\ δ_{↑} & otherwise. \end{matrix}

Of course, FlexReduce(M) does not follow from abduction over M so no lemma comparable to Lemma 5.8.4 above applies. However, the following slightly weaker lemma is immediate:

Lemma 5.8.6 If M is f-convergent then FlexReduce(M) = f-Reduce(M).

Proof: By the definitions of FlexMAX, f-convergent, and L_{F}(ν_{μi}, M).

Corollary 5.8.2 If M is f-unambiguous then if FlexReduce(M) is a solution to M, then it is in fact the most general solution [Definition 5.2.3].

Proof: By Corollary 5.8.1 and the preceding lemma.

The corresponding relaxed version of Lemma 5.8.5 is immediate:

Lemma 5.8.7 If M is f-consistent and convergent, then FlexReduce(M) is a solution [Definition 5.2.2] to the matching problem M.

As earlier [p. 70], generalizing the above formalizations to incorporate lub/glb in place of MAX/MIN extends the domain over which solutions are computed by f-Reduce and FlexReduce without loss of lemma or corollary (or proof thereof).

5.9 Implementing Abduction over Set Inclusion

The question remains then how specifically to implement such an approach. The strategy used in FIX I call flexibility indexing.

First the Reduce algorithm is generalized by making it initialize an empty B_{F}, passing this on to Abduces for updating along with the already passed L-env and U-env. Then Abduces directly calls Abduce as before but now with this additional B_{F} argument. The generalization of Abduce is discussed below. The call to Resolve could be similarly generalized to take B_{F} as argument along with L-env and U-env, but it is more clear to simply introduce a new sub-algorithm to perform the FlexMAX. This generalization of Resolve is the topic of the next paragraph, following which the generalization of Abduce is discussed.

The generalization of the definition of Reduce to FlexReduce involves computing both MAX(L(ν_{μi}, M)) and MIN(U(ν_{μi}, M)) as before, but, as formally defined in FlexReduce, the MAX over the lower bounds must incorporate L_{F}(ν_{μi}, M) as well. Since MAX is associative, this may be implemented by first calling Resolve as before, afterward updating

TO COMPUTE FlexReduce( M) DO
   INITIALIZE U-env SUCH THAT U-env(ν_{μ i}) = {}
               L-env SUCH THAT L-env(ν_{μ i}) = {}

               B_{F}  SUCH THAT B_{F}  = {}

        WHERE U-env maps MATCHVARs in M to their upper bounds sets {δ_{↑}. . .}
               L-env       "                       lower bounds sets {δ_{↓}. . .}
               B_{F} is a list of flexible lower-bound constraints
   FOR EACH CONSTRAINT τ_{↓} ⊑ τ_{↑} IN M DO
       UPDATE U-env, L-env AND B_{F} BY PERFORMING Abduces(τ_{↓} ⊑ τ_{↑})
   IF Abduces FAILS ON ANY CONSTRAINT IN M
   THEN FAIL "Inconsistent terminal constraint"
   ELSE COLLAPSE U-env AND L-env BY PERFORMING Resolve( U-env, L-env)
        FOLD B_{F} INTO L-env BY PERFORMING FlexUpdate L( L-env, B_{F}, U-env)
        RETURN  ;; A Resolution Context Solution
              {τ ⊑ τ′ | either <τ,{τ′}> ∈ U-env  or  <τ′,{τ}> ∈ L-env}

Figure 5-4: Flexible Context Resolution Algorithm

the MAX bound in L(ν_{μi}, M) computed by Resolve according to the FlexMAX over the flexible bounding constraints in B_{F}, incorporating each bound according to FlexMAX before generating a resolution context solution to return from FlexReduce. This update procedure is illustrated by the FlexUpdateL algorithm below [Figure 5-5]. Notice, however, that this algorithm implements more than just an update to L: it also both discovers L_{F}(ν_{μi}, M) from B_{F}(M) and it implements the matchvar cancellation abduction axiom.

The generalization of Abduce to accumulate B_{F}(M) involves adding to the Abduce algorithm [Figure 5-2] new condition cases for handling constraints of the form δ_{↓} ⊑ δ_{↑} where either δ_{↓} or δ_{↑} is of the form (RUNION ρ_{1} … ρ_{n}). Notice already the generalization of τ_{↓} and τ_{↑} in the original Abduce algorithm to δ_{↓} and δ_{↑} since we now perform abduction over regions as well as over types. All old condition cases merely pass B_{F} along unmolested. We incorporate into Abduce the flattening abduction axioms over RUNIONs and the region literal cancellation abduction axiom by adding the new condition clauses of Figure 5-6.

Before returning to the question of how flexibility indexing can be incorporated into the more general context resolution procedure of FIX (recall that we must consider MAXEFF and RECORDOF/ONEOF axioms in addition to the RUNION axiom already considered), we should consider a nagging correctness condition regarding locally bound description parameters occurring within match instances. This is what motivated the closedness stipulation mentioned in the definition of resolution contexts [Definition 5.2.1].^{16} It is the topic of the next section, after which we consider specifically how FIX incorporates flexibility indexing into the implicit projection context resolution.

16Namely, that {} ⊢_{⊑} δ_{↓i} ⊑ δ_{↑i} for all δ_{i} in the resolution context.

TO COMPUTE FlexUpdate L( L-env, B_{F}, U-env)
WHERE U-env maps MATCHVARs in M to their upper bounds sets {δ_{↑}. . .}
 L-env       "                       lower bounds sets {δ_{↓}. . .}
 B_{F} is a list of flexible lower-bound constraints
DO
FOR EACH CONSTRAINT δ _{F} ⊑ (RUNION ν_{μ 1} . . . ν_{μ n}) IN B_{F}

FOR EACH ν_{μ i} ∈ {ν_{μ 1} … ν_{μ n}}

LOOKUP <ν_{μ i},{δ_{↓ MAX}}> IN L-env

IF δ _{F} ⊑ δ_{↓ MAX}

THEN CONTINUE WITH NEXT CONSTRAINT ;; Not in L_{F}, so punt
ELSE CONTINUE WITH NEXT ν_{μ i}
;; In L_{F}, so update L to FlexMAX
INITIALIZE f-consistent? TO FALSE ;; pessimistic flag

FOR EACH ν_{μ i} ∈ {ν_{μ 1} … ν_{μ n}}

LOOKUP <ν_{μ i},{δ_{↓ MAX}}> IN L-env

<ν_{μ i},{δ_{↑ MIN} }> IN U-env IF δ _{F} ⊑ δ_{↑ MIN}

THEN f-consistent? := TRUE
     UPDATE <ν_{μ i},{δ_{↓ MAX}}> IN L-env

TO <ν_{μ i}, FlexMAX({δ_{↓ MAX} δ _{F}},δ_{↑ MIN})>

IF (NOT f-consistent?) ;; was not set to TRUE so we lose

THEN FAIL "Inconsistent flexible terminal lower-bound constraint"

Figure 5-5: FlexUpdateL Subroutine Algorithm

TO PERFORM Abduce(τ_{↓} ⊑ τ_{↑}) WRT μ-env_{↓} assumed-⊑ μ-env_{↑} assumed-⊒
DO

⋮

[Unitary]. IF δ_{↑} = (RUNION ρ_{↑})
           THEN Abduce(δ_{↓} ⊑ ρ_{↑}) WRT μ-env_{↓} assumed-⊑ μ-env_{↑} assumed-⊒
[Flatten]. IF δ_{↓} = (RUNION ρ_{1} . . . ρ_{n})
           THEN FOR i FROM 1 to n
                Abduce(ρ_{i} ⊑ δ_{↑}) WRT μ-env_{↓} assumed-⊑ μ-env_{↑} assumed-⊒
[Cancel].  IF δ_{↑} = (RUNION ρ_{1} . . . ρ_{n})  AND δ_{↓} IS μ-CLOSED
           THEN IF THERE EXISTS A ρ_{i} ∈ {ρ_{1} . . . ρ_{n}} SUCH THAT δ_{↓} ≡ ρ_{i}
                THEN RETURN    ;; {} ⊢_{⊑} δ_{↓} ⊑ δ_{↑}
                ELSE IF ONLY ONE OF ρ_{1} . . . ρ_{n} IS μ-OPEN  ;; [Unitary]
                     THEN Abduce(δ_{↓} ⊑ ρ _{open}) WRT μ-env_{↓} assumed-⊑
                                               μ-env_{↑} assumed-⊒
                     ELSE UPDATE B_{F} TO INCLUDE δ_{↓} ⊑ (RUNION ρ_{j} . . . ρ_{k})

WHERE {ρ_{j} … ρ_{k}} = {ρ | ρ ∈ {ρ_{1} … ρ_{n}} and

                                                ρ is μ-CLOSED}
                     RETURN

⋮

OTHERWISE FAIL "Inconsistent terminal constraint"

Figure 5-6: Flexible Abduces Subroutine Algorithm

5.10 Context Resolution Without Parameter Liberation

One subtle well-formedness condition on resolution contexts [Definition 5.2.1] has heretofore been ignored. Specifically, matching must not liberate locally parameterized description variables. This problem is yet another of a plethora of concerns which encourage maintaining a highly decorated parse tree.^{17} We will see how decoration of a description according to whether it is open or closed will avoid inadvertent liberation of locally bound description parameters during resolution matching.

Consider the following Implicit Projection:

  (f e)    where    f : (POLY ((τ_{μ} TYPE))
                          (SUBR PURE ((POLY ((τ TYPE))
                                        (SUBR PURE ((PAIROF τ_{μ} τ @=)) τ)))
                                τ_{μ}))
                    e : (POLY ((τ TYPE))
                          (SUBR PURE ((PAIROF τ τ @=)) τ))

Recall [§ 5.2] that the implied projection is discovered by matching the argument’s type against the expected type specified in the operator. Specifically, we try to match the argument e’s type against the operator f’s formal parameter type as per:

(POLY ((τ TYPE))                        (POLY ((τ TYPE))
  (SUBR PURE ((PAIROF τ τ @=)) τ)) ⊑  (SUBR PURE ((PAIROF τ_{μ} τ @=)) τ))

where here τ_{μ} is the matchvar. The subtle problem is that τ_{μ} matches with τ, yielding the following invalid explicated projection: ((PROJ f τ) e). The problem is that τ has been liberated from the scope of its binding. This illustrates a correctness condition for Implicit Projection: the projection arguments inferred by the matching must not liberate parameterized description variables.

To prevent liberation of parameterized description variables upon matching, we have two choices: either the matching algorithm must detect liberation at match time, or the projection algorithm must check the projection arguments for liberation at projection time (by checking for free description variables). The latter alternative is unacceptable since it charges all projections with the cost of guarding against bogus matches. It also is not strictly correct since a liberated description variable may be captured by the surrounding scope of the Implicit Projection, in which circumstance the resulting projection argument would appear to be bound but the projection would nonetheless be incorrect. For example, imagine that the above Implicit Projection were enclosed by (PLET ((τ INT)) …). The τ will have been liberated from its scope as before, but this would be nontrivial to detect since another τ is bound in an outer scope. This issue is further complicated if, rather than attempting to match τ_{μ} with τ, we were to match it with say (REF τ) or any other type with an embedded free variable. Clearly, the preferred solution is for the matching algorithm to not generate bogus matches from the outset.^{18} But how?

17Recall that we have already seen [§ 3.1.1] motivation for tagging descriptions according to whether they contain (or are themselves) Sorting forms, or RECTYPEs, and the like.

What is needed is a restriction that matchvars may not match against descriptions that contain free parameterized description variables. This is easily enforced by internally decorating description expressions with an accounting of their free parameterized description variables. This decoration I call the openness status of a description. When this decoration indicates the existence of a free parameterized description variable within a description, that description cannot match against any matchvar, ever. Note that this entails decorating a description throughout, not just at the outermost level, since a matchvar may attempt to be matched against any subexpression within a matching description.^{19}

Having resolved this potential problem, I now return to the issue of incorporating flexibility indexing into the FIX implicit projection context resolution process.

18Although the interpreter described in [Jouvelot & Gifford 88] opted for the other choice. The Implicit Projection code was written by neither of those authors (nor by this author) and has not been defended as desirable. It was a preliminary experimental implementation intended primarily to flush out bugs in the language definition.

19FIX takes further advantage of this internal decoration when performing the substitution phase of the projection, as detailed elsewhere. For now, suffice it to say that it will be useful for this openness status tag to profile specifically which description variables appear free within the open description. This profile portion of the openness status decoration is dubbed the openness profile. Again, more detail elsewhere.

5.11 Summary of Implicit Projection

    Flattening:     (f x (f y z)) = (f x y z)        [F]
    Associativity:  (f x (f y z)) = (f (f x y) z)    [A]
    Commutativity:  (f x y) = (f y x)                [C]
    Idempotence:    (f x x) = x                      [I]
    Unity:          (f x 1) = x                      [U]
    Zero:           (f x 0) = 0                      [Z]
    Homomorphism:   (h (* x y)) = (+ (h x) (h y))    [H]

Figure 5-7: Equational Axioms Relevant to Set Descriptions

Noting the above algebraic equivalence axioms, consider the description equivalence axioms for REGION, EFFECT, and RECORDOF/ONEOF forms [§2.3.2–2.3.4]. First, RUNIONs denote sets and are therefore ACI. Note that RUNIONs have no unity [U] since we do not admit the empty set, viz., the empty region (RUNION). It would not denote a proper region of the store since it would intersect with all other regions. By contrast, MAXEFF is [ACIUZH] with:

                           1 = PURE = (MAXEFF)
                           0 = (WRITE @=)
                           h = READ/WRITE/ALLOC
                           * = RUNION
                           + = MAXEFF

that is,

  (READ  (RUNION r1 r2)) = (MAXEFF (READ  r1) (READ  r2))
  (WRITE (RUNION r1 r2)) = (MAXEFF (WRITE r1) (WRITE r2))
  (ALLOC (RUNION r1 r2)) = (MAXEFF (ALLOC r1) (ALLOC r2))

The equivalence and inclusion axioms introduce additional complexity. Specifically, RUNION and MAXEFF are flattening, variable-arity forms [F] whereas READ, WRITE, and ALLOC are not;^{20} however, internally, READ/WRITE/ALLOC can be represented as variable-arity forms to enhance uniformity. Finally, fieldname/type-pairs within RECORDOF/ONEOF forms are commutative [C]. How then does the FIX flexibility-index based, implicit projection context resolution algorithm accommodate these axioms?

First, no context resolution is attempted on non-normalized descriptions. Thus axioms [I] and [Z] can be disregarded. The [U] axiom applies only to effects (viz., PURE) which really just amounts to permitting unsatisfiable upper bounds on effects to bottom out rather than signal an immediate failure. The [A] axiom is dealt with by flattening all forms into variable-arity forms [F] whose elements can be ordered into a canonical order. Similarly, the [C] axiom is obviated by defining a partial order on elements (e.g., lexicographical ordering on description printnames) then ordering elements accordingly. The matchvars within these forms must be distinguished, however. This is not difficult to arrange. Finally, the [H] axiom is dealt with in MAXEFF forms by separating MAXEFF components into collected READs, WRITEs, ALLOCs, parameterized effects, and non-β-reducible description applications, reducing the problem to the previous cases. All this will be detailed in a forthcoming technical report. The only pending concern is for fieldname/type fields within RECORDOF/ONEOF forms. Of course, as an instance of the [C] axiom they can be ordered on the fieldnames. Moreover, since there is no flattening axiom for these components, we needn’t be concerned with ferreting them out within lower-bound instances. This is fortunate since doing so would involve a general glb procedure rather than the simple ⊑-based maximum test heretofore prescribed.

20Otherwise, the corresponding READ/WRITE/ALLOC axiom would not be well kinded since an effect cannot be an argument to an effect.

In sum then, the generalization of the flexibility index approach to doing context resolution over REGION and EFFECT forms is straightforward. The generalization over RECORDOF and ONEOF forms is likewise easy by involves testing more than mere occurrence of fieldname/type pairs since the type components of corresponding tag-field entries must be checked for inclusion. Nonetheless, the extension of the above described technique should be non-problematic so it is not detailed beyond its treatment above.

Finally, before leaving Implicit Projection, observe an interesting property of the destructive nature of the resolution context. Since the local environments (viz., L-env, U-env and B_{F}) are destructively updated only by strictly lowering their indices, the specific order in which a parallelized implementation may schedule such resolution is inconsequential so long as it corresponds to some sequential execution. Analogous observations apply to destructive update of resolution context bound entries. Such a blending of imperative with functional programming techniques within a parallel execution environment is the very raison d’être of FX-87. It would be interesting therefore to implement this in FX-87 itself to observe the effectiveness of the language. It has been argued [Day 87] that such data parallelism would not be effectively supported in FX-87 due to a lack of concurrent vector operations, although a modest effort has been made to alleviate this problem [Jouvelot 88]. More aggressive techniques for dealing with data parallelism have been proposed for the dataflow programming language ID by a mechanism called managers [Barth & Nikhil 89] and in the massively concurrent object-oriented language for MIMD architectures called Concurrent Aggregates (CA) [Chien & Dally 90]. How to incorporate such mechanisms into the effect system of FX-87 is an intriguing topic for future research.

5.12 Dynamically Bound Description Variables

One final complication exists for Implicit Projection in FX-87. It involves description variables which are dynamically scoped within the VDKenv during type and effect checking. For such variables, a local redefinition effectively acts as a mutation to the dynamic variable during the extent of the local redefinition. Any forward substitution must therefore be careful, within the body of higher order descriptions, not to replace free occurrences of such variables by their values since this value is not static. (An illustrative example of this follows later.) This implies that such references must be dereferenced in the dynamic VDKenv upon description application. Thankfully, there is no mechanism for the programmer to define a new dynamic description variable in FX-87; however, the language manual predefines one such variable: default-region [Gifford et al. 87, p.41]. It is used to establish a default region for implicit projections.^{21} This introduces three complications into the language.

First, as stated above, free occurrences of default-region must be dynamically resolved during type and effect checking. Specifically, free occurrences of it within Dλ and Pλ bodies must not be resolved until liberated from the scope of any dynamically enclosing PLET family member. For example:

  (PDEFINE mix-hue (Dλ ((r REGION)) (RUNION r default-region)))
  (PROJ (Pλ ((default-region REGION))
          (PLET ((r (mix-hue @RED)))
            (Pλ ((default-region REGION))
              ((PROJ NEW (mix-hue r)) 0))))
        @BLUE)
  : (POLY ((default-region REGION))
      (REF INT (RUNION (RUNION @RED @BLUE) default-region)))

Notice that, after the projection, the innermost description application of mix-hue is still within the scope of a statically enclosing Pλ whereas the application within the binding for r is liberated from its enclosing Pλ upon projection. Therefore, dereferencing is postponed for the occurrence of default-region within the inner call to mix-hue whereas the occurrence within the outer call to mix-hue is dereferenced upon projection (to yield

(RUNION @RED @BLUE)).

Second, the default-region is dynamically re-bound via PLET, PLET*, PLETREC, and Pλ forms [Gifford et al. 87, p.41]. Therefore, local rebindings of this variable via one of these forms must not be α-renamed else the intended rebinding of the global value would not be detected in subsequent phases. Note that this is not the case for local rebindings via DLET and family since these are not specified by the manual to perform rebinding of the global instance; here the α-renaming must be performed so as to eliminate the unintended shadowing. This reflects a disturbing asymmetry in the language: PLET and family perform dynamic rebinding of dynamic description variables (viz., default-region) whereas DLET and family do not. This is confusing in cases such as:

21Why such predefined dynamic variables are not provided for other circumstances, such as a default region in which to allocate aggregate data structures, was a matter of taste on part of the language designers.

  (PDEFINE mix-hue (Dλ ((r REGION)) (RUNION r default-region)))
  (LET ((make-shaded-INT-REF (PLET ((default-region @RED))
                               (PROJ NEW (mix-hue @BLUE)))))
    (make-shaded-INT-REF 0))
  :  (REF INT (RUNION @RED @BLUE))
  (LET ((make-shaded-INT-REF (PROJ NEW (DLET ((default-region @RED))
                                         (mix-hue @BLUE)))))
    (make-shaded-INT-REF 0))
  :  (REF INT (RUNION @RED @=))

Third, by introducing default-region as a dynamic description variable, the substitution semantics for the PLET family is violated. Specifically, the manual defines PLET as:

(PLET ((dvar_{1} δ_{1}) …) ν_{1} ν_{2} …)

The value of a PLET value expression is the value of its body. Whenever dvar_{i} is encountered [free]^{22} in the PLET body, it is replaced by δ_{i}. [Gifford et al. 87, p.43]

This is violated by PLET expressions whose bodies contain instances of Implicit Projection, since by eliminating the PLET surrounding the Implicit Projection the intended rebinding of default-region is lost. Thus, defining default-region to be a dynamic description variable is incompatible with defining substitution semantics for its rebinding forms, viz., PLET and family.

This is a mess. Admittedly, I’ve been indulging in irony: it was not the intention of the language designers that default-region be treated as a dynamic variable, although that is not what the manual entry says. To point, the manual defines:

… the special description variable default-region. This variable is initially bound to the value @=, but it may be re-bound by the programmer using PLET [and family]. [Gifford et al. 87, p.41] [Emphasis mine]

By the terminology of [Steele 85, Chap.3], this defines a dynamic variable; however, all that was intended by the designers of FX-87 is that there be a default region for Implicit Projection and that the programmer be able to temporarily override this default. Specifically, all free references to description variables are to be resolved lexically. This solves the first of the above mentioned three problems, but the other two remain.

First, the problem still remains of how to α-rename occurrences of default-region. The problem is that instances of Implicit Projection may contain implied occurrences of default-region. (See the Implicit Projection type and effect inference rule [§ 2.5.8].) This is a problem since it defines Implicit Projection to behave as if it were a description macro that expands into an explicit projection (PROJ) that may introduce new occurrences of default-region. How is this a problem? Well, this seems to imply that the macro expansion of all Implicit Projections must precede α-renaming since we must be sure to α-rename the implied instances of the identifier default-region; however, this macro expansion is contingent upon the description information associated with the application (for instance, the types and regions of the formals) which is not available until the type checking phase. Consequently, α-renaming cannot be performed until after type checking. This precludes early α-renaming altogether, which is a serious problem: recall [§ 3.1.1] that it was this early α-renaming strategy that eliminated shadowing, allowing simple substitution and trivial enforcement of the McCracken Criterion. Eliminating the ability to do this early renaming introduces significant complications to substitution and McCrackening. The substitution semantics for PLET similarly must require a macro-expansion pre-pass, which again cannot be performed until the type checking phase. Alternatively, the renaming and substitution could be performed up to the first occurrence of an Implicit Projection, delaying traversal into the body of the Implicit Projection until the type checking phase, but this complicates implementations. Therefore, merely stating that default-region be treated as an ordinary description variable does not suffice to allow early α-renaming and auto-McCrackening. As I shall argue presently, this complexity can all be avoided by reworking the treatment of the default region override mechanism. First, however, it is interesting to consider why these last two problems were not solved simply by declaring default-region to be a mere static description variable like any other.

22This corrects an oversight in the manual.

What is the underlying design problem? It is in considering Implicit Projection to be a macro that expands into an expression which may introduce instances of a description variable that may be captured by the surrounding context. Note that this capture is by design since this is what allows one to say that PLET and family “rebind” default-region: they rebind by capture. Upon more careful examination of this “call-by-macro-expansion” calling mechanism for Implicit Projection one should notice something suspicious: where did these new occurrences of default-region come from? The truth is that they were magically buried in the macro-definition of the Implicit Projection mechanism, where it was prearranged that they be resolved dynamically. Thus, we still have dynamic occurrences of the identifier default-region: burying these occurrences in the definition of a macro has not made them go away, it has merely obfuscated the problem.

Now, to address how to salvage the default region overriding mechanism. The mistake in the specified mechanism is in naming this default region by an identifier and exposing that identifier to the programmer. To point, the goal of providing an overriding mechanism for the default Implicit Projection region is similar to the goal in the value domain of being able to override the default port used to direct I/O in Scheme. The approach there

is to provide functions WITH-INPUT-FROM-FILE and WITH-OUTPUT-TO-FILE to temporarily

override the default input and output ports, respectively. Note that this allows overriding of defaults without exposing the name of the dynamic variable that their use implies. Thus, the Scheme programmer has no dynamic variables, so the myriad implementation difficulties caused by them do not arise in Scheme. Curiously, these same I/O facilities were provided in FX-87, but the design principle behind this approach was apparently overlooked when providing a default projection region.

To correct this oversight, I propose to replace all instances of:

  (PLET ((default-region ρ)) ν_{1} . . . ν_{n})

with:

  (WITH-DEFAULT-PROJECTION-REGION ρ ν_{1} . . . ν_{n})

where any Implicit Projections occurring within ν will use ρ as the default projection region. Thus, the identifier default-region is just an identifier like any other, with no special status in the language. Specifically, it is not the name of the dynamic description variable implied by the above form. Should the programmer wish to re-establish the previous default while maintaining a handle on this new default, this can be done as:

  (LET ((new-default-region ρ))
    (WITH-DEFAULT-PROJECTION-REGION new-default-region ν))

where new-default-region can occur free within ν.

How can this be efficiently implemented? Within the internal state of the type checking phase, the current value of the default region may be maintained on a stack separate from the VDKenv. Initially, this stack should contain @= as the default projection region [Gifford et al. 87, p.41]. Upon encountering WITH-DEFAULT-PROJECTION-REGION, the ρ argument is pushed onto this stack. Upon encounter of an Implicit Projection, the current top-of-stack is used as the default projection region.

Interestingly, this approach is not substantially different in implementation detail from the above Implicit-Projection-as-macro-expansion approach: consider that performing type checking in the absence of having eliminated shadowing reduces to traversing an expression while maintaining a stack-like environment that maps description variables to their current lexically closest bindings. Of course, FIX does likewise but the difference is that in the macro model the default region is maintained in the same stack as the lexical variables so interactions with other elements of the same stack must be considered. In the separatestack approach, no such interactions are possible since the default region stack is entirely inaccessible to the FX-87 programmer. By providing this separation, early α-renaming can be performed on the variables which occur in the programmer-visible environment without concern for the default region stack.

Effects in FX-87

Until now, we have ignored the intent of including effect annotations within SUBR types. This chapter considers in more detail how these effects can actually be used. Specifically, in this chapter we consider briefly what their intended use is, then we consider in detail how to make these effect annotations precise when inferred by the FX-87 type/effect checker.

6.1 Effects: What They Mean

Recall [§ 2.5] that the type/effect checking rule for λ expressions includes not only the types of the expected arguments and of the returned value but also the effect which can be incurred on the store when the procedure is invoked. This latent effect is useful for a number of compiler optimizations. As mentioned in Section 1.2, these include automatic memoization of PURE procedures, stack allocation of non-exposed locals, and perhaps the most important use: automatic parallelization of compiled code. In fact, one of the primary design goals of the FX-87 language was to support a mixture of imperative and functional programming styles within a parallelizing run-time environment [Gifford & Lucassen 86] [Lucassen & Gifford 88]. The success of this mixing of styles depends crucially on the ability of the compiler to “mask” those effects which occur within a procedure but which are not externally observable.

The rule for when this masking is permitted is called the Effect Masking Rule. As it is stated in the FX-87 Reference Manual [Gifford et al. 87, p.30], this rule is succinct but difficult to fathom and not particularly precise in masking all provably non-observable effects. I include it here for completeness, even though we will derive an improved rule.

If a value expression has effects on some region r, and if r does not appear in the type [or region]^{1} of any free ordinary variables in the expression, then any READ or WRITE effect on r is masked; furthermore, if r does not appear in the type of the whole expression, then any ALLOC effect on r is also masked.

This rule is formalized and its soundness proposed in [Gifford et al. 87, Appendix B].

1Omission noted by both Pierre Jouvelot and James O’Toole

The precision with which this rule can mask effects which are in fact not externally observable is crucial for permitting parallelism in FX-87 programs. Unfortunately, it does not do as precise a job as it could. For this reason, I will not belabor explaining the rule as stated in the manual, nor will I directly address how it could be implemented efficiently within FIX. Instead, I discuss in the remainder of this chapter what the issues are behind effect masking, then I propose an improved masking rule and demonstrate how it can be efficiently implemented. Once the issues have been presented, the improved rule should seem relatively straightforward and its implementation is likely to perform more efficiently (and certainly more precisely) than the rule prescribed by the manual. We proceed by developing a READ and WRITE Effect Masking Rule, afterward considering ALLOC masking.

6.2 Observability of READ and WRITE Effects

We now derive a READ and WRITE effect masking rule by considering the following (contrived but nonetheless illustrative) sample program:

(DEFINE global-mutable-vector ((PROJ VECTOR @GMV) #F #F))
(DEFINE global-reader  (λ () (VECTOR-REF  global-mutable-vector 0)))
(DEFINE global-writer! (λ ((b BOOLE))
                             (VECTOR-SET! global-mutable-vector 1 b)))
(DEFINE global-string "Down" @GSTRING)
(DEFINE global-symbol 'BEAM)
(DEFINE xport (λ ((whom SYMBOL)(where STRING))
  (LET* ((local-mutable-vector ((PROJ VECTOR @LMV) 'SPOCK 'SCOTT 'KIRK))
         (local-reader (λ () (VECTOR-REF local-mutable-vector 1))))
    (global-reader)
    (global-writer! #T)
    (SET! global-string where)
    (VECTOR-SET! local-mutable-vector 0 whom)
    (VECTOR global-symbol
            (VECTOR-REF  local-mutable-vector 0)
            global-string
            (local-reader)
            (VECTOR-REF global-mutable-vector 1)))))
(xport 'ME "Up")

Ignoring for now all ALLOC effects,^{2} let’s consider step by step what observable READ and WRITE effects the call to xport may have when evaluated.

First, global-reader is invoked, which will incur a READ effect on the region in which the components of global-mutable-vector were allocated (viz., @GMV); however, this READ is not observable since it was performed by a piece of non-returning code— that is, the expression does not have an observable WRITE effect and its return value is not used so this expression can be dead-code eliminated at compile time. Were this not the case, the READ could not be masked. Notice, by the way, that this maskable (READ @GMV) effect appears in the type of global-reader. Second, global-writer! is invoked. Again, the result of this procedure invocation is not used, but unlike the call to global-reader, global-writer! incurs a WRITE effect (on @GMV). This WRITE effect cannot be masked since it will be externally visible to processes performing READ effects to @GMV. Notice, by the way, that this (WRITE @GMV) appears in the type of global-writer!. Next, a SET! is performed on global-string, which incurs a (WRITE @GSTRING) effect. This cannot be masked since it is observable by any other process which may reference global-string. Next, a WRITE effect is incurred on the locally defined local-mutable-vector. Since this vector is never exposed to external processes, this WRITE is unobservable outside the LET expression; however, within the LET expression this WRITE is observable so it should not be masked until outside the scope of the LET binding.^{3} Lastly, we return a VECTOR but only after having evaluated its arguments in an unspecified order.^{4} Imagining, for the sake of argument, that the arguments are evaluated left-to-right this time, the reference to global-symbol will be PURE since it is not defined to be a mutable variable. Next, the VECTOR-REF to local-mutable-vector will incur a READ effect on @LMV because this is where the variable’s binding was ALLOCd, but it will be masked outside the scope of the LET since local-mutable-vector is not externally accessible. By contrast, the reference to global-string will incur a READ on @GSTRING which cannot be masked since external WRITEs to it must be properly synchronized with respect to this READ to preserve the sequential semantics of the language. For example, if the above call to export appeared in a BEGIN code block in which a preceding expression incurred a WRITE to @GSTRING, then a data dependency would exist between the two expressions so a synchronization point must be imposed to maintain the sequential semantics of the code block. Next, the invocation of local-reader will incur a READ effect on @LMV which will be unobservable outside the scope of the LET, thus it can be masked. And finally, the VECTOR-REF to global-mutable-vector will incur an unmaskable READ effect since this is a mutable externally visible datum.

2In fact, xport has no externally observable ALLOC effects when invoked.

6.3 Classes of Region Occurrences

The above discussion encourages us to distinguish four distinct classes of region occurrences, which are enumerated below. Specifically, our first two considerations focused on two of these classes: those regions which appear within the types of free SUBR variables either within 1) READ or 2) WRITE components. More generally, we should consider those components of any free variable whose type may contain a SUBR type, for instance a REF to a SUBR or even a PURESUBR which returns a SUBR with latent READ/WRITE effects.^{5} The third consideration involved 3) those regions in which free variables have been bound— that is, not where the binding’s components have been allocated, but specifically where the variable binding itself has been allocated. For example, to define a global mutable variable we must specify where that variable is to allocate its binding so that subsequent SET! expressions can mutate it. This is contrasted with the fourth consideration, which isolated interest on 4) those region components in which free mutable structure components were allocated— that is, the regions of the components of the bindings, not the regions of the bindings themselves. The final considerations further involved READ effects over these region occurrence classes.

3This point is addressed in detail when we discuss implementation of the effect masking rule(s) [§ 6.7].

4Actually, the FX-87 manual dictates a left-to-right evaluation order on applications [Gifford et al. 87, p.36], but I choose to ignore this for several reasons. First, it is a gratuitous violation of the Scheme standard so Scheme-based implementations of FX-87 would be unduly complicated. Second, it encourages a poor style of programming, leaving potentially critical dependencies implicit in the program. Finally, it complicates certain compiler optimizations on FX-87 programs such as optimized register allocation on tail-recursive calls: the dependency issue can be ignored if no order of evaluation is specified.

We formalize these notions, following Lucassen [Gifford et al. 87, Appendix B.5], by first introducing locations, l_{τ,ρ}, subscripted by both the type of values which they can contain and by the (possibly intersecting and possibly discontiguous) regions of the store which these locations encompass. We then define selectors T (l_{τ,ρ}) = τ and R(l_{τ,ρ}) = ρ. In general, we will omit the type and region subscripts in what follows, instead subscripting locations by natural numbers to distinguish them. We define the Venv to map value domain variables to their associated locations, while introducing a store (denoted σ) which maps locations to values in canonical form (denoted ν_{canonical}). We define the store valuation function S on value expressions (denoted ν), given a Venv and store, to yield a (possibly extended) store which reflect the effect of having canonicalized ν.^{6} We define the value valuation function V over the same domain to yield a value in canonical form (e.g., V((+ 1 2), initial − Venv, initial − Store) = 3). That is:

l ∈ Loc = {l_{1} l_{2}...}
env ∈ Venv : Vvar ↦ Loc
σ ∈ Store : Loc ↦ Val_{canonical}
S : Val × Venv × Store ↦ Store
V : Val × Venv × Store ↦ Val_{canonical}

These valuation functions are the standard semantic valuation functions defined over well-formed FX-87 value expressions. For the formal semantics, as well as the definition of well-formedness in this context, see [Gifford et al. 87, Appendix B]. The language considered here is but a modest extension of that formal language, which in turn follows closely the formal semantic definition of the second-order typed λ-calculus. The type and effect inference rules of Section 2.5 are based on these valuation functions (and, hence, on the type and effect inference rules of [Gifford et al. 87, ibid.]). The major simplification made in my presentation has been to combine the value and description environments and stores into a single VDKenv in the type and effect inference rules. In what follows, we casually substitute ⟨env, σ⟩ for what we have heretofore denoted as simply VDKenv.

5Notice that we need not consider the argument types in SUBRs. This point will be discussed more carefully when considering ALLOC masking below.

6We do not consider Venv extension resulting from top-level DEFINE forms, nor do we consider a description environment (Denv) or description store (Dstore) with Denv extension via top-level PDEFINE forms.

These extensions are straightforward so they have been suppressed in the interest of conciseness.

We proceed by defining the evaluation of value expressions to involve a reduction from state to state, where a state (denoted θ) is a triple of Val × Venv × Store. The evaluation reduction, ⟹^{red}, is then a mapping from state to state, again as defined by Lucassen. For our purposes, it is of interest only to note that the transitive closure of ⟹^{red} (denoted ⟹^{red}^{∗}) yields a canonical state (i.e., a state whose value component is fully evaluated, denoted by ν_{canonical}); hence ⟹^{red}^{∗} is called a canonicalization. More importantly, value canonicalization respects the value and effect valuation functions as per:

Lemma 6.3.1

⟨ν, env, σ⟩ ⟹^{red}^{∗} ⟨ν_{canonical}, env, σ′⟩  for ν_{canonical} = V(ν, env, σ)
σ′ = S(ν, env, σ)

We are now equipped to introduce notation for the set of locations read and written by the evaluation of an expression as follows:

For θ = ⟨ν, env, σ⟩ : R_{l}(θ) = {l ∈ Domain(σ) | θ ⟹^{red}^{∗} θ_{canonical} reads l}
W_{l}(θ) = {l ∈ Domain(σ) | θ ⟹^{red}^{∗} θ_{canonical} writes l}

Similar to Lucassen, R_{l}(θ) and W_{l}(θ) (read “read locations” and “written locations”) are the set of locations observably read and written, respectively, in the process of reducing the value component of θ to canonical form.^{7} Although left implicit by Lucassen, to say that a canonicalization “reads l” is to have said that the location l that was created by an application of NEW has been passed as the argument to an invocation of GET. Similarly, a canonicalization “writes l” if l is the argument to an invocation of SET, as in (SET l <newval>). It is straightforward to generalize this notion of locations read and written by a canonicalization (the cell model of mutable memory) to include mutable structure creation, access and mutation (e.g., via CONS, CAR, CDR, SET-CAR! and SET-CDR! for PAIROFs). I omit the details for conciseness.

We relate value canonicalization (⟹^{red}^{∗}) to the type and effect checking rules [§ 2.5] by recasting Lucassen’s type and effect soundness claims in our new notation:

Claim 6.3.1 [Soundness of Type and Effect Inference Rules]

         ⟨env, σ⟩ ⊢  ν : τ ! (MAXEFF (READ ρ_{r})(WRITE ρ_{w})(ALLOC ρ_{a}))

⟨ν, env, σ⟩ ⟹^{red}_{∗} ⟨ν_{canonical}, env, σ′⟩
⟨env, σ⟩ ⊢  ν_{canonical} : τ
{} ⊢_{⊑} injρ({R(l) | l ∈ R_{l}(⟨ν, env, σ⟩)}) ⊑ ρ_{r}
{} ⊢_{⊑} injρ({R(l) | l ∈ W_{l}(⟨ν, env, σ⟩)}) ⊑ ρ_{w}

Here and throughout, injρ maps a set of (closed) region descriptions to the RUNION over those region descriptions.^{8} Intuitively, this soundness claim states that if a value can be shown from the type and effect checking rules to have type τ and READ and WRITE effects on regions ρ_{r} and ρ_{w}, respectively (for now, we ignore the ALLOC effects on region ρ_{a}), then the fully canonicalized value (ν_{canonical}) will provably be of type τ and the regions observably read and written in this canonicalization process will be a subset of those estimated by the type and effect checking rules.

7Lucassen does not consider forms which allocate mutable locals such as LETREC or the introduction of mutable formal parameters in λ applications. He also does not consider immutable locations, but we consider them in saying that a reduction “reads l” or “writes l” in that reads to the immutable region @= do not count and writes to @= are illegal.

Finally, we may now discuss the goal of effect masking formally. Specifically, computing precisely the set of locations observably read and written in the canonicalization of an expression is, in general, undecidable. Even settling for a minimally conservative decidable approximation would require a complex and potentially expensive non-standard abstract interpretation of value expressions [Weihl 80]. As an alternative, effect masking allows us to perform a simpler, primarily syntactic flow-insensitive analysis of an expression to compute a conservative approximation of the same information but to do so based on regions rather than on locations per se. If the programmer is careful to allocate distinguished locations in distinct regions, then this effect masking should produce precisely the same information as a more complex semantic analysis.^{9}

Returning to the derivation of a READ and WRITE effect masking rule, we are now equipped to formally define selectors for the classes of region occurrence described earlier. First, we define selectors ρ_{R} and ρ_{W} (read “region READ occurrences” and “region WRITE occurrences”) for region occurrences within a description, δ, as follows:

ρ_{R}(δ) — regions appearing within READ effects of SUBR latent effects and return types in δ

or those appearing within region components of returned structure types in δ

ρ_{W}(δ)— regions appearing within WRITE effects of SUBR latent effects and return types in δ or those appearing within region components of returned mutable structure types in δ

Next, we define FV_{l} (read “free variable locations”) to select the locations of the free variables of a value given an environment. Using this, we define FV_{ρ} and FV_{τ} which select the binding regions and types of the free variable locations:

FV_{l}(ν, env) = { l | l = env(var) for some var ∈ FV(ν)}
FV_{ρ}(ν, env) = {R(l) | l ∈ FV_{l}(ν, env)}
FV_{τ} (ν, env) = {T (l) | l ∈ FV_{l}(ν, env)}

8By convention, injρ({}) = ⊥REGION where by definition (READ ⊥REGION) = (WRITE ⊥REGION) = (ALLOC ⊥REGION) = PURE. Note that ⊥REGION is not equivalent to @= since (WRITE @=) is forbidden.

9Unfortunately, it is not always possible to allocate distinct locations in distinct regions. For example, looping constructs like DO must allocate locals in the same regions with each iteration.

Now, we define the region occurrence classes desired for masking as follows (the boxed numbers relate these terms to the region occurrence classes as enumerated at the beginning of this section [p. 97]):

R_{ρ}(ν, env) = \overbrace{\{ ⋃_{i} ρ_{R}(τ_{i}) | τ_{i} ∈ FV_{τ} (ν, env)\}}^{1 & 4} ∪ \overbrace{FV_{ρ}(ν, env)}^{3}
W_{ρ}(ν, env) = \underbrace{\{ ⋃_{i} ρ_{W}(τ_{i}) | τ_{i} ∈ FV_{τ} (ν, env)\}}_{2 & 4} ∪ \underbrace{FV_{ρ}(ν, env)}_{3}

We read R_{ρ} as “observable READ regions” and W_{ρ} as “observable WRITE regions”.

Claim 6.3.2 {} ⊢_{⊑} injρ({R(l) | l ∈ R_{l}(⟨ν, env, σ⟩)}) ⊑ injρ(R_{ρ}(ν, env))

{} ⊢_{⊑} injρ({R(l) | l ∈ W_{l}(⟨ν, env, σ⟩)}) ⊑ injρ(W_{ρ}(ν, env))

This formally states that R_{ρ} and W_{ρ} compute conservative estimates of the regions observably read and written, respectively, in the canonicalization of state ⟨ν, env, σ⟩ for any choice of store σ.

6.4 The READ and WRITE Effect Masking Rule

Using the notation of the preceding section, we may now formalize our earlier discussion of observable READ and WRITE effects by the following READ and WRITE Effect Masking Operators and the READ and WRITE Effect Masking Rule followed by a soundness claim relating effect masking over the type and effect inference rules to value canonicalization

(⟹^{red}^{∗}).

Definition 6.4.1 [READ and WRITE Effect Masking Operators]

• R_{unmaskable}(ρ_{r} , ν, env) = ρ_{r} ⊓ injρ(R_{ρ}(ν, env))

• W_{unmaskable}(ρ_{w}, ν, env) = ρ_{w} ⊓ injρ(W_{ρ}(ν, env))

Moreover, dead-code READs may be ignored when computing R_{ρ}(ν, env) (and a warning should be issued if indeed any are discovered).

Here and throughout, ⊓ denotes the “meet” operator defined as the greatest lower bound (glb) with respect to description inclusion (⊑). Similarly, we may have occasion to employ the “join” operator ⊔ which denotes the least upper bounds (lub) with respect to ⊑.^{10} Intuitively, the READ and WRITE masking operators define those regions in ρ_{r} (resp., ρ_{w}) which may not be disregarded when considering the observable READ (resp., WRITE) effects incurred in the canonicalization of ν in environment env and any store σ. By contraposition, therefore, those regions not selected by these operators can be disregarded.

10We will use these only over region descriptions, for which they are always defined given that regions denote sets and given our newly introduced null-region ⊥REGION.

Lemma 6.4.1 [Soundness of READ and WRITE Effect Masking Operators]

       ⟨env, σ⟩ ⊢ ν ! (MAXEFF (READ ρ_{r})(WRITE ρ_{w})(ALLOC ρ_{a}))

{} ⊢_{⊑} injρ({R(l) | l ∈ R_{l}(⟨ν, env, σ⟩)}) ⊑ R_{unmaskable}(ρ_{r} , ν, env)
{} ⊢_{⊑} injρ({R(l) | l ∈ W_{l}(⟨ν, env, σ⟩)}) ⊑ W_{unmaskable}(ρ_{w}, ν, env)

Intuitively, this states that the set of observable READ (resp., WRITE) effects incurred by the canonicalization of a state is a subset of the READ (resp., WRITE) effects remaining after applying the READ (resp., WRITE) effect masking operator to the region of the READ (resp., WRITE) component of the effect computed by the type and effect inference rules.

We can therefore safely incorporate these effect masking operators into the type and effect inference system via the following Effect Masking Rule:

Definition 6.4.2 [READ and WRITE Effect Masking Rule]

       ⟨env, σ⟩ ⊢ ν ! (MAXEFF (READ ρ_{r})(WRITE ρ_{w})(ALLOC ρ_{a}))

⟨env, σ⟩ ⊢ ν ! (MAXEFF (READ R_{unmaskable}(ρ_{r} , ν, env))
(WRITE W_{unmaskable}(ρ_{w}, ν, env))(ALLOC ρ_{a}))

Lemma 6.4.2 [Soundness of Effect Inference with READ and WRITE Masking] Extending the system of type and effect inference rules of Section 2.5 to incorporate the READ and WRITE Effect Masking Rule preserves the soundness of the type and effect inference rules proved by Lucassen [Lucassen 87].

This means, in short, that the type and effect of an expression, as inferred by the type and effect inference rules with READ and WRITE effect masking, is a conservative estimate of the actual type and effect of the expression. As a consequence, the compiler writer can use these rules as a basis for various optimizations of the object code. As mentioned in Section 1.2, this masking expands the set of expressions for which the compiler can soundly employ memoization (software caching), common subexpression elimination, code motion within side-effect boundaries, and parallelization of non-interfering expressions. Naturally, the objective of any implementation of the resulting inference system is to compute the least type and effect possible with respect to the inclusion axioms.

6.5 Observability of ALLOC Effects

In short, ALLOC effects are visible only when the allocated memory is “exposed”. Allocation is exposed in only one of three ways: a mutable aggregate is allocated (e.g., via CONS) and is permitted to escape from the lexical context in which it was created either 1) by being directly returned within the return value, or 2) by being stored into an externally defined datum; or 3) a mutable local variable is allocated and it is closed over by one or more locally defined procedures which collectively both read and write the local and which are permitted to escape from the lexical context in which they were created.^{11} An (admittedly contrived) program fragment which exemplifies all these cases follows:

(DEFINE global-mutable-vector ((PROJ VECTOR @HAT)   ; a catty pair...
                                 ((PROJ CONS @BLUE) 'DOLPHIN 'WHALE)))
(DEFINE seuss-itate (λ ()
  (LET (( red-fish 'HERRING @RED)                    ; a mutable local var
        (blue-fish ((PROJ CONS @BLUE ) 'SCROD 'COD)) ;   mutable pairs...
        (ges&h     ((PROJ CONS @GREEN) 'CHICKEN-EMBRYOS 'N1DZE)))
    (VECTOR-SET! global-mutable-vector 0 blue-fish)
    (LET ((reader   (λ () red-fish))
          (mutator! (λ ((new-fish SYMBOL)) (SET! red-fish new-fish))))
      (CONS (VECTOR reader mutator!) ges&h)))))
(DEFINE seuss-pool (seuss-itate))

Note that we are not concerned with the allocation of immutable values (such as the local variables blue-fish and ges&h) but rather with the allocation of mutable values only (such as the mutable pairs to which blue-fish and ges&h are bound, and the mutable local red-fish over which reader and mutator! are closed).

When invoked, seuss-itate should be considered to have an ALLOC effect on the @RED, @BLUE, and @GREEN regions— in FX-87 parlance, one would say therefore that the LET expression has (at least) the effect (ALLOC (RUNION @RED @BLUE @GREEN)). Let’s consider each distinct allocation in turn.

First, consider what would happen if only reader were returned (via the returned vector) but not mutator!. In that case, two separate evaluations of the LET expression would produce two distinct reader procedures which are nonetheless operationally indistinguishable. This is because no means will have been provided whereby either instances of the locals over which the readers were closed could be altered. Conversely, if only mutator! were returned but not reader, two distinct procedures would be produced that mutate a closed local which no process (not even themselves!) would be able to read. Thus, in both cases the allocation to @RED could be made to immutable storage instead since in the one case no mutation would be feasible while in the second the mutation would be effectively unobservable. Of course, to allow ALLOC masking by virtue of providing only a reader or only a mutator to a local is likely to be a reflection of a programmer error, so it would not be unreasonable for an implementation to signal a warning in such situations to encourage the programmer to re-seuss-itate the program.

11Not unexpectedly, these are all instances of the more general notion that whenever the extent of a mutable locally allocated datum exceeds its scope, that allocation is potentially observable.

With this first maskability issue in mind, consider the type of the value returned:

(PAIROF (VECTOROF (SUBR (READ  @RED)  ()   INT)
                  (SUBR (WRITE @RED) (INT) INT)
            @=)
        (PAIROF SYMBOL SYMBOL @GREEN)
    @=)

The important detail here is that within this return type there appears both a READ and a WRITE effect on the region in which the mutable local will be allocated (viz., @RED). We conclude from this that ALLOC effects to regions which appear in both READ and WRITE regions within the latent effect (or return type) of a returned SUBR component may not be masked.

Notice one subtlety above in the treatment of SUBR types. Were we to return only a reader, but one which accepts an argument which is itself a SUBR with a WRITE effect, this argument type of the reader would not indicate an ability to mutate the local which we have allocated. Thus, for purposes of seeking out READ and WRITE effects of returned SUBRs, we always completely ignore the arguments’ types, looking only at the latent effect component and the return type since only these components reveal if the SUBR returned will expose the local storage or will itself return a SUBR which will expose the local storage. More generally, when discussing any region components of a type, we will heretofore take this to mean that the argument-type components within SUBR types are to be ignored.

Next, imagine if the storage of blue-fish into global-mutable-vector via the call to VECTOR-SET! had not been performed. Then the allocation of the blue-fish pair components in @BLUE would be unobservable. The interesting detail to note here is that whenever a global variable (or, more generally, a free variable) appears within an expression wherein some newly allocated structure is stored into that variable, the type of the variable’s binding (in this example, (PAIROF SYMBOL SYMBOL @BLUE)) must mention the region in which the new structure’s components were allocated in order for the mutation to be permitted. Thus, if the programmer takes care to allocate local structure components in regions which do not collide with the region components appearing in the types of free variables bound to mutable structure, then we may conclude with no loss of precision that ALLOC effects to regions which do collide in this manner may not be masked. This is a modest, natural discipline to impose on the programmer who is interested in precise masking. In essence, it encourages the programmer to use regions to encode patterns of potential sharing.

Finally, the locally allocated mutable pair ges&h was returned as a component of the pair returned by the LET expression. Notice that, therefore, the region in which ges&h’s mutable components were allocated (viz., @GREEN) will appear in the region component of a mutable structure type within the return type (viz., (PAIROF SYMBOL SYMBOL @GREEN)). Therefore, we conclude that ALLOC effects to regions appearing within mutable structure components of the result type of an expression may not be masked.

In light of this discussion, we are now prepared to formally define the set of locations observably allocated by the evaluation of an expression as follows. First, let ψ_{closed} denote the functions with no free variables other than primitives (i.e., those functions closed with respect to the initial FX-87 user environment). Now, let l_{R}(ν_{canonical}, σ′) and l_{W}(ν_{canonical}, σ′) (read “locations readable” and “locations writable”) denote the set of locations which can be respectively read and written through manipulation of canonical value ν_{canonical} given a store σ, as follows:

l_{R}(ν_{canonical}, σ) = {l ∈ Domain(σ) | There exists some function f ∈ ψ_{closed}

for which the canonicalization of (f ν_{canonical}) reads l.}

l_{W}(ν_{canonical}, σ) = {l ∈ Domain(σ) | There exists some function f ∈ ψ_{closed}

for which the canonicalization of (f ν_{canonical}) writes l.}

Finally, using these and extending from Lucassen [Gifford et al. 87, Appendix B.5], we define A_{l}(θ) (read “allocated locations”) to be the set of locations observably allocated in the process of canonicalizing θ, as follows:^{12}

A_{l}(θ) = {l ∈ Domain(σ′) | θ ⟹^{red}^{∗} θ_{canonical} allocates l} ∩ l_{R}(ν_{canonical}, σ′)
∩ l_{W}(ν_{canonical}, σ′)
where  θ = ⟨ν, env, σ⟩
θ_{canonical} = ⟨ν_{canonical}, env, σ′⟩

Note that our attention to l_{R}(ν_{canonical}, σ′) and l_{W}(ν_{canonical}, σ′) is concerned solely with discounting allocated locations which cannot subsequently be effectively both read and written. Again, the case of solely readable locations may be commonplace in well-written FX-87 programs, but the case of solely writable locations probably signifies a programming error so should be brought to the attention of the FX-87 programmer by emitting a compiler warning.

We can now fully relate value canonicalization (⟹^{red}^{∗}) to the type and effect checking rules [§ 2.5] by recasting Lucassen’s type and effect soundness claims in our new notation:

Claim 6.5.1 [Soundness of Type and Effect Inference Rules]

         ⟨env, σ⟩ ⊢  ν : τ ! (MAXEFF (READ ρ_{r})(WRITE ρ_{w})(ALLOC ρ_{a}))

⟨ν, env, σ⟩ ⟹^{red}_{∗} ⟨ν_{canonical}, env, σ′⟩
⟨env, σ⟩ ⊢  ν_{canonical} : τ
{} ⊢_{⊑} injρ({R(l) | l ∈ R_{l}(⟨ν, env, σ⟩)}) ⊑ ρ_{r}
{} ⊢_{⊑} injρ({R(l) | l ∈ W_{l}(⟨ν, env, σ⟩)}) ⊑ ρ_{w}

Intuitively, this soundness claim states that if a value can be shown from the type and effect checking rules to have type τ and READ,WRITE, and ALLOC effects on regions ρ_{r}, ρ_{w}, and ρ_{a} respectively, then the fully canonicalized value (ν_{canonical}) will provably be of type τ and the regions observably read, written, and allocated in this canonicalization process will be a subset of those estimated by the type and effect checking rules.

As with detecting observable READ and WRITE effects, a non-standard abstract interpretation of value expressions could be defined to precisely detect observable ALLOC effects, but again this would be complicated and potentially expensive. Again, therefore, we develop a more simple, primarily syntactic analysis of an expression to compute a conservative approximation of the same information but to do so based on regions rather than on locations per se. Specifically, using this notation, we can relate the semantic and syntactic ALLOC properties of expressions as follows:

12Lucassen does not consider forms which allocate mutable locals such as LETREC or the introduction of mutable formal parameters in λ applications. He also does not consider immutable locations, but we consider them in saying that a reduction “allocates l” in that allocation in the immutable region, @=, does not count.

Claim 6.5.2

⟨env, σ⟩ ⊢ ν_{canonical} : τ
{} ⊢_{⊑} injρ({R(l) | l ∈ l_{R}(ν_{canonical}, σ)}) ⊑ injρ( ρ_{R}(τ))
{} ⊢_{⊑} injρ({R(l) | l ∈ l_{W}(ν_{canonical}, σ)}) ⊑ injρ(ρ_{W}(τ))

Intuitively, this states that by merely analyzing the type of a canonicalized value, we can discover all regions of the store which can be observably read and written via manipulation of the value given a store.

Returning now to the derivation of an ALLOC effect masking rule, we are equipped to formally define the “observable ALLOC regions” occurrence class as:

A_{ρ}(ν, env, σ, τ, ρ_{w}) = ρ_{R&W}(τ) ∪ R&W_{ρ}(ν, env, ρ_{w})
where  ρ_{R&W}(δ) = {ρ | {} ⊢_{⊑} ρ ⊑ injρ(ρ_{R}(δ)) ⊓ injρ(ρ_{W} (δ))}
R&W_{ρ}(ν, env, ρ_{w}) = \{ \begin{matrix}if & W_{unmaskable}(ρ_{w}, ν, env) = \{\} \\ then & \{\} \\ else & \{ρ | \{\} ⊢_{⊑} ρ ⊑ injρ(R_{ρ}(ν, env)) ⊓ injρ(W_{ρ}(ν, env))\} \end{matrix}

Naturally, we read ρ_{R&W} as “region READ&WRITE occurrences” and R&W_{ρ} as “observable READ&WRITE regions”.

Notice that this suggests that ALLOC effect masking presumes READ and WRITE effect masking. Specifically, the conditional within the definition of R&W_{ρ}(ν, env, ρ_{w}) reflects our concern with exposing a locally allocated location by writing it into a free variable in a manner which would make the allocation observable by virtue of there existing both read and write access to the variable’s value components. Clearly, if no writes occur during the canonicalization of ν (i.e., ρ_{w} = ⊥REGION) then this is a mute concern. We will see later that this can be relaxed ever when writes do occur.

6.6 The ALLOC Effect Masking Rule

Using the notation of the preceding section, we may now summarize the discussion of observable ALLOC effects by the following ALLOC Effect Masking Rule followed by a soundness claim relating effect masking over the type and effect inference rules to value reduction.

Definition 6.6.1 [ALLOC Effect Masking Operator]

• A_{unmaskable}(ρ_{a}, ν, env, σ, τ, ρ_{w}) = ρ_{a} ⊓ injρ(A_{ρ}(ν, env, σ, τ, ρ_{w}))

Intuitively, this operator defines those regions in ρ_{a} which may not be disregarded when considering the ALLOC effects incurred in the canonicalization of ν in environment env and store σ where, in addition, τ and the regions in ρ_{w} reflect potential points of exposure of allocate effects. Conversely, those regions not selected by this operator can be disregarded.

Lemma 6.6.1 [Soundness of ALLOC Effect Masking Operator]

    ⟨env, σ⟩ ⊢ ν : τ ! (MAXEFF (READ ρ_{r})(WRITE ρ_{w})(ALLOC ρ_{a}))

{} ⊢_{⊑} injρ({R(l) | l ∈ A_{l}(⟨ν, env, σ⟩)}) ⊑ A_{unmaskable}(ρ_{a}, ν, env, σ, τ, ρ_{w})

Intuitively, this states that the set of observable ALLOC effects incurred by the canonicalization of a state is a subset of the ALLOC effects remaining after applying the ALLOC effect masking operator to the region of the ALLOC effect computed by the type and effect inference rules, using the type of the return value and the region of the WRITE effect computed by the inference rules as indications of when local allocations may have been exposed.

We therefore incorporate this final effect masking operator into the type and effect inference system via the following full Effect Masking Rule:

Definition 6.6.2 [Full FIX Effect Masking Rule]

       ⟨env, σ⟩ ⊢ ν : τ ! (MAXEFF (READ ρ_{r})(WRITE ρ_{w})(ALLOC ρ_{a}))

⟨env, σ⟩ ⊢ ν : τ ! (MAXEFF (READ R_{unmaskable}(ρ_{r} , ν, env))
(WRITE W_{unmaskable}(ρ_{w}, ν, env))
(ALLOC A_{unmaskable}(ρ_{a} , ν, env, σ, τ, ρ_{w})))

Lemma 6.6.2 [Soundness of Effect Inference with Full FIX Effect Masking] Extending the type and effect inference system of Section 2.5 to incorporate the Full FIX Effect Masking Rule preserves the soundness of the type and effect inference rules proved by Lucassen [Lucassen 87].

This means, in short, that the type and effect of an expression, as inferred by the type and effect inference rules with full FIX effect masking, is a conservative estimate of the actual type and effect of the expression. As a consequence, the compiler writer can use these rules as a basis for various optimizations of the object code. As mentioned in Section 1.2, the newly incorporated ALLOC masking expands the set of expressions for which the compiler can soundly employ memoization (software caching), stack allocation (and hence automatic garbage collection) of local non-observably allocated temporary values, and common subexpression elimination.

6.7 The Process of Effect Masking

Now that we have considered the information needed in order to perform effect masking, let’s consider how the process of effect masking would interact with the type/effect checking process.

6.7.1 Implementing ALLOC Effect Masking

First, notice that the first term, ρ_{R&W}(τ), of A_{ρ} used in the definition of the ALLOC effect masking operator involves only the regions appearing within the return type of the expression. The second term R&W_{ρ}(ν, env, ρ_{w}), on the other hand, involves the types of the free variables appearing within the expression. As alluded to in the discussion of READ and WRITE effect masking, this concern with free variables is a nuisance since what is free at one level of scope may be bound at an enclosing level (at worst, being globally bound). This is a problem because it suggests that in order to do precise effect masking as we bottom-up return from type/effect checking, we must consider lexical contours, masking the inferred effects accordingly at each contour boundary. This is tedious, although it is desirable to generate precise effect annotations at each node of an expression as we back out so that this local information can be effectively used by the compiler, for instance to perform compile-time concurrency scheduling of value subexpressions.

It is desirable, therefore, to relax this second term, R&W_{ρ}(ν, env, ρ_{w}), when used in the ALLOC effect masking operator. Fortunately, we can. The trick is to note that, in addition to the ALLOC masking operator, the READ and WRITE effect masking operators also mention the types of the free variables. Recall that the troublesome term in the ALLOC operator was concerned with the exposure of allocating a mutable datum via storage into an already exposed mutable datum. This was accomplished (ultimately) by a WRITE effect. Therefore, this sort of exposure of allocation will be reflected in both an ALLOC and a WRITE effect, although probably not over the same region. To capitalize on this insight, reconsider the semantic implications of an ALLOC effect: ALLOC effects indicate that the associated expression cannot be memoized and that the exposed datum cannot be (permanently) stack allocated. Now consider the ramifications of a WRITE effect: the associated expressions cannot be memoized and the value written must be allocated in an appropriate region of the store. The same expression in which the ALLOC occurs will have a WRITE effect. This means not only that the expression cannot be memoized, but that it must be scheduled appropriately to maintain the sequential semantics of the program in which it occurred. This is a far more severe constraint. Moreover, the mutation operator which actually performs the WRITE will certainly arrange for the locally allocated datum to be moved off the stack (if indeed it was allocated there) and migrate it into the appropriate region of memory where it should be stored (perhaps into another region of the stack or into a garbage collected heap).

The upshot of this is that the ALLOC masking process need not pay heed to the term involving R&W_{ρ}(ν, env, ρ_{w}) in the ALLOC masking operator since it is, in effect, subsumed by the WRITE masking operator. This allows ALLOC masking to be performed solely on the basis of the return type of the expression under consideration. This simplification, then, allows the ALLOC masking process to proceed top-down in lockstep with the type/effect checking process, remembering at each successive subexpression those ALLOC effects of locals that appear to have taken place. Upon bottom-up return, the type/effect checker can return not only the type of each subexpression, but it can separate out those regions within the return type which are of interest to the ALLOC masking process. The ALLOC masking process can then perform the mask incrementally at each step out by intersecting the assumed potential ALLOC regions with the returned type’s ρ_{R&W}(τ). This annotates each local ALLOC effect with the desired precision while avoiding filtering the returned ALLOC effect masking information at each lexical level to compensate for internally bound variables. Note that this intersection could be done in O(n) where n is the number of potential ALLOC regions if a sorted list of regions is maintained, for instance as a bit-vector.

6.7.2 Implementing READ and WRITE Effect Masking

Unfortunately, the same trick cannot be played with READ and WRITE effects. For them, the sole concern is with the region occurrences involving free variables. However, again implementing this as a bit-vector could prove effective. The idea is to maintain a mapping from locally bound variables’ binding regions (FV_{ρ}(lvar, env)) and readable & writable component regions (ρ_{R&W}(T (env(lvar)))) to a bit-vector of READ/WRITE occurrences on those regions. This bit-vector would be extended and retracted with each successive lexical level entry and exit. Global READ/WRITEs should not map into this lexical contour bitvector as they would, of course, be non-maskable: they could be maintained in a separate list of known-nonmaskable READ/WRITEs. Of course, if a local variable collides with a global variable in any of its ρ information, then that ρ information will never be maskable so its READ/WRITE entries could be promoted into the known-nonmaskable list, or potentially never placed in the local bit-vector from the outset.

Notice that this does not give READ/WRITE annotation at the level of precision of specific locations or even of specific variable instances. Rather, it propagates information based on the region information embedded within each variable’s type and binding region. This will not be as precise as traditional static analysis of aliasing and sharing information [Banning 78/79] [Barth 77/78] [Rosen 79], but such traditional approaches have been shown to be P-space hard [Weihl 80] or even NP-complete or co-NP-complete [Myers 81]. Using region and effect annotations seems a reasonable trade-off in light of the potential expense of these more aggressive methods. Moreover, using region and effect annotations significantly reduces the sheer engineering effort otherwise necessary to implement a traditional approach [Cooper, Kennedy & Torczon 86].

6.7.3 Consideration of Irreducible Description Applications

One final concern that I have heretofore suppressed is how to treat regions which appear as arguments to parameterized DFUNCs when the kind of the return description is known to be EFFECT or TYPE. Such instances arise, for example, inside the body of a Pλ which is parameterized over a type constructor. Specifically, consider (δ_{ψ} δ_{1} δ_{2} ...) where δ_{ψ} has

kind (DFUNC (TYPE REGION) κ_{rtn}). In the cases where κ_{rtn} is EFFECT or TYPE, it must

be assumed that the region arguments would appear in both ρ_{R} and ρ_{W} of the description application.

Such situations are not as far-fetched as they might at first seem. For example, consider the program fragment below:

(DEFINE make-widget-mapper
        (Pλ ((widgetof (DFUNC (TYPE REGION) TYPE)))
          (Pλ ((τ TYPE) (τ′ TYPE) (ρ REGION) (ρ′ REGION) (ϵ EFFECT))
            (λ ((widget-map (SUBR (MAXEFF (READ ρ)(ALLOC ρ′))
                                  ((SUBR ϵ (τ) τ′)  (widgetof τ ρ))
                                  (widgetof τ′ ρ′))))
              (λ ((widget (widgetof τ ρ))
                  (proc   (SUBR ϵ (τ) τ′)))
                (widget-map proc widget))))))

This implements a procedure polymorphized over a type constructor that, when projected, produces a polymorphic procedure. This polymorphic procedure, when further projected, takes as argument a widget mapper then generates a procedure which, in turn, takes a widget and a procedure and widget-maps the procedure over the widget to produce a fresh new widget. This is quite plausible if, say, one wanted a LIST-MAP, a VECTOR-MAP, a STRING-MAP, etc. Such a generate-mapper construct has been proposed for the next revision of Scheme.^{13} Compiling such a beast in FX-87 would involve this final concern. In general, any polymorphic abstraction over aggregate data constructors raise this issue.

13No, not by me... by Morry Katz. It has received mixed but overall positive response from the Scheme language design community. Such appreciation for orthogonality in language design is a hallmark of Scheme advocates, who extol the virtues of minimality and elegant simplicity.

6.8 Summary of Effect Masking

To summarize, this chapter derived a precise Effect Masking Rule defined in terms of the distinct syntactic classes of region occurrences which one naturally considers when trying to decide if an effect is observable at some point within an expression. This rule is, presumably, more straightforward than the terse rule presented in the FX-87 Manual and it yields more precise results in the sense that it masks effects that the “official” manual masking rule could not. Further, the plausibility of efficiently implementing this more powerful rule was presented. Moreover, since the newly derived rule filters out more irrelevant information than does the former rule— for example, by altogether ignoring argument types within SUBR types— and since it compares only those segments of the collected information which are relevant— for instance, it considers only ρ_{R&W} in ALLOC masking rather than both the complete sets ρ_{R} and ρ_{W}, and the READ and WRITE masking operators consider only one of ρ_{R} or ρ_{W}, respectively— the new masking rule derived here is likely to execute faster than the prescribed rule from the manual. This is clear if one views the effect masking process as using a generate-and-test paradigm where local effects are generated which may later be masked based on the success/failure of the masking test. The improved rule generates fewer initial local effects and it can be accelerated by appropriate data structures to separate the independent mask testing concerns.

Of course, the soundness of the improved Effect Masking Rule has not been formally proved. This is not unexpected since neither has the proposition of soundness of the old rule from the manual ever been formally proved by any of the FX-87 designers. Although this thesis does not address a soundness proof for effect masking, the next section does address a heretofore unanswered concern regarding the soundness of passing mutable structures to procedures which may mutate these arguments’ structure components. Recall that the application rule heretofore accepts any argument whose type is a subtype of the expected type. We will see in the next section that this is not always sound. The application rule is refined accordingly.

6.9 Modulated Type Inclusion

Now that we have addressed the sematics of effects in FX-87 and we have looked at the issue of interference/sharing detection as performed via effect masking, we can return to the issue of effect modulation in the type and effect rule for procedure application [Section 2.5.5]. In short, the issue was that rather than allow the types of the actual arguments of an application to be subtypes of the types declared for the formal parameters when the procedure was defined, we must stipulate inclusion modulated by the latent effect of the operator. This issue is finally put to rest in this section.

6.9.1 The Problem

The imperative minded reader will have, by this point, become concerned with the soundness of performing assignment to components of structured data such as PAIROF and VECTOROF data. The concern is that procedure application has heretofore been presented as if it permitted the arguments to have types which are subtypes of the formals’ declared types. If we view subtyping intuitively as set inclusion on those values approximated by the types, then component mutation of structured arguments raises a subtle soundness issue. Specifically, consider the following figure:

[↓] (REF x @!)        ----------         (REF x @!) [↑]
         |         /     SUPER  \  |

         |      /       ------  \  /
           \ |      /   SUB  \  |    /
            \__|_____|____\/      | \/__|___/
              |     |    / \  | / \ |
              |  \  /      |
                 \  ------       /

                    \  /
                      ----------

Figure 6-1: Structured Data Subtyping

According to the type inclusion axioms [§ 2.4.5], REF [↓] is a subtype of REF [↑] since SUB is a subtype of SUPER. Thus, by the application type checking rule [§ 2.5], we should be permitted to pass a REF [↓] to any procedure which expects an argument of type REF [↑]. Now consider that in general there can be many pointers to a value of type REF [↓]. These other aliases for the same REF will be used by other procedures to manipulate the component of this REF. Type soundness would be lost were it not guaranteed that any mutation to the component of a REF will always be equivalent to or a subtype of the current component’s type. This is as prescribed by the type checking rule for SET. For instance, it would be safe for us to SET the component of a REF [↑] to be a value of type SUB, but it would be unsound to SET the component of a REF [↓] to be a value of type SUPER. Unfortunately, if we pass a REF [↓] to a procedure which expects a REF [↑], and that procedure mutates the cell of the REF passed to it so that the REF afterwards contains a new value of type SUPER, then that procedure will have violated type soundness.

6.9.2 The Solution

The way to remedy this potential problem is to use a more constrained notion of type inclusion when passing structured data as arguments. We need to consider the writable regions in the type of the operator being applied to the structured datum and to modulate our argument inclusion type tests according to the intersection of these operator type ρ_{W}’s and the arguments types’ read/write and structure regions, ρ_{R&W}. This new modulated inclusion we denote as ⊑_{ϵ} (read “is included in, modulo ϵ”).

VDKenv ⊢ υ_{ψ} :  (SUBR ϵ_{ψ} (τ_{χ1} … τ_{χn}) τ_{rtn})  ! ϵ
VDKenv ⊢ υ_{i} : τ_{αi}  ! ϵ
{} ⊢_{⊑} τ_{αi} ⊑_{ϵ_{ψ}} τ_{χi}
VDKenv ⊢ (υ_{ψ} υ_{1} … υ_{n}) : τ_{rtn}

                                      ! (MAXEFF ϵ ϵ_{ψ})

Figure 6-2: Modulated Application Type and Effect Rule

This new modulated inclusion (⊑_{ϵ}) could be defined inductively over the structured types, but for brevity I present here only the rule for REF types. The corresponding modulations for the other structure types are straightforward.

@= ⊑ ρ_{↑} ∨ ¬∃ ρ∈ρ_{W}(ϵ) . ρ ⊑ ρ_{↑}  @= ⋢ ρ_{↑} ∧ ∃ ρ∈ρ_{W}(ϵ) . ρ ⊑ ρ_{↑}
ρ_{↓} ⊑ ρ_{↑}  ρ_{↓} ⊑ ρ_{↑}
τ_{↓} ⊑_{ϵ} τ_{↑}  τ_{↓} ≡ τ_{↑}

 (REF τ_{↓} ρ_{↓}) ⊑_{ϵ} (REF τ_{↑} ρ_{↑})                  (REF τ_{↓} ρ_{↓}) ⊑_{ϵ} (REF τ_{↑} ρ_{↑})

Figure 6-3: Modulated REF Inclusion

The intuition here is that if the argument to an operator which has effect ϵ_{ψ} is expected to be immutable or if the procedure does not mutate any surface components of the REF argument, then it is safe to pass as argument a value whose actual type is a subtype of that expected so long as the component types are likewise safe. If, on the other hand, the argument is expected to be surface mutable and the procedure expects to have the right to surface mutate it, then the component types must be strictly equivalent to the expected component types so they will denote values at least as high in the type inclusion ordering as any new value that we may update them to now contain.

For non-structured types (such as INT, BOOLE, UNIT, NULL, etc.), ⊑_{ϵ} is identical to ⊑. Finally, the application type rule must change, accordingly, to check argument type inclusion as before, but to do so modulated by the operator’s latent effect. In retrospect, we have chosen to maintain inclusion axioms for structured types based solely on an intuitive typesas-sets/subtypes-as-subsets characterization. We subsequently had to hone the application rule to tolerate argument subtyping modulated by the latent effect of the operator. The FX-87 manual, by contrast, chose to develop structure type inclusion modulated solely on the mutability of the region of the structure components, without consideration of whether this is the type of an argument to an operator which actually has a WRITE effect on said region. Such a stance makes the inclusion axioms no longer be based on the intuitive notion of subtypes as subsets. More disturbing, it also permits the application soundness concern to bleed into the subtyping test even when an inclusion test does not involve argument/application inclusion of an operator which has a WRITE effect. This is unsettling since, for instance, two branches of an IF expression may fail to be in inclusion relation under the manual’s axiomatization of inclusion whereas the more perceptive modulated formulation developed here would succeed. This has important implications for the set of programs which FIX will accept as well-types but which a strict manual-prescribed implementation would spuriously reject. Semantically rationalizing the set of programs rejected by a manual-prescribed implementation would therefore be, at best, haphazard.

6.9.3 The Repercussions

To be fair, though, one subtle question does arise from separating effect modulation from the inclusion rules: how does this affect the theory of abductive inference for implicit projection that was developed in Chapter 5? Fortunately, generalizing the theory to account for this effect modulation is relatively straightforward. Implicit projection with effect modulation can still be done in time linear in the number of projection parameter occurrences.

Recall that Implicit projection is an instance of an application, so we can determine the latent effect of the (polymorphic) operator and modulate the abduction according to its ρ_{W}. This injρ(ρ_{W}(ϵ)) we shall call the abduction ρ_{w}, noting that we are really modulating by the region ρ_{w} rather than the whole latent effect of the polymorphic operator (although I will continue to express the abduced inclusion constraints using ⊑_{ϵ} rather than ⊑_{ρ_{W}(ϵ)} for consistency with our derivation of the need for modulation). The abductive transform of the modulated inclusion rules would then be used to direct the abductive inference. For example, the abductive transform of the modulated REF inclusion rule yields the two rules:

      (REF τ_{↓} ρ_{↓}) ⊑ (REF τ_{↑} ρ_{↑})                (REF τ_{↓} ρ_{↓}) ⊑ (REF τ_{↑} ρ_{↑})

If @= ⊑ ρ_{↑} ∨ ¬∃ ρ∈ρ_{W}(ϵ) . ρ ⊑ ρ_{↑}  ρ_{↓} ⊑ ρ_{↑}
Then  τ_{↓} ⊑_{ϵ} τ_{↑}
Else  τ_{↓} ≡ τ_{↑}

Since every abductive transform of an structured data type will involve this kind of conditionalization, it is natural to build the conditionalization directly into the abduction process. In essence, whenever a structured type like REF is abduction matched against another description, one of six cases can arise.

First, they can trivially not match (for instance, if the other description is a PAIROF form) in which case the abduction just fails as before. This is the easy case.

Second, the constraint being abduced could be a lower bounding on some matchvar, that is, our current subproblem could be of the form μ_{i} ⊑_{ϵ} (REF τ ρ), where τ and ρ must be closed descriptions. In this situation, we can merely process the constraint as in the unmodulated abduction algorithm, but we should flag this matchvar as being “interesting” in the sense that once the abduction has completed, we will have to reconcile the final upper and lower bounds against this intermediate modulated constraint. Specifically, if the final upper bound on the matchvar has a region component which does not intersect @= but does intersect some component of the abduction ρ_{w}, then the type components of the final upper and lower bounds must both be equivalent to the type component of the intermediate inclusions encountered throughout the abduction. Rather than bookkeep all the intermediate τ components encountered, we could simply maintain a Boolean toggle with each matchvar that flags whether all intermediate τ components have been equivalent. This is not expensive since we have shown equivalence to be an amortized constant time operation using algorithmic complexity slicing for lazy normalization. This strategy is safe because underlying it is the notion that normal unmodulated abduction can be run but with bookkeeping. When the unmodulated abduction produces a result, the result may be too flexible to be safe with respect to the necessay modulation. The insight is to notice that if the appropriate bookkeeping was done during the abduction, we can merely interate over the modulation-tagged matchvars, testing to see if their final bounds must be further constrained with respect to the abduction ρ_{w}. Fortunately, this further constraining, if necessary, is a monotonic tightening of the abduced constraints, so it will always terminate.

Third, the constraint being abduced could be an upper bounding on some matchvar, that is, our current subproblem could be of the form (REF τ rho) ⊑_{ϵ} μ_{i}, where τ and ρ must be closed descriptions. In this situation, we can again merely process the constraint as in the unmodulated abduction algorithm, flagging the matchvar as being “interesting”. When the abduction has completed, we will have to reconcile the final upper and lower bounds against this intermediate modulated constraint just as before.

Fourth, in the case of set-like descriptions (e.g., , RUNION forms) we could encounter a flexible match constraint, such as ρ ⊑_{ϵ} (RUNION μ_{1} μ_{2} ... μ_{n}) where ρ is closed. Our concern is when such a constraint arose from a structure constraint of the for (REF τ ρ) ⊑_{ϵ} (REF τ′ (RUNION μ_{1} μ_{2} ... μ_{n}) where τ and ρ must be closed but τ′ can itself contain matchvars, and hence can lead to further abduction constraints which should be modulated by the abduction ρ_{w} and the μ_{i}. In the case of unions over types (like RECORDOF forms), the type components do not introduce new contingencies of themselves— it is the region components of the field which give rise to contingency— so abduction can continue without complication. The way to handle unions over regions is to continue optimistically with the assumption that we can permit the inclusion abduction τ ⊑_{ϵ} τ′ rather than a more confining equivalence abduction τ ≡ τ′, but we must take care to remember that this optimistic inclusion is contingent on the modulation between ρ and the matchvars μ_{i}. Once the optimistic abduction has completed, we then must reconcile this optimism. Specifically, for each contingency tagged matchvar, we must check that either one of the matchvars from the original flexible upper bound contains @= or that none of the matchvars intersects the abduction ρ_{w}. If either situation is true, then the optimism was well-founded so the resulting abduced bounds are safe. If, on the other hand, this predication fails, then the component inclusion abductions which were contigent upon the successful modulation must be tightened into equivalence constraints. Notice carefully that this predication depends only on @=, ρ_{w}, and the matchvar’s final upper bounds. This is a strictly local property so no context information need be bookkept. With appropriate bookkeeping during the optimistic inclusion abduction, the set of accrued contingent matchvars can be easily isolated and processed. For example, a dependence graph mapping each contigent region matchvar (or RUNION of region matchvars) to the structure component matches which resulted from the optimistic inclusion could be easily generated during the abduction by creating a simple parent/child structure where each type component of a structure type is considered to be a child of the region component. Note that this must include even those contingent inclusions which did not involve subordinate matchvars. For example, if τ were NULL and τ′ were (PAIROF τ_{?} τ′_{?}) in the above example, subsequent recognition that the optimistic inclusion was unfounded must result in subsequent abduction failure by noticing the NULL¬ ≡ (PAIROF τ_{?} τ′_{?}). Again, this failure/success of equivalence could be precomputed on fully closed constraints to avoid reprocessing of the abduction traversal. Once the optimistic abduction has completed, again all tagged matchvars could be tested for modulation. Upon detecting that any contingency RUNION ultimately violates the optimistic modulation, a transitive closure of the parent/child dependence graph must be traversed to force all subordinate constraints to be forced to equivalence, being mindful of the precomputed success/failure of closed component equivalence.

The fifth situation is when two closed descriptions are being abductively compared. As already detailed, both the modulated inclusion and the equivalence should be tested and the results of each incorporated into the surrounding bookkeeping environment, assuming bookkeeping has been initiated by some ancester region matchvar.

Sixth, and finally, matching a closed description against a non-closed description in which the contingent ancestor region nevertheless is closed is not problematic. Since both corresponding ancestor regions are closed, the modulation can be computed immediately. It has already been argued that this merely involves two intersection tests over normalized region descriptions.

6.9.4 The Upshot

To summarize, with an appropriate bookkeeping mechanism engaged during an optimistic non-modulated abduction traversal, an optimistic set of abduced constraints can be generated. If this set of constraints is indeed a solution [Definiton 5.2.2], then the modulation can be enforced expost facto by verifying the optimistic modulations against the solution constraints, tightening over-optimistic constraints by following the contingency dependency graph generated during the optimistic traversal. This does not affect the afore derived running time of the abduction process, so we conclude that Implicit Projection with effect modulation can still be performed in time linear in the number of projection parameter (matchvar) occurrences.

Bibliography

[Abelson & Sussmans 85] Harold Abelson and Gerald Jay Sussman with Julie Sussman Structure and Interpretation of Computer Programs (Fifth Printing) (The MIT Electrical Engineering and Computer Science Series) The MIT Press, 1985

[Abelson, Halfant, Katzenelson & Sussman 88] Harold Abelson, Matthew Halfant, Jacob Katzenelson and Gerald Jay Sussman The Lisp Experience Annual Reviews in Computer Science, Vol.3, 1988, pp.167–195

[Aho, Hopcroft & Ullman 74] Alfred V.Aho, John E.Hopcroft, and Jeffrey D.Ullman The Design and Analysis of Computer Algorithms Addison-Wesley, 1974

[Aho & Ullman 86] Alfred V.Aho and Jeffrey D.Ullman Compilers: Principles, Techniques and Tools Addison-Wesley, 1986

[Arvind & Culler 86] Arvind and David E. Culler Dataflow Architectures Annual Reviews of Computer Science, Vol.1, 1986, pp.225–253

[Banning 78/79] John P.Banning An Efficient Way to Find the Side Effects of Procedure Calls and the Aliases of Variables In Proc. ACM POPL 1979, pp.29–41, as condensed from A Method for Determining the Side Effects of Procedure Calls Ph.D. Thesis, Stanford University Report No.213, Stanford Linear Accelerator Center, Aug 78.

[Barendregt 84] H.P.Barendregt The Lambda Calculus: Its Syntax and Semantics [Revised Edition] Studies in Logic and Foundations of Mathematics Vol.103, Elsevier Science Publishing Company, 1984

[Barnes 80] J.G.P.Barnes An Overview of Ada Software — Practice and Experience, Vol.10, Jul 1980, pp.851–887

[Barth 77/78] Jeffrey M.Barth A Practical Interprocedural Data Flow Analysis Algorithm In CACM Vol.21 No.9, Sept. 1978, pp.724–736, as condensed from A Practical Interprocedural Data Flow Analysis Algorithm and its Application Ph.D. Thesis, CS TR No.770520, UC Berkeley, May 1977

[Barth & Nikhil 89] Paul S.Barth and Rishiyur Sivaswami Nikhil Supporting State-Sensitive Computation in a Dataflow System MIT CSG Memo 294, Mar 1989

[de Bruijn 72] N.G.de Bruijn Lambda Calculus Notation with Nameless Dummies, A Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem In Proc. Akademie van Wetenschappen, Series A: Mathematical Sciences, Vol.75, pp.381–392, or Indag. Math., Vol.34, 1972, pp.381–392

[Burstall & Lampson 84/88] R.Burstall and B.Lampson A Kernel Language for Modules and Abstract Data Types DEC SRC TR No.1, Sept 1984

[Cardelli 84/85/86] Luca Cardelli Amber Tech. Memo 11271-840924-10TM, AT&T Bell Laboratories, Murray Hill, NJ, Sept 1984 or In Proc. Treizième Ecole de Printemps d’Informatique Théorique, Le Val D’Ajol, Vosges (France), May 1985, pp.1–27 or Combinatorics and Functional Programming Languages, Lecture Notes in Computer Science No.242, Springer-Verlag, 1986, pp.21–40 [Cardelli 84/88]

Luca Cardelli A Semantics of Multiple Inheritance In Semantics of Data Types, Lecture Notes in Computer Science No.173, Springer-Verlag, Jun 1984, pp.301–315 or Information and Computation, Vol.76 Nos.2/3, Feb/Mar 1988, pp.138–164 (Updated)

[Cardelli & Wegner 85] Luca Cardelli and Peter Wegner On Understanding Types, Data Abstraction, and Polymorphism ACM Computing Surveys, Vol.17 No.4, Dec 1985, pp.471–522

[Cardelli 86] Luca Cardelli A Polymorphic λ-calculus with Type:Type DEC SRC TR No.10, May 1986

[Cardelli 87] Luca Cardelli Typechecking Dependent Types and Subtypes In Proc. Workshop on Foundations of Logic and Functional Programming, Trento, Italy, Dec 1986, Lecture Notes in Computer Science No.306, Springer-Verlag, 1986, pp.45–57

[Cardelli 88] Luca Cardelli Structural Subtyping and the Notion of Power Type (Extended Abstract) In Proc. ACM POPL 1988, pp.70–79

[Cardelli 89] Luca Cardelli Typeful Programming DEC SRC TR No.45, May 1989

[Cardelli 90em] Luca Cardelli Private electronic mail correspondence 5 Mar 1990 [Chien & Dally 90]

Andrew A.Chien and William J.Dally Concurrent Aggregates (CA) In Proc. ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Mar 1990, pp.186–197, and Experience with Concurrent Aggregates (CA): Implementation and Programming In Proc. Distributed Memory Computers Conference, Apr 1990, both as condensed from Concurrent Aggregates (CA): An Object-Oriented Language for Fine-Grained Message-Passing Machines Ph.D. Thesis, MIT AI-TR-1248, Sept 1990

[Church 51] Alonzo Church The Calculi of Lambda-Conversion Annals of Mathematical Studies Vol.6, Princeton University Press, 1951

[Cleaveland & Uzgalis 77] J.Craig Cleaveland and Robert C.Uzgalis Grammars for Programming Languages Programming Language Series No.4, Elsevier Computer Science Library, 1977

[Cook, Hill & Canning 90] William R.Cook, Walter L.Hill, and Peter S.Canning Inheritance is Not Subtyping In Proc. ACM POPL 1990, pp.125–135

[Cooper, Kennedy & Torczon 86] Keith D.Cooper, Ken Kennedy, and Linda Torczon The Impact of Interprocedural Analysis and Optimization in the R^{n} Programming Environment In ACM TransPLaS, Vol.8 No.4, Oct. 1986, pp.491–523

[Coucelle 83] B.Coucelle Fundamental Properties of Infinite Trees In Theoretical Computer Science, Vol.25 No.2, Mar 1983, pp.95-169

[Day 87] Mark S. Day Effects Considered Ineffectual, or Loss of Concurrency in FX Internal Memo MIT PSRG, 1987

[Eastman & Laird 87] Kevin Eastman and Peter Laird with Dave Sim and Steve Lavigne Teenage Mutant Ninja Turtles: Book III First Publishing, Inc. 1987 [Field & Harrison 88]

Anthony J.Field and Peter G.Harrison Functional Programming (International Computer Science Series) Addison-Wesley, 1988

[Fischer & LeBlanc 88] Charles N.Fischer and Richard J.LeBlanc, Jr. Crafting A Compiler The Benjamin/Cummings Publishing Company, Inc., 1988

[Fuh & Mishra 88] You-Chin Fuh and Prateek Mishra Type Inference with Subtypes In Proc. ESOP ’88, Lecture Notes in Computer Science No.300, Springer-Verlag, Mar 1988, pp.94–114, reprinted in Theoretical Computer Science, Vol.73 No.2, Jun 1990, pp.155–175

[Geschke, Morris & Satterwaite 77] Charles M.Geschke, James H.Morris Jr., and Edwin H.Satterwaite Early Experience with Mesa In CACM Vol.20 No.8, Aug 1977, pp.540–553

[Gifford & Lucassen 86] David K.Gifford and John M.Lucassen Integrating Functional and Imperative Programming In Proc. 1986 ACM Conference on Lisp and Functional Programming, Aug 1986, pp.28–38

[Gifford et al. 87] David K.Gifford, Pierre Jouvelot, John M.Lucassen, and Mark A.Sheldon FX-87 Reference Manual MIT/LCS/TR-407, Sept 1987

[Goldfarb 81] W.D.Goldfarb The Undecidability of the Second-Order Unification Problem Theoretical Computer Science No.13, 1981, pp.225-230

[Habermann 73] A.N.Habermann Critical Comments on the Programming Language Pascal In Acta Informatica, Vol.3, 1973, pp.47–57

[Halfant & Sussman 87/88] Matthew Halfant and Gerald Jay Sussman Abstraction in Numerical Methods MIT AI Memo 997, Oct 1987, or In Proc. ACM Conference on Lisp and Functional Programming, Jul 1988, pp.1–7 [Harper & Mitchell 87]

Robert Harper and Kevin Mitchell Introduction to Standard ML Computer Science Department, University of Edinburgh, Sept 1986

[Hewitt 69] Carl Hewitt Planner: A Language for Proving Theorems in Robotics In Proc. IJCAI, Washington D.C., 1969, pp.295–301

[Hoare 69] C.A.R.Hoare An Axiomatic Basis for Computer Programming In CACM Vol.12 No.10, Oct 1969, pp.576–580,583

[Hopcroft 71] John E.Hopcroft “An n lg n algorithm for minimizing states in a finite automaton” in Theory of Machines and Computations P.Kohavi and A.Paz (editors) Academic Press, 1971, pp.189–196

[Hopcroft & Ullman 79] John E.Hopcroft and Jeffrey D.Ullman Introduction to Automata Theory, Languages, and Computation Addison-Wesley, 1979

[IEEE 90] IEEE Scheme Standardization Committee Draft Standard for the Scheme Programming Language IEEE Document No.P1178/D4, Mar 1990

[Jouvelot 88] Pierre Jouvelot Towards a proposal for array operations in FX Internal Memo of MIT PSRG, Aug 1988

[Jouvelot & Gifford 88] Pierre Jouvelot and David K.Gifford The FX-87 Interpreter In Proc. IEEE Int. Conf. on Comp. Lang., Oct 1988, pp.65–72

[Jouvelot & Gifford 89a] Pierre Jouvelot and David K.Gifford Reasoning about Continuations with Control Effects MIT/LCS/TM-378, or In Proc. ACM SIGPLAN PLDI, Jun 1989, pp.218–226 [Jouvelot & Gifford 89b]

Pierre Jouvelot and David K.Gifford Communication Effects for Message-Based Concurrency MIT/LCS/TM-386, Feb. 1989

[Kathail 89] Vinod Kathail An optimal interpreter for the λ-calculus Notes from a talk presented at The MIT Dataflow Workshop, Nov 2, 1989

[Knuth 86] Donald E.Knuth The TEXbook Addison-Wesley Publishing Company, 1986

[Kowalski 79] Robert Kowalski Algorithm = Logic + Control In CACM Vol.22 No.7, Jul 1979, pp.424–436

[Lamport 86] Leslie Lamport LaTEX: A Document Preparation System Addison-Wesley Publishing Company, 1986

[Lampson & Burstall 88] B.Lampson and R.Burstall Pebble, A Kernel Language for Modules and Abstract Data Types Information and Computation, Vol.76 No.2/3, Feb/Mar 1988, pp.278–346

[Levy 80] J.J.Levy Optimal reduction in the lambda calculus In To H.B.Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism J.R.Hindley and J.P. Seldin (editors) Academic Press, 1980

[Lieberman & Hewitt 83] Henry Lieberman and Carl Hewitt A Real-Time Garbage Collector Based on the Lifetimes of Objects In CACM Vol.26 No.6, Jun 1983, pp.419–429

[Liskov et al. 79] Barbara Liskov et al. CLU Reference Manual MIT/LCS/TR-225, 1979 or Lecture Notes in Computer Science No.114, Springer-Verlag, 1981 [Lucassen 87]

John M.Lucassen Types and Effects: Towards the Integration of Functional and Imperative Programming Ph.D. Thesis, MIT/LCS/TR-408, Aug 1987

[Lucassen & Gifford 88] John M.Lucassen and David K.Gifford Polymorphic Effect Systems In Proc. ACM POPL 1988, pp.47–57

[McAllester 89] Dave A.McAllester ONTIC: A Knowledge Representation System for Mathematics (The MIT Press Series in Artificial Intelligence) The MIT Press, 1989

[McCracken 79] Nancy McCracken An Investigation of a Programming Language with a Polymorphic Type Structure Ph.D. Thesis, Syracuse University, Jun 1979

[McCracken 84] Nancy McCracken The Typechecking of Programs with Implicit Type Structure In Semantics of Data Types. Lecture Notes in Computer Science No.173, Springer-Verlag, Jun 1984, pp.301–315

[MacLennan 87] Bruce J.MacLennan Principles of Programming Languages: Design, Evaluation, and Implementation [2nd Edition] CBS College Publishing, 1987

[Meyer & Reinhold 86] Albert R.Meyer and Mark B.Reinhold ‘Type’ Is Not a Type: Preliminary Report In Proc. ACM POPL 1986, Jan 1986, pp.287–295

[Milner 78] Robin Milner A Theory of Type Polymorphism in Programming In Journal of Computer and System Sciences 17, 1978, pp.348–375

[Milner 84] Robin Milner A Proposal for Standard ML In Proc. 1984 ACM Symposium on Lisp and Functional Programming, Aug 1984, pp.184–197 [Mitchell 81]

Tom M.Mitchell Generalization as Search In Readings in Artificial Intelligence, Bonnie Lynn Webber and Nils J.Nilson (Editors) Morgan Kaufman Publishers, Inc., 1981, pp.517–542

[Myers 81] Eugene W.Myers A Precise Inter-Procedural Data Flow Algorithm In Proc. ACM POPL 1981, pp.219–230

[Naur 63] Peter Naur (Editor) Revised Report on the Algorithmic Language ALGOL 60 In CACM Vol.6 No.1, Jan 1963, pp.1–20

[Nielson 86] Flemming Nielson Abstract Interpretation of Denotational Definitions (A survey) In STACS ’86, Lecture Notes in Computer Science 210, Springer-Verlag, 1986, pp.1–20

[Nielson 87/88] Flemming Nielson Strictness Analysis and Denotational Abstract Interpretation (Extended Abstract) In Proc. ACM POPL 1987, Jan 1987, pp.120–131, as condensed from Information and Computation, Vol.76 No.1, Jan 1988, pp.29–92.

[O’Toole & Gifford 89] James William O’Toole Jr. and David K.Gifford Type Reconstruction with First-Class Polymorphic Values MIT S.M. Thesis, MIT/LCS/TM-380, or In Proc. ACM SIGPLAN PLDI, Jun 1989, pp.207–217

[Park 76] David Park Finiteness is μ-Ineffable Theoretical Computer Science No.3, pp.173–181

[Peyton-Jones 87] Simon L.Peyton-Jones The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science) Prentice Hall, 1987

[Pfenning 88] Frank Pfenning Partial Polymorphic Type Inference and Higher-Order Unification In Proc. 1988 ACM Conference on Lisp and Functional Programming, Jul 1988, pp.153–163 [Popek, Horning & London 77]

G.J.Popek, J.J.Horning and R.L.London Notes on the Design of Euclid In SIGPLAN Notices, Vol.12 No.3, Mar 1977, pp.11–18

[Pratt 84] Terrence W.Pratt Programming Languages: Design and Implementation [2nd Edition] Prentice Hall, Inc., 1984

[Rees & Clinger 86] Jonathan Rees and William Clinger (Editors) Revised^{3} Report on the Algorithmic Language Scheme MIT/AI/Memo 848a or Indiana University CS/TR 174 or ACM SIGPLAN Notices, Vol.21 No.12, Dec 1986

[Reinhold 88] Mark B.Reinhold Typechecking Is Undecidable When ‘Type’ Is a Type MIT S.M. Thesis, MIT/LCS/TR-458, December 1989.

[Reynolds 74] John C.Reynolds Towards a Theory of Type Structure In Proc. Colloque sur la Programmation, Lecture Notes in Computer Science No.19, Springer-Verlag 1974, pp.408–425

[Rosen 79] Barry K.Rosen Data Flow Analysis for Procedural Languages In JACM Vol.26 No.2, Apr 1979, pp.322–344

[Roylance 87/88] Gerald L.Roylance Expressing Mathematical Subroutines Constructively MIT AI Memo No.999, Nov 1987, or In Proc. 1988 ACM Conference on Lisp and Functional Programming, Jul 1988, pp.8– 13

[Sheldon 89] Mark Sheldon Static Dependent Types for First-Class Modules MIT S.M. Thesis, MIT/LCS/TR-472, December 1989, or In Proc. 1990 ACM Conference on Lisp and Functional Programming, Jun 1990, pp.20– [Shivers 88]

Olin Shivers Control Flow Analysis in Scheme In Proc. ACM SIGPLAN PLDI 1988, pp.164–174

[Snyder 86] Alan Snyder Encapsulation and Inheritance in Object-Oriented Programming Languages In Proc. ACM OOPSLA ’86, Sept 1986, pp.38–45

[Steele 85] Guy L.Steele Jr. Common Lisp: The Language Digital Press, 1984

[Tarjan 83] Robert Endré Tarjan Data Structures and Network Algorithms Chapter 2 (Disjoint Sets) Society for Industrial and Applied Mathematics, 1983

[Wand & O’Keefe 89] Mitchell Wand and Patrick O’Keefe On the Complexity of Type Inference with Coercion In Proc. ACM/IFIP Functional Programming Languages and Computer Architecture, 1989, pp.293–298

[Ward & Halstead 89] Stephen A. Ward and Robert H. Halstead, Jr. Computation Structures The MIT Electrical Engineering and Computer Science Series The MIT Press, 1990

[Weihl 80] William E.Weihl Interprocedural Data Flow Analysis in the Presence of Pointers, Procedure Variables, and Label Variables (Extended Abstract) In Proc. ACM POPL 1980, pp.83–94, as condensed from MIT/LCS/TR-247, Jan. 1980

[Wirth 71] Niklaus Wirth The Programming Language Pascal In Acta Informatica, Vol.1, 1971, pp.35–63

[van Wijngaarden et al. 76] Aad van Wijngaarden et al. Revised Report on the Algorithmic Language ALGOL 68 Springer-Verlag, 1976, pp.103–107 [XLRG 81]

The Xerox Learning Research Group The Smalltalk-80 System BYTE, Vol.6 No.8, Aug 1981, pp.36–48

[Yelick 85] Kathy A.Yelick A Generalized Approach to Equational Unification MIT S.M. Thesis, MIT/LCS/TR-344, Aug 1985