19.3 Nominal and Structural Type Systems

 < Free Open Study > 



19.3 Nominal and Structural Type Systems

Before proceeding with the formal definition of FJ, we should pause to examine one fundamental stylistic difference between FJ (and Java) and the typed lambda-calculi that are the main focus in this book. This difference concerns the status of type names.

In previous chapters, we have often defined short names for long or complex compound types to improve the readability of examples, e.g.:

   NatPair = {fst:Nat, snd:Nat}; 

Such definitions are purely cosmetic: the name NatPair is a simple abbreviation for {fst:Nat,snd:Nat}, and the two are interchangeable in every context. Our formal presentations of the calculi have ignored abbreviations.

By contrast, in Java, as in many widely used programming languages, type definitions play a much more significant role. Every compound type used in a Java program has a name, and, when we declare the type of a local variable, a field, or a method parameter, we always do so by giving the name. "Bare" types like {fst:Nat,snd:Nat} simply cannot appear in these positions.

These type names play a crucial role in Java's subtype relation. Whenever a new name is introduced (in a class or interface definition), the programmer explicitly declares which classes and interfaces the new one extends (or, in the case of a new class and an existing interface, "implements"). The compiler checks these declarations to make sure that the facilities provided by the new class or interface really extend those of each super-class or super-interface-this check corresponds to record subtyping in a typed lambda-calculus. The subtype relation is now defined between type names as the reflexive and transitive closure of the declared immediate-subtype relation. If one name has not been declared to be a subtype of another, then it is not.

Type systems like Java's, in which names are significant and subtyping is explicitly declared, are called nominal. Type systems like most of the ones in this book, in which names are inessential and subtyping is defined directly on the structures of types are called structural.

Nominal type systems have both advantages and disadvantages over structural presentations. Probably the most important advantage is that the type names in nominal systems are useful not only during typechecking, but at run time as well. Most nominal languages tag each run-time object with a header word containing its type name, represented concretely as a pointer to a run-time data structure describing the type and giving pointers to its immediate supertypes. These type tags are handy for a variety of purposes, including run-time type testing (e.g., Java's instanceOf test and downcasting operation), printing, marshaling data structures into binary forms for storage in files or transmission over networks, and reflective facilities that permit a program to dynamically investigate the fields and methods of an object that it has been given. Run-time type tags can also be supported in structural systems (see Glew, 1999; League, Shao, and Trifonov, 1999; League, Trifonov, and Shao, 2001; and the citations given there), but they constitute an additional, separate mechanism; in nominal systems, the run-time tags are identified with the compile-time types.

A less essential, but pleasant, property of nominal systems is that they offer a natural and intuitive account of recursive types-types whose definition mentions the type itself. (We will discuss recursive types in detail in Chapter 20.) Such types are ubiquitous in serious programming, being required to describe such common structures as lists and trees, and nominal type systems support them in the most straightforward possible way: referring to List in the body of its own declaration is just as easy as referring to any other type. Indeed, even mutually recursive types are straightforward. We view the set of type names as being given from the beginning, so that, if the definition of type A involves the name B and the definition of B refers to A, there is no issue about "which is defined first." Of course, recursive types can also be handled in structural type systems. Indeed, high-level languages with structural typing, such as ML, generally "bundle" recursive types with other features, so that, for the programmer, they are just as natural and easy to use as in nominal languages. But in calculi intended for more foundational purposes, such as type safety proofs, the mechanisms required to deal rigorously with recursive types can become rather heavy, especially if mutually recursive types are allowed. The fact that recursive types come essentially for free in nominal systems is a decided benefit.

Another advantage of nominal systems is that checking whether one type is a subtype of another becomes almost trivial. Of course, the compiler must still do the work of verifying that the declared subtype relations are safe, which essentially duplicates the structural subtype relation, but this work needs to be done only once per type, at the point where it is defined, rather than during every subtype check. This makes it somewhat easier to achieve good performance in typecheckers for nominal type systems. In more serious compilers, though, it is not clear that the difference between nominal and structural styles has much effect on performance, since well-engineered typecheckers for structural systems incorporate representation techniques that reduce most subtype checks to a single comparison-see page 222.

A final advantage often cited for explicit subtype declarations is that they prevent "spurious subsumption," where the typechecker fails to reject a program that uses a value of one type where a completely different, but structurally compatible, type is expected. This point is more contentious than the ones above, since there are other-arguably better-ways of preventing spurious subsumption, for example using single-constructor datatypes (page 138) or abstract data types (Chapter 24).

Given all these advantages-especially the general usefulness of type tags and the simple treatment of recursive types-it is no surprise to find that nominal type systems are the norm in mainstream programming languages. The research literature on programming languages, on the other hand, is almost completely concerned with structural type systems.

One immediate reason for this is that, at least in the absence of recursive types, structural systems are somewhat tidier and more elegant. In a structural setting, a type expression is a closed entity: it carries with it all the information that is needed to understand its meaning. In a nominal system, we are always working with respect to some global collection of type names and associated definitions. This tends to make both definitions and proofs more verbose.

A more interesting reason is that the research literature tends to focus on more advanced features-in particular, on powerful mechanisms for type abstraction (parametric polymorphism, abstract data types, user-defined type operators, functors, etc.)-and on languages such as ML and Haskell that embody these features. Unfortunately, such features do not fit very comfortably into nominal systems. A type like List(T), for example, seems irreducibly compound-there will be just one definition somewhere in the program for the constructor List, and we need to refer to this definition to see how List(T) behaves, so we cannot treat List(T) as an atomic name. A few nominal languages have been extended with such "generic" features (Myers, Bank, and Liskov, 1997; Agesen, Freund, and Mitchell, 1997; Bracha, Odersky, Stoutamire, and Wadler, 1998; Cartwright and Steele, 1998; Stroustrup, 1997), but the results of such extensions are no longer pure nominal systems, but somewhat complex hybrids of the two approaches. Designers of languages with advanced typing features thus tend to favor the structural approach.

A full account of the relation between nominal and structural type systems remains a topic of ongoing research.



 < Free Open Study > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net