Browse Books

Reviewer: David B. Benson

In Robin Milners famous phrase, “well-typed programs cannot go wrong.” In more detail, programming languages with a type inference and checking system based on type unification are widely recognized as significantly enhancing the creation of correct code without heroics, either in proving or testing. Type system design for programming languages has attempted to balance effectiveness and accuracy with intuitive behavior and sufficient flexibility of the type system. These latter goals have led to languages that not only include parametric polymorphism in the type system, but also have qualified types. Two programming languages with qualified type systems are Haskell and Gofer. The type systems for both of these languages are discussed in this monograph, based on the authors Ph.D. thesis at Oxford University. In a qualified type system, there are implications, not just statements about what the types are. Here is an example. The expression == :: Eq aaa Bool states that the equality operator (==) is polymorphic over the type variable a , but only for those types satisfying the predicate Eq. For these types, the equality operator has parametric polymorphic type aa Bool . The intention is that the equality operator only makes sense for concrete types that can support an equality operation. One may then specify that Int satisfies Eq and additionally specify the runtime primitive operator for runtime equality checking on entities of type Int. The concrete type Int Int does not have a meaningful notion of runtime equality checking, however, so it is not specified as satisfying Eq. A qualified type system is said to support operator overloading. Languages with parametric polymorphism, but without qualified types, have an elegant type inference algorithm [1]. An important problem for languages with qualified types is to create a type inference algorithm that balances effectiveness, accuracy, intuitive behavior, and flexibility. The approach taken in this monograph uses a concept called evidence. This approach is shown to incorporate techniques previously used in the implementation of type inference and checking systems. Chapter 5 is devoted to showing that qualified type systems with evidence have the important property of coherence. That is, the meaning of a term does not depend upon the particular type checking algorithm. Chapter 6 is less rigorously formal than the previous chapter, concentrating on features that might prove useful in practical compilers that have qualified types. This leads nicely into chapter 7, which discusses some implementation techniques, called HTC, for use with the Haskell qualified type system. Chapter 8 presents the type system used in Gofer: This chapter describes GTC, an alternative approach to the use of type classes that avoids the problems associated with context reduction, while retaining much of the flexibility of HTC. In addition, GTC benefits from a remarkably clean and efficient implementation that does not require sophisticated compile-time analysis or transformation. As in the previous chapter we concentrate more on implementation details than on formal properties of GTC. An early description of GTC … was used as the basis for Gofer, a small experimental system based on Haskell. …The two languages are indeed very close, and many programs that are written with one system in mind can be used with the other with little or no changes. On the other hand, the underlying type systems are slightly different: Using explicit type signature declarations it is possible to construct examples that are well typed in one but not in the other. Moreover, I am under the distinct impression that Goferites strongly prefer their language, that it has certain advantages in writing good code, and that the new Haskell standard will adopt portions of the type class examples in Gofer. This short review is not an appropriate place to explicate the subtle differences between Haskell and Gofer. Instead, I encourage you to read this exemplar of computer science research and the appropriate presentation thereof. The writing is excellent, the typesetting is perfect, and the extremely fine point that Jones has made will encourage scholarly contemplation about the nature of type systems.