Chapter 6
Type Systems

In D, if we evaluate the expression

3 + (If False Then 3 Else False),

we will get some kind of interpreter-specific error at runtime. If D had a type system, such an expression would not have been allowed to evaluate.

In Lisp, if we define a function

(defun f (x) (+ x 1)),

and then call (f "abc"), the result is a runtime type error. Similarly, the Smalltalk expression

String new myMessage

results in a “message not supported” exception when run. Both of these runtime errors could have been detected before runtime if the languages supported static type systems.

The C++ code

int a[10]; a[123] = 5;

executes unknown and potentially harmful effects, but the equivalent Java code will throw an ArrayIndexOutOfBoundsException at runtime, because array access is checked by a dynamic type system.

These are just a few examples of the kinds of problems that type systems are designed to address. In this chapter we discuss such type systems, as well as algorithms to infer and to check types.

6.1 An Overview of Types

A type is simply a property with which a program is implicitly or explicitly annotated before runtime. Type declarations are invariants that hold for all executions of a program, and can be expressed as statements such as “this variable always holds a String object,” or “this function always returns a tree expression.”

Types have many other advantages besides simply cutting down on runtime errors. Since types (and module signatures) specify invariant properties of the program, they serve as precise and descriptive comments on the functionality of the code. In this manner, types aid in large software development.

With a typed language, more information is known at compile-time, and this helps the compiler produce much faster code. For example, the record implementation we will use in our DSR compiler (via hashing, see Chapter 7) is not needed in C++ due to its static type system. We know the size of all records at compile-time, and therefore know where they should be laid out in memory. In contrast, Smalltalk is very slow, and the lack of a static type system counts for much of the slowness. The Strongtalk system [7] attempts to bring a static type system into Smalltalk.

Finally, in an untyped language its easier to do very ugly “hacking”. For instance, a list [1;true;2;false;3;true] can be written in an untyped language, but this is dangerous and it would be much preferred to represent this as [(1,true);(2,false);(3,true)], which, in Caml, has the type (int * bool) list.

However, untyped languages have one distinct advantage over typed ones: they are more expressive. For example, consider the DSR encoding of DOB from Chapter 5. This encoding would not work with Caml as the target language, because the Caml type system disallows record polymorphism. The Y -combinator is another example of where an untyped language really shines. D could support recursion via the Y -combinator, but a simple typed version of D can’t since it cannot be typed. Recall from Section 2.3.5 that Caml can not type the Y -combinator, either.

All of us have seen types used in many ways. The following is a list of some of the more common dimensions of types.

• Atomic types: int, float, ...
• Type constructors, which produce types from types: 'a -> 'b, 'a * 'b
• Caml-style type constructor definitions via type
• C-style type definitions via struct and typedef
• Object-oriented types: class types, object types
• Module types, or signatures
• Java-style interfaces
• Exception types: <method> throws <exception>
• Parametric polymorphism: 'a -> 'a
• Record/Object polymorphism: pass a ColorPoint to a function which expects a Point.

There are also several newer dimensions of types that are currently active research areas.

• Effect types: the type “int -x,y-> int” indicates that variables x and y will assigned to in this function. Java’s throws clauses for methods are a form of effect types.
• Concrete class analysis: for variable x:Point, a concrete class analysis produces a set such as {Point, ColorPoint, DataPoint}. This means at runtime x could either be a Point, a ColorPoint, or a DataPoint (and, nothing else). This is useful in optimization.
• Typed Assembly Language [2, 17]: put types on assembly-level code and have a type system that guarantees no unsafe pointer operations.
• Logical assertions in types: int -> { x:int | odd(x) } for a function returning odd numbers.

There is an important distinction that needs to be made between static and dynamic type systems. Static type systems are what we usually mean when we talk about type systems. A static type system is the standard notion of type found in C, C++, Java and Caml. Types are checked by the compiler, and type-unsafe programs fail to compile.

Dynamic type systems, on the other hand, check type information at runtime. Lisp, Scheme, and Smalltalk are, in fact, dynamically typed. In fact, D and DSR are technically dynamically typed as well, since they will raise a typeMismatch when the type of an expression is not what it expects. Any time you use a function, the runtime environment makes sure that its a function. If you use an integer, it makes sure it’s an integer, etc. These runtime type checks add a lot of overhead to the runtime environment, and thus cause programs to run slowly.

