A maximum-flow approach to anomaly isolation in unification-based incremental type inference

ABSTRACT

A crucial aspect of a program intended for general use is its behavior in the presence of erroneous inputs. For instance, much attention has been devoted to the problems of error detection, reporting, and correction in compilers^1,2. As programming languages and systems based in one way or another on unification³ become more common, it becomes increasingly important to develop a theory of error detection and correction for unification-based systems. We report here on a language-based editor for a variant of ML⁴ that uses a novel approach to the isolation of likely causes of user errors. As the user edits and manipulates his or her program, unification is incrementally applied to determine its type correctness. If a type inconsistency arises, a maximum flow technique is applied to the set of type equations to determine the most likely source of error. In this way a determination can be made as to the relative strengths with which the set of type equations asserts multiple contradictory hypotheses. In a language such as ML, the type of an object is inferred from patterns of usage. Often it is the case that most uses of a given object are mutually consistent, whereas one or a very small number of uses conflict with the general usage pattern. In MOE (ML-Oriented Editor), if it is possible to discern that such a situation has arisen, likely errors are highlighted at high intensity and all other program components that contributed to the inferred type of the object are highlighted at a lower intensity. In providing error information to the user, two principles are observed:(1) Error indications should be complete but parsimonious; the user should see highlighted on the screen everything that contributed directly to an error, but nothing. more,(2) The user's attention should be drawn to what appear to be the anomalies that are responsible for errors.Language-based editors permit a new level of quality in the process of helping users when inputs are, for one reason or another, invalid. Unification-based type inference in language-based editors appears to have been first considered by Meertens 5. Snelting and Bahlke have more recently also explored this approach.

REFERENCES

• 1: Fischer, Charles N., Donn R. Milton, and Jon Mauney, "A locally least-cost LL(1) error corrector," Tech. Report #371, University of Wisconsin (August 1979).
• 2: Susan L. Graham , Charles B. Haley , William N. Joy, Practical LR error recovery, ACM SIGPLAN Notices, v.14 n.8, p.168-175, August 1979
• 3: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 4: Milner, R., "A theory of type polymorphism in programming," <i>Journal of Computer and System Sciences</i> <b>17</b>(1978).
• 5: Lambert Meertens, Incremental polymorphic type checking in B, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.265-275, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567092]
• 6: Rolf Bahlke , Gregor Snelting, The PSG - Programming System Generator, Proceedings of the ACM SIGPLAN 85 symposium on Language issues in programming environments, p.28-33, June 25-28, 1985, Seattle, Washington, United States
• 7: Thomas Reps , Tim Teitelbaum , Alan Demers, Incremental Context-Dependent Analysis for Language-Based Editors, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.3, p.449-477, July 1983 [doi>10.1145/2166.357218]
• 8: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.165-174, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800528]
• 9: C. N. Fischer , Gregory F. Johnson , Jon Mauney , Anil Pal , Daniel L. Stock, The Poe language-based editor project, Proceedings of the first ACM SIGSOFT/SIGPLAN software engineering symposium on Practical software development environments, p.21-29, April 1984
• 10: Alberto Martelli , Ugo Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.2, p.258-282, April 1982 [doi>10.1145/357162.357169]
• 11: Donald E. Knuth, The art of computer programming, volume 1 (3rd ed.): fundamental algorithms, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1997
• 12: Cardelli, Luca, "Basic polymorphic typechecking," Technical report, AT&amp;T Bell Laboratories (1984).