Challenges in Type Systems Research

Martin Odersky University of Karlsruhe

Type systems are one backbones of programming language design and implementation. Current research addresses questions in fields as diverse as mathematical logic, program analysis, and human factors engineering. Some of the future challenges for the field are: increasing the expressiveness of typed programming languages, broadening the information carried by types, and making type systems amenable to user definition and customization.

Over the last 20 years, type systems have developed into a backbone of programming language research. Research in the area was driven to a large degree by the desire to combine the flexibility of dynamically typed languages with the security and early error detection potential of statically typed languages. By and large this goal has been met. The polymorphic type systems of modern programming languages are sufficiently flexible for most programming tasks. At the same time their ability to detect errors early has led to considerable improvements in the productivity and quality of the programming task.

Research in type systems is interesting because it combines several areas of computer science and neighboring fields. The foundation of type systems is in mathematical logic, where theorems and types are related by the Curry-Howard isomorphism. Mathematical logic continues to be an inspiration. An example is Girard’s linear logic[3], which is now the foundation of many resource-conscious type systems. Type system research also has large overlaps with static program analysis. Strictness analysis, binding time analysis and many others have alternative formulations as type systems or as abstract interpretations. The type-systematic formulations often have the advantage that they allow better communication with the programmer, since they offer a convenient formalism to attach information to program terms. Information can flow from the programmer to the compiler via type annotations, or from the compiler to the programmer as the result of type reconstruction. With type systems being progressively more expressive and flexible, the concise representation of type annotations has become more difficult. Hence we expect type system design to have an increasingly strong human factors aspect. For instance, we would like to have better ways of communicating type errors to the programmer, perhaps by exploring typings interactively.

The development in type systems is far from complete. On the one hand, there is the challenge to statically type difficult program constructs that now still require

1ACM Workshop on Strategic Directions in Computing Research, June 1996, ACM Computing Surveys 28(4es). Permission to copy without fee all or part of this material is granted, provided that the copies are not made for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission.

2 · Martin Odersky

run-time type checks. As a side effect, this quest often leads to a better understanding of the “hard to type” constructs[2], witnessed by the successful work on typing object oriented languages.

On the other hand, we would like to further refine the possible sets of values characterized by a type. For instance, we would like to extend information about functions from the types of arguments and results to the side-effects performed and exceptions raised[4]. To a certain theoretical degree this extension is straightforward, at least in the absence of higher-order constructs, but it raises challenging problems before it can be applied practically. The problems are a combination of human factors (how do we represent these types concisely?) and type reconstruction (how do we relieve the programmer from the need to give too much information explicitly?).

Even if these challenges are met, another problem remains: The resulting type systems risk being large and complex due to the highly diverse information they capture. An inspiration for a solution might again come from mathematical logic: Type systems might evolve to meta-languages that can be specified by a programmer. This is analogous to the progression from theorem provers over a fixed logic to logical frameworks where the underlying logic is specifiable. Eventually such an approach might lead to flexible program development tools that allow the program designer to specify the relevant static program properties. Unlike in program verification one would not aim for complete program correctness, but would settle for properties that are efficiently verifiable without programmer interaction. Even so, it can be expected that such an approach could lead to a further significant reduction in program errors.

Before we can achieve such lofty goals however, there is a more immediate concern to ensure continued support for the field: So far, modern type systems have been applied only in “exotic” programming languages, at least as seen from a mainstream perspective. Eventually, the results obtained in the context of these languages must be made available to a wider audience. We can best achieve this goal by making a modern typed language such as ML[1] mainstream, but such a leap is probably beyond the power of the type systems community alone. So one should also look into how type-systematic ideas might be adapted to more conventional languages, either in the form of language extensions or as add-on verification tools.

Finally, it is also necessary to promote the teaching of type systems and type theory to make the concepts accessible to a large audience. While the Backus-Naur notation for context-free syntax has been commonplace for a long time, the equally important role of type systems for the description of a language’s context-dependent syntax has not yet been sufficiently appreciated.

REFERENCES

[1] Andrew W. Appel and David B. MacQueen. Standard ML of New Jersey. In J. Maluszyński and M. Wirsing, editors, Programming Language Implementation and Logic Programming, pages 1–13. Springer-Verlag, August 1991. Lecture Notes in Computer Science 528.

[2] Kim Bruce, Luca Cardelli, Guiseppe Castagna, The Hopkins Objects Group, Gary T.Leavens, and Benjamin Pierce. On binary methods. Theory and Practice of Object Systems, 1(3), 1996.

[3] Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[4] Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. In Seventh Annual

Challenges in Type Systems Research · 3

IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 162–173, Los Alamitos, California, June 1992. IEEE Computer Society Press.