There is some dynamic typechecking that occurs in statically typed languages too. For instance, in Java, downcasts are verified at run-time and can raise exceptions. Out-of-bounds array accesses are also checked at run-time in Java and Caml, and are thus dynamically typed. Array accesses are not typed in C or C++, since no check is performed at all. Note that the type of an array (i.e. int, float) is statically checked, but the size is dynamically checked.

Finally, languages can be untyped. The DSR compiler produces untyped code, since runtime errors cause core dumps. It is important to understand the distinction between an untyped language and a dynamically typed one. In an untyped language there is no check at all and anomalous behavior can result at runtime. In Chapter 7, we compile DSR to untyped C code, using casts to “disable” type system. Machine language is another example of an untyped language.

To really see the difference between untyped and dynamically typed languages, consider the following two program fragments. The first is C++ code with the type system “disabled” via casts.

The code compiles with no errors, but when we run it the output is “ã¿.” But if we compile it with optimization, the result is “Ãà.” Run it on a different computer and it may result in a segmentation fault. Use a different compiler, and the results may be completely exotic and unpredictable. The point is that because we’re working with an untyped language, there are no dynamic checks in place, and meaningless code like this results in undefined behavior.

Contrast this behavior with that of the equivalent piece of Java code. Recall that Java’s dynamic type system checks the type of the object when a cast is made. We will use approximately the same code:

When we run this Java code, the behavior is quite predictable.

The ClassCastException is an exception raised by Java’s dynamic type system. The unsafe code is never executed in Java, and so the behavior of the program is consistent and well-defined. With the C++ version, there is no dynamic check, and the unsafe code is executed, resulting in wild and unexpected behavior.

6.2 TD: A Typed D Variation

We will use the prefix “T” to represent a typed version of a language which we have previously studied. Thus we have several possible languages: TD, TDS, TDS, TDSR, TDOB, TDX, TDSRX, etc. There are too many languages to consider individually, so we will first look at TD as a warm-up, and then consider full-blown TDSRX.

6.2.1 Design Issues

Before we begin to investigate TD or any typed language, there are a few general design issues to address. We will take a moment to discuss these issues before giving the specification for TD.

The first question to ask is how much explicit type information must our language contain? How much type information must the program be decorated with, and how much can be inferred by the compiler? A spectrum of possibilities exists.

On one end of the spectrum, we can use no decoration at all. We simply stick to our untyped language syntax, and let the compiler infer all the type information.

Alternatively, we can use limited decoration, and have the compiler do partial inference. There is a wide range of possibilities. C for instance requires function argument and return types to be specified, and declared variables to be given types. However, within the body of a function, individual expressions do not need to be typed as those types may be inferred. Some languages only require function argument types be declared, and the return values of functions is then inferred.

At the other end of the spectrum, every subexpression and its identifier must be decorated with its type. This is too extreme, however, and makes the language unusable. Instead of writing

Function x -> x + 1,

we would need some gross syntax like

(Function x -> (x:int + 1:int):int):(int -> int).

For TD and TDSRX, we will concentrate on the C and Pascal view of explicit type information. We specify function argument and return types, and declared variable types, and allow the rest to be inferred.

We should also illustrate the difference between type checking and type inference. In any typed language, the compiler should typecheck the program before generating code. Type inference algorithms infer types and check that the program body has no type errors. Caml is an example of this.

A type checker generally just checks the body is well-typed given the types listed on declarations. This is how C, C++, and Java work, although technically they are also inferring some types, such as the type of 3+4.

In any case it must be possible to run the type inference or type checking algorithm quickly. Caml in theory can take exponential time to infer types, but in practice it is linear.

6.2.2 The TD Language

Finally, we are ready to look at TD, a typed D language. To simplify things, we will not include the Let Rec syntax of D, but only non-recursive, anonymous functions. We will discuss typing recursion in Section 6.4.

In analogue with our development of operational semantics and interpreters, we will define two things when discussing types. First we define type systems, which are language-independent notations for assigning types to programs. Type systems are analogous to operational semantics. Secondly, we define type checkers, which are Caml implementations of type systems analogous to interpreters. We begin with type systems.

Type Systems

Type systems are rule-based formal systems that are similar to operational semantics. Type systems rigorously and formally specify what program have what types, and have a strong and deep parallel with formal logic (recall our discussion of Russell’s Paradox in Section 2.3.5). Type systems are generally a set of rules about type assertions.

The TD types in the concrete syntax are

Tau ::= Int | Bool | Tau -> Tau.

We can represent this in a Caml abstract syntax as

The expressions of TD are almost identical to those of D, except that we must explicitly decorate functions with type information about the argument. For example, in the concrete syntax we write

