Resumé
ResuméThe thesis is an impressively broad and deep piece of work developing the fundamental theory of explicit dynamic typing, with applications to static debugging and innovative compilation of run-time typed programming languages such as Scheme.
Statically and dynamically typed programming languages have been taken to be opposites of each other, trading off expressiveness and programming convenience (dynamically typed languages) against safety, modularity and efficiency (statically typed languages). The early 90's, however, have seen the advent of so-called soft typing systems, which seek to combine the benefits of dynamically and statically typed systems without inheriting their disadvantages. Dynamic typing as a type discipline is one of these systems.
In the dynamic typing discipline all the otherwise implicit run-time tagging and checking operations are made explicit as type operations that generate and consume run-time tagged values. Once these (run-time type) coercions are made explicit one can reason about them and optimize them, with the ultimate goal of eliminating them wherever possible, though without requiring that they all be eliminable as in conventional statically typed languages. The coercions, however, have to be inferred automatically since they are normally not provided in the source program as written by a programmer. Thus the task of type inference, as known from languages such as Standard ML, CAML, Haskell or Miranda, is generalized to one of inferring program completions with types and coercions in such a fashion that the result contains as few coercions as possible and that those occur in good'' places only.
Reasoning about coercions is captured formally by rules of type inference, equational theories for semantic equivalence of different completions, and oriented transformations (p-reduction) for improving one completion into a better'' one.
The thesis takes work by the supervisor on monomorphic dynamic typing as point of departure, and generalizes and expands it in several directions. In particular, the results that are either new or break new ground are:
S A thorough recasting of Thatte's quasi-static typing in terms of dynamic typing (Chapter 3): The results show that best'' completions exist, are unique and can be computed efficiently if the types of function parameters are fixed and cannot be changed. At a deeper level they also highlight that the expressive power and all the theoretical and algorithmic problems of dynamic typing are due to its flexibility of letting the types of parameters vary'' freely.
S The development of a general theory of coercion equivalence with sum, error and recursive types based on the theory of categorical co-products, where the initial and the terminal object in the category are identified (Chapter 4).
S Establishment of confluence for p-reduction (Chapter 2) and its normalization in various completion classes (Chapter 5): This shows that best'' completions in a certain, precise sense exist in dynamic typing. The technical problems the author addresses here are extremely hard. In these two chapters he develops new reduction-theoretic tools and answers almost all the questions I had left open (or, frankly, simply couldn't solve) previously.
S A polymorphic type system with coercion parameters that extends ML (also called Hindley-Milner'') polymorphism and generalizes both monomorphic dynamic typing and the soft typing systems developed at Rice University (Chapter 6): Here the major novelty lies in Jakob's analysis of the conflicting goals of safety and minimality of polymorphic completions in all contexts, necessitating the inclusion of coercion parameters in the polymorphic type system.
S Design and analysis of two dynamic type systems for IEEE Standard Scheme, with particular care paid to practically important issues such as the imperative features of Scheme (Chapter 7): This applies the basic theory developed in the previous chapters to an existing real-world language (with all its warts''). It is also the basis of a prototype Scheme-to-SML translator that demonstrates the essence of dynamic type inference based compilation.
On a more general level, the author of the thesis effuses solid scholarship: he draws on and crosslinks his work with the relevant literature, as evidenced by his ample bibliography and careful references. He carefully follows scientific discipline by carefully stating his goals, making his assumptions explicit, and analyzing the problem at hand without making a priori and ad hoc restrictions. He uses precise language, both in the expository presentation and in the mathematical formulation of the technical material in the speciale.
The benefits of the work's scholarliness to the scientific community and to any interested reader are that his speciale is firmly placed in the context of current state-of-the-art knowledge, it sheds and clarifies new insight gained, not only new results, and, last but not least, it substantially advances the state of knowledge on the integration of statically and dynamically typed programming languages.
This does not mean that the speciale is an easy read, simply because it covers a lot of material both in breadth and depth, and both conceptually and technically. Since no stone is left unturned everything is mathematically precisely formulated and no nontrivial proof is left undone it requires a lot of concentration on the reader's behalf. The presentation is very coherent and reflects a systematic mind that identifies, analyzes and then seeks to solve the heart of a problem. As such the speciale is also relentlessly concise, drawing on and bringing in, as needed, required background knowledge from type theory, type inference (incl. type-based program analysis), term rewriting theory, category theory, operational and denotational semantics, the semantics of Scheme and knowledge of Standard ML, and without much mention that a fundamental understanding of logic, algorithms and data structures is implicitly assumed.
The author covers the background material only as far as is needed in the context of his work and relies on the reader to either know that material to start with or to look up the literature he refers to. At 230 pages of concise writing the author has too much to say about dynamic typing to include tutorial material on background tools and results. If ease of reading with emphasis on tutorial features for a broad audience is the main criterion for awarding the prize of best speciale of the year 1995, then the thesis isn't it. But if it is impressive scholarship, new ideas and new results both in breadth and depth, then the thesis is enthusiastically recommended for the prize.
Vejleder: Lektor Fritz Henglein, DIKU