Function x:Tau -> e

where the abstract syntax representation is

The TD Type Rules

We are now ready to define the TD types rules. These rules have the same structure as the operational semantics rules we have looked at before; the horizontal line reads “implies.” The following three rules are the axioms for out type system (recall that an axiom is a rule that is always true, that is, a rule with nothing above the line).

The Hypothesis rule simply says that if a variable x contained in a type environment Gamma has type Tau then the assertion Gamma|-x : Tau is true. The Int and Bool rules simply give types to literal expressions such as 7 and False. These rules make up the base cases of our type system.

Next, we have rules for simple expressions.

These rules are fairly straightforward. For addition and subtraction, the operands must typecheck to Ints, and the result of the expression is an Int. Equality is similar, but typechecks to a Bool. Note that equality will only typecheck with integer operands, not boolean ones. The And, Or, and Not rules are similar, and their definition should be obvious.

The If rule is a bit more complicated. Clearly, the conditional part of the expression must typecheck to a Bool. But what about the Then and Else clauses. Consider the following expression.

If e Then 3 Else False

Should this expression typecheck? If e evaluates to True, then the result is 3, an Int. If e is False, the result is False, a Bool. Clearly, then this expression should not typecheck, because it does not always evaluate to the same type. This tells us that for an If statement to typecheck, both clauses must typecheck to the same type, and the type of the entire expression is then the same as the two clauses. The rule is as follows.

We have now covered all the important rules except for functions and application. The Function rule is a bit different from other rules, because functions introduce new variables. The type of the function body depends on the type of the variable itself, and will not typecheck unless that variable is in Gamma, the type environment. To represent this in our rule, we need to perform the type assertion with the function’s variable appended to the type environment. We do this in the following way.

Notice the use of the type constructor -> to represent the type of the entire function expression. This type constructor should be familiar, as the Caml type system uses the same notation. In addition, the Function rule includes the addition of an assumption to Gamma. We assume the function argument, x, is of type Tau, and add this assumption to the environment Gamma to derive the type of e. The Application rule follows from the Function rule:

Just as in operational semantics, a derivation of Gamma|-e : Tau is a tree of rule applications where the leaves are axioms (Hypothesis, Int or Bool rules) and the root is Gamma|-e : Tau.

Let’s try an example derivation.

Given the above and letting

we then have

As we mentioned before, TD is a very weak language. No recursive functions can be defined. In fact, all programs are guaranteed to halt. TD is thus normalizing. Without recursion, TD is not very useful. Later we will add recursion to TDSRX and show how to type it.

Now that we have a type system for the TD language, what can we do with it. We can detect whether or not our programs are well-typed, but what does it mean if they are. The answer comes in the form of the following type soundness theorem.

We will not precisely define the concept of a stuck state. It is basically a point at which evaluation can not continue, such as 0 (Function x -> x) or (Function x -> x) + 4. In terms of a D interpreter, stuck stated are the cases that raise exceptions. This theorem asserts that a type system prevents runtime errors from occurring. Similar theorems are the goal of most type systems.

6.3 Type Checking

To write an interpreter for TD, we simply modify the D interpreter to ignore type information at runtime. What we are really interested in is writing a type checker. This is the type system equivalent of an interpreter; given the language-independent type rules, define a type checking algorithm in a particular language, namely Caml.

A type-checking algorithm typeCheck, takes as input a type environment Gamma and expression e as and either return its type, Tau, or raises an exception indicating e is not well-typed in the environment Gamma.

Some type systems do not have an easy corresponding type-checking algorithm. In TD we are fortunate in that the type checker mirrors the type rules in a nearly direct fashion. As was the case with the interpreters, the outermost structure of the expression dictates the rule that applies. The flow of the recursion is that we pass the environment Gamma and expression e down, and return the result type Tau back up.

Here is a first pass at the TD typechecker, typecheck : envt * expr -> dtype. Gamma can be implemented as a (ide * dtype) list, with the most recent item at the front of the list.

This Lemma implies the typecheck function is a sound implementation of the type system for TD.

6.4 Types for an Advanced Language: TDSRX

Now that we’ve looked at a simple type system and type checker, let us move on to a type system for a more complicated language: TDSRX. We include just about every piece of syntax we have used up to now, except for DOB’s classes and objects and DV’s variants. Here is the abstract syntax defined in terms of a Caml type.

Next, we will define the type rules for TDSRX. All of the TD type rules apply, and so we can move directly to the more interesting rules. Let’s begin by tackling recursion. What we’re really typing is the In clause, but we need to ensure that the rest of the expression is also well-typed.

Next, we move on to records and projection. The type of a record is simply a map of the field names to the types of the values associated with each field. Projection is typed as the type of the value of the field projected. The rules are

We’ll also need to be able to type side effects. We can type Ref expressions with the special type Tau Ref. Set and Get expressions easily follow.

Finally, the other kind of side effects we need to type are exceptions. To type an exception itself, we will simply use the type Exn. This allows all exceptions to be typed in the same way. For example, the code

If b Then (#IntExn 1) Else (#BoolExn False)

will typecheck, and has type Exn. We do this to allow maximum flexibility.

Because they alter the flow of evaluation, Raise expressions should always typecheck, provided the argument typechecks to an Exn type. It is difficult to know what type to give a raise expression, though. Consider the following example.

If b Then Raise (#Exn True) Else 4

This expression should typecheck to type Int. From our If rule, however, we know that the Then and Else clause must have the same type. We infer, therefore, that the Raise expression must have type Int for the If to typecheck. In Section 6.6.2 we see how to handle this inference automatically. For now, we will simply type Raise expressions with the arbitrary type Tau. Note that this is a perfectly valid thing for a type rule to do, but it is difficult to implement in an actual typechecker.

Next, notice that the With clause of the Try expression is very much like a function. Just as we did with functions, we will need to decorate the identifier with type information as well. However, as we see below, this decoration can be combined with the final kind of type decoration, which we will discuss now.

Consider the expression

The type of this expression is clearly Int. But suppose the example were modified a bit.

This expression will also type to Int. But suppose we were to evaluate the expression using our operational semantics for exceptions. When the exception is raised, False will be substituted for x, which could cause a runtime type error. The problem is that our operational semantics is ignorant of the type of the exception argument.

We can solve this problem without changing the operational semantics, however. Suppose, instead of writing #Ex False, we wrote #Ex@Bool False. The @Bool would be used by the type rules to verify that the argument is indeed a Bool, and the interpreter will simply see the string “#Ex@Bool”, which will be used to match with the With clause. This also eliminates the need for type decoration on the With clause identifier, since it serves the same purpose. In a sense, this is very much like overloading a method in Java or C++. When a method is overloaded, the type and the method name are needed to uniquely identify the correct method. Our final exception syntax looks like this:

This expression typechecks and has type Int. When evaluated, the result is Raise #Ex@Bool False, i.e. the exception is not caught by the With clause. This is the behavior we want.

Now that we’ve got a type-friendly syntax worked out, let’s move on to the actual type rules. They are fairly straightforward.

Using these rules, let’s type the expression from above:

Therefore, by the Try rule, we deduce the type Int for the original expression.

6.5 Subtyping

The type systems that we covered above are reasonably adequate, but there are still many types of programs that have no runtime errors that will nonetheless not typecheck. The first extension to our standard type systems that we would like to consider is what is known as subtyping. The main strength of subtyping is that it allows record and object polymorphism to typecheck.

Subtypes should already be a familiar concept from Java and C++. Subclasses are subtypes, and extending or implementing an interface gives a subtype.

6.5.1 Motivation

Let us motivate subtypes with an example. Consider a function

Function x:{l:Int} -> (x.l + 1):Int.

This function takes as an argument a record with field l of type Int. In the untyped DR language the record passed into the function could also include other fields besides l, and the call

(Function x -> x.l + 1) {l = 4; m = 6}

would generate no run-time errors. However, this would not type-check by our TDSRX rules: the function argument type is different from the type of the value passed in.

The solution is to re-consider record types such as {m:Int; n:Int} to mean a record with at least the m and n fields of type Int, but possibly other fields as well, of unknown type. Think about the previous record operations and their types: under this interpretation of record typing, the Record and Projection rules both still make sense. The old rules are still sound, but we need a new rule to reflect this new understanding of record types:

This rule is valid, but it’s not as good as we could do. To see why, consider another example,

F = Function f -> f ({x=5; y=6; z=3}) + f({x=6; y=4}).

Here the function f should, informally, take a record with at least x and y fields, but also should accept records where additional fields are present. Let us try to type the function F.

F : ({x:Int; y:Int} -> Int) -> Int

Consider the application F G for

G = Function r -> r.x + r.x.

If we were to typecheck G, we would end up with G : {x:Int} -> Int, which does not exactly match F’s argument, {x:Int; y:Int} -> Int, and so typechecking F G will fail even though it does not cause a runtime error.

In fact we could have given G a type {x:Int; y:Int} -> Int, but its too late to know that was the type we should have used back when we typed G . The Sub-Rec₀ rule is of no help here either. What we need is a rule that says that a function with a record type argument may have fields added to its record argument type, as those fields will be ignored:

Using this rule, F G will indeed typecheck. The problem is that we still need other rules. Consider records inside of records:

{pt = {x=4; y=5}; clr = 0} : {pt:{x:Int}; clr:Int}

should still be a valid typing since the y field will be ignored. However, there is no type rule allowing this typing either.

6.5.2 The STD Type System: TD with Subtyping

By now it should be clear that the strategy we were trying to use above can never work. We would need a different type rule for every possible combination of records and functions!

The solution is to have a separate set of subtyping rules just to determine when one type can be used in the place of another. Tau <: Tau' is read “Tau is a subtype of Tau',” and means that an object of type Tau may also be considered an object of type Tau'. The rule added to the TD type system is

We also need to make our subtyping operator reflexive and transitive. This can be accomplished with the following two rules.

Our rule for subtyping records needs to do two things. It needs to ensure that if a record B is the same as record A with some additional fields, then B is a subtype of A. It also needs to handle the case of records within records. If B’s fields are all subtypes of A’s fields, then B should also be a subtype of A. We can reflect this concisely in a single rule as follows.

The function rule must also do two things. If functions A and B are equivalent except that B returns a subtype of what A returns, then B is a subtype of A. However, if A and B are the same except that B’s argument is a subtype of A’s argument, then A is a subtype of B. Simply put, for a function to be a subtype of another function, it has to take less and give more. The rule should make this clear:

From our discussions and examples in the previous section, it should be clear that this more general set of rules will work.

6.5.3 Implementing an STD Type Checker

Automated typechecking of STD is actually quite difficult. There are two ways to make the task easier. The first is to add more explicit type decoration to help the typechecker. The second it to completely infer the types in a constraint form, a topic covered in Section 6.7.

Here, we briefly sketch how the typecheck function for STD may be written. The TD typechecker requires certain types to be identical, for example, the function domain type must be identical to the type of the function argument in an application e e'.

In STD at this point, we need to see if subtyping is possible. typecheck(e') returns Tau'' and then Tau'' <: Tau is checked via a function areSubtypes(Tau'',Tau). This produces a valid proof by the Sub rule. Other rules where the TD rules require a type match similarly are generalized to allow the Sub rule to be used.

6.5.4 Subtyping in Other Languages

It it interesting to see how subtyping is used in other languages. Consider, for example, Java and C++. In these languages, subclassing is the main form of subtyping. A subclass is a subtype of the class from which it extends. In Java, a class is also a subtype of any interfaces it implements.

Java and C++ are thus more restrictive. Suppose there were classes with structure {x:Int; y:Int; color:Int} and {x:Int; y:Int} that weren’t one of the two cases above (that is, the prior is not a subclass of the latter, and the two share no common interface). The two classes, then, are not subtypes in Java or C++, but they are in STD. Declared subtyping has the advantage, however, that subtype relationships do not have to be completely inferred.

OCaml objects are more flexible in that there is no restriction to a hierarchy, but it’s also less flexible in that there is really no object polymorphism-- an explicit coercion of a ColorPoint to a Point is required. There are several research languages with type inference and subtyping, but the types are often complex or hard to read [8].

6.6 Type Inference and Polymorphism

Type inference was originally discovered by Robin Milner, the original creator of ML, and independently by the logician J. Roger Hindley. The key idea of Milner’s “Algorithm W” is to initially give all variables arbitrary types, 'a, and then to unify or equate the types, if indicated by the program. For example, if the application f x has type 'a -> 'b and x has type 'c, we may equate 'a and 'c.

We will look at full type inference, that is, type inference on programs with no explicit type information.

6.6.1 Type Inference and Polymorphism

Type inference goes hand-in-hand with parametric polymorphism (often called “generic types”). Consider the function Function x -> x. Without polymorphism, what type can be inferred for this function? Int -> Int is a flawed answer, because the function could be used in a context where it is passed a boolean. With type inference we need to achieve something called a principal type.

What principality means is no other typing will let more uses of the program typecheck, so the principal typing will always be best. The desired property of our type inference algorithm is that it will always infer principal types. An important corollary is that with a principal-type algorithm, we know inference will never “get in the way” of the programmer by, for example, inferring Bool -> Bool for the identity function when the programmer wants to use it on Int -> Int.

Caml infers the type 'a -> 'a for the identity function, which can be shown to be a principal type for it. In fact, Caml type inference always infers principal types.

6.6.2 An Equational Type System: ED

We are going to present type inference in a nonstandard way. Milner’s “Algorithm W” eagerly unifies 'a and 'c: it replaces one with the other everywhere. We will present equational inference, in which we lazily accumulate equations like 'a = 'c, and then solve the system of equations at the end of the algorithm.

We will study ED, a simple, equationally typed version of D. ED uses the same grammar for expressions as the D language did, since ED does not have any type decorations. The ED types are

Tau ::= Int|Bool|Tau -> Tau|'a|'b|...

ED types during inference are going to include an extra set of constraining equations, E, which constrain the behavior of the type variables. Type judgments for ED are thus of the form Gamma|-e : Tau\E, the same as before but tacking a set of equations on the side. Each member of E is an equation like 'a = 'c. Equational types will be used to aid inference. Here is an outline of the overall approach.

1. Infer equational types for the whole programs.
2. If the equations are inconsistent, pronounce that there is a type error.
3. If the equations are consistent, simplify them to give an inferred type.

It is a fact that if there are no inconsistencies in the equations, they can always be simplified to give an equation-free type.

Each Tau = Tau' is an equation on types, meaning Tau and Tau' have the same meaning as types. We will let E mean some arbitrary set of type equations. For instance,

Int -> 'a\{'a = Int -> 'a1,'a1 = Bool}

is an equational type. If you think about it, this is really the same as the type

Int -> Int -> Bool.

This is known as equation simplification and is a step we will perform in our type inference algorithm. It is also possible to write meaningless types such as

Int -> 'a\{'a = Int -> 'a1,'a = Bool}

which cannot be a type since it implies that functions and booleans are the same type. Such equation sets are deemed inconsistent, and will be equated with failure of the type inference process. There are also possibilities for circular (self-referential) types that don’t quite look inconsistent:

Int -> 'a\{'a = Int -> 'a }

Caml disallows such types, and we will also disallow them initially. These types can’t be simplified away, and that is the main reason why Caml disallows them: users of the language would have to see some type equations.

The ED Type Rules

The ED system is the following set of rules. Note that Gamma serves the same role as it did in the TD rules. It it a type environment that binds variables to simple (non-equational) types. Our axiomatic rules look much like the TD rules.

The rules for +, -, and = also look similar to their TD counterparts, but now we must take the union of the equations of each of the operands to be the set of equations for the type of the whole expression, and add an equation to reflect the type of the operands.

The And, Or, and Not rules are defined in a similar way. The rule for If is also similar to the TD If rule. Notice, though, that we do not immediately infer a certain type like we did in the previous rules. Instead, we infer a type 'd, and equate 'd to the types of the Then and Else clauses.

Finally, we are ready for the function and application rules. Functions no longer have explicit type information, but we may simply choose a type 'a as the function argument, and include it in the equations later. The application rule also picks a 'a type, and adds an equation with 'a as the right hand side of a function type. The rules should make this clear.

These rules almost directly define the equational type inference procedure: the proof can pretty much be built from the bottom (leaves) on up. Each equation added denotes two types that should be equal.

Solving the Equations

One thing that should be immediately clear from the ED type rules is that any syntactically correct program may be typed by these rules. Whether or not a program is well-typed is not determined until we actually solve the system of equations in the equational type of the entire program. The ED type rules are really just accumulating constraints.

Solving the equations involves two steps. First we compute the closure of the equations, producing new equations that hold by transitivity, etc. Next, we check for any inconsistent equations, such as Int = Bool that denote type errors.

The following algorithm computes the equational closure of set E.

• For each equation of the form Tau₀ -> Tau₀' = Tau₁ -> Tau₁' in E, add Tau₀ = Tau₁ and Tau₀' = Tau₁' to E.
• For each set of equations Tau₀ = Tau₁ and Tau₁ = Tau₂ in E, add the equation Tau₀ = Tau₂ to E (by transitivity).
• Repeat (1) and (2) until no more equations can be added to E.

Note that we will implicitly use the symmetric property on these equations, and so there is no need to add Tau₁ = Tau₀ for every equation Tau₀ = Tau₁.

The closure serves to uncover inconsistencies. For instance,

directly uncovering the inconsistency Int = Bool.

The closure of E can be computed in polynomial time. After computing the closure, the constraints are consistent if

1. No immediate inconsistencies are uncovered, such as Int = Bool, Bool = Tau -> Tau', or Int = Tau -> Tau'.
2. No self-referential equations exits (we will deal with this issue shortly).

If the equations are consistent, the next step is to solve the equational constraints. We do this by substituting type variables with actual types. The algorithm is as follows. Given Tau\E,

1. Replace some type variable 'a in Tau with Tau', provided 'a = Tau' or Tau' = 'a occurs in E and either
   • Tau' is not a type variable, or
   • Tau' is a type variable 'b which lexographically succeeds 'a.
2. Repeat (1) until no more such replacements are possible.

Notice that step (1) considers the symmetric equivalent of each equation, which is why we didn’t include them in the closure. The algorithm has a flaw though: the replacements may continue forever. This happens when E contains a circular type. Recall the example of a self-referential type

Int -> 'a\{'a = Int -> 'a}.

Trying to solve these constraints results in the nonterminating chain

The solution is to check for such cycles before trying to solve the equations. The best way to do this it to phrase the problem in graph-theoretical context. Specifically, we define a directed graph G in which the nodes are the the type variables in E. There is an directed edge from 'a to 'b if 'a = Tau is an equation in E and 'b occurs in Tau.

We raise a typeError if there is a cycle in G for which there is at least one edge representing a constraint that isn’t just between type variables (’a = ’b).

In summary, our entire ED type inference algorithm is as follows. For expression e,

1. Produce a proof of |-e : Tau\E by applying the ED type rules. Such a proof always exists.
2. Extend E by computing its closure.
3. Check if E is immediately inconsistent. If so, raise a typeError.
4. Check for cycles in E using the above algorithm described above. If there is a cycle, raise a typeError.
5. Solve E by the above equation solution algorithm. This algorithm will always terminate if there are no cycles in E.
6. Output: the solution type Tau' for e produced by the solution algorithm.

The proof of this theorem is beyond the scope of this book.

Let’s conclude with an example of the type inference algorithm in action. Suppose we want to infer the type of the expression

(Function x -> If x Then 3 Else 4) False

First we produce the following proof.

Given the proof of

we compute the closure of the set of equations to be

{'a = Bool,Int = 'b,'a -> 'b = Bool -> 'c,'b = 'c,Int = 'c}

The set is not immediately inconsistent, and does not contain any cycles. Therefore, we solve the equations. In this case, Tau contains only 'a, and we can replace 'a with Int. We output Int as the type of the expression, which is clearly correct.

6.6.3 PED: ED with Let Polymorphism

After all our work on ED, we still don’t have polymorphism, we only have type variables. To illustrate this, consider the function

Let x = Function y -> y In Function x -> (x True); (x 0)

Recalling our encoding of Let as a function, this expression is equivalent to

(Function x -> (x True); (x 0)) (Function y -> y)

In Caml, such programs typecheck fine. Different uses of Function y -> y can have different types. Consider what ED would do when typing this expression, though.

But when we compute the closure of this equational type, we get the equation Int = Bool! What went wrong? The problem in this case is that each use of x in the body used the same type variable 'a. In fact, when we type Function y -> y, we know that 'a can be anything, so for different uses, 'a can be different things. We need to build this intuition into our type system to correctly handle cases like this. We define such a type system in PED, which is ED with Let and Let-polymorphism.

PED has a special Let typing rule, in which we allow a new kind of type in Gamma:  forall 'a₁...'a_n. Tau. This is called a type schema, and may only appear in Gamma. An example of a type schema is  forall 'a. 'a -> 'a. Note that the type variables 'a₁...'a_n are considered to be bound by this type expression.

The new rule for Let is

where Tau' is a solution of |-e : Tau\E using the above algorithm, and Tau' has free type variables 'a₁...'a_n that do not occur in Gamma.

Notice that since we are invoking the simplification algorithm in this rule, it means the full algorithm is not the clean 3-pass infer-closure-simplify form give above: the rules need to call close-simplify on some sub-derivations.

We also need to add an axiom to ensure that a fresh type variable is given to each Let usage. The rule is

where R(Tau') is a renaming of the variables 'a₁...'a_n to fresh names. Since these names are fresh each time x is used, the different uses won’t conflict like above.

It will help to see an example of this type system in action. Let’s type the example program from above:

Let x = Function y -> y In (x True); (x 0)

We have

|-Function y -> y : 'a -> 'a\{}

This constraint set trivially has the solution type 'a -> 'a. Thus, we then typecheck the Let body under the assumption that x has type  forall 'a.'a -> 'a.

x :  forall 'a.'a -> 'a|-x : 'b -> 'b\{}

by the Let-Inst rule. Then

x :  forall 'a.'a -> 'a|-x True : 'c\{'b -> 'b = Bool -> 'c}

Similarly,

x :  forall 'a.'a -> 'a|-x 0 : 'e\{'d -> 'd = Int -> 'e}

The important point here is that this use of x gets a different type variable, 'd, by the Let-Inst rule. Putting the two together, the type is something like

which by the Let rule then produces

Since 'b and 'd are different variables, we don’t get the conflict we got previously.

6.7 Constrained Type Inference

There was a reason why we presented Hindley-Milner type inference in the form above: if we replace equality constraints by subtyping constraints, <:, we can perform constrained type inference. To understand why it is useful to perform this generalization, it is easiest to just look at the rules.

D is not the best system to show off the power of replacing equality with subtyping. Since the language does not have records, there is not any interesting subtyping that could happen. To show the usefulness of subtyping, we thus define the constraints in an environment where we have records, DR. DR plus constraints is CDR. We can contrast CDR with the EDR language which we did not study but is simply ED with support for records. Instead of types Tau\E for a set of equations E, CDR has types

Tau\{Tau₁ <: Tau₁',...,Tau_n <: Tau_n'}

CDR has the following set of type rules. These are direct generalizations of the ED rules, replacing = by <:. the <: is always in the direction of information flow. We let C represent a set of subtyping constraints.

The two rules we have not seen in ED are the Record and Projection rules. There is nothing particularly special about these rules, however.

As with ED, these rules almost directly define the type inference procedure and the proof can pretty much be built from the bottom up.

The complete type inference algorithm is as follows. Given an expression e,

1. Produce a proof of |-e : Tau\C using the above type rules. Such a proof always exists.
2. Extend C by computing the closure as described below.
3. If C is immediately inconsistent, raise a typeError.
4. Check C for cycles as described below. If C contains a cycle, raise a typeError.
5. The inferred type is e : Tau\C.

The algorithms for computing the closure of C and doing cycle detection are fairly obvious generalizations of the ED algorithms. Closure is computed as follows.

1. For each constraint {l₁ : Tau₁,...,l_n : Tau_n,...,l_m : Tau_m} <: {l₁ : Tau₁',...,l_n : Tau_n'} in C, add Tau₁ <: Tau₁', ..., Tau_n <: Tau_n' to C.
2. For each constraint Tau₀ -> Tau₀' <: Tau₁ -> Tau₁' in C, add Tau₁ <: Tau₀ and Tau₀' <: Tau₁' to C.
3. For constraints Tau₀ <: Tau₁ and Tau₁ <: Tau₂, add Tau₀ <: Tau₂ to C (by transitivity).
4. Repeat until no more constraints can be added.

A constraint set is immediately inconsistent if Tau <: Tau' and Tau and Tau' are different kinds of type (function and record, Int and function, etc), or two records are ordered by <: and the right record has a field the left record does not.

To perform cycle detection in C, we use the following algorithm. Define a directed graph G where nodes are type variables in C. There is an edge from a 'a node to a 'b node if there is an equation 'a <: Tau' in C, and 'b occurs in Tau'. Additionally, there is an edge from 'b to 'a if Tau' <: 'a occurs in C and 'b occurs in Tau'. C has a cycle if and only if G has a cycle.

It seems that there is a major omission in our constrained type inference algorithm: we never solve the constraints! The algorithm is correct, however. The reason we don’t want to solve the constraints is that any substitution proceeds with possible loss of generality. Consider, for example, a constraint 'a <: Tau, and the possibility of substituting 'a with Tau. This precludes the possibility that the 'a position be a subtype of Tau, as the substitution in effect asserts the equality of 'a and Tau. In simpler terms, we need to keep the constraints around as part of the type. This is the main weakness of constrained type systems; the types include the constraints, and are therefore difficult to read and understand.

We have the same shortcomings as in the equational case at this point: there is as of yet no polymorphism. The solution used in the equational case won’t work here, as it required the constraints to be solved.

The solution is to create constrained polymorphic types

 forall 'a1,...,'an. Tau\C

in the assumptions Gamma, in place of the polymorphic types (type schema) we had in the equational version. The details of this process are quite involved, and we will not go into them. Constrained polymorphic types make very good object types, since polymorphism is needed to type inheritance.