COP 4555 - Homework 6

Due Wednesday, April 20

Type Inference for PCF

Your PCF interpreter does not do any static typechecking of PCF programs. Instead, your interpreter treats PCF as a dynamically typed language, which means that it checks at runtime whether the operands of each operation are of the appropriate type. For example, the program

  (fn b => if b then 5 else succ true) true
is accepted by the interpreter, producing result AST_NUM 5, while the program
  (fn b => if b then 5 else succ true) false
fails at runtime with a message like "succ needs an integer argument".

In this homework, we will make PCF into a statically typed language by developing a program to do type inference for PCF programs. As in SML, type inference will be done using unification.

We begin by giving the type system for PCF that we wish to enforce. First of all, we will use the following set of types:

  t ::= 'a | int | bool | t -> t | (t)
Here 'a is a type variable, used for polymorphic types. As in SML, we'll assume that -> associates to the right. These types will be represented as the following SML datatype:
  datatype typ = VAR of string | INT | BOOL | ARROW of typ * typ
Typing is done with respect to an environment E, which is a mapping from identifiers to types; the environment gives the types of any free identifiers in the expression. Thus the form of typing judgment that we use is
  E |- e : t
which can be read "from environment E, it follows that expression e has type t".

Next we describe the actual typing rules. Here's the rule for typing identifiers:

      	      E(x) = t
  (ID)        ----------
              E |- x : t
And here are the rules for integer literals and booleans:
  (NUM)       E |- n : int

  (BOOL)      E |- true : bool
  
	      E |- false : bool
Here are the rules for the built-in operators:
  (BASE)      E |- succ : int -> int

	      E |- pred : int -> int

	      E |- iszero : int -> bool
Next we have the rule for if-then-else:
      	      E |- e1 : bool  E |- e2 : t  E |- e3 : t
  (IF)        ----------------------------------------
              E |- if e1 then e2 else e3 : t
Notice that this rule requires both branches of the if-then-else to have the same type.

Now we come to the rules for functions.

      	      E[x : t1] |- e : t2
  (-> INTRO)  -------------------------
              E |- fn x => e : t1 -> t2
The (-> INTRO) rule uses the notation E[x : t1] to denote an updated environment that is the same as E except that it maps x to t1. What this rule says, intuitively, is that if e has type t2 under the assumption that x has type t1, then fn x => e has type t1 -> t2 without that assumption.

Here's the rule for function application:

      	      E |- e1 : t1 -> t2  E |- e2 : t1
  (-> ELIM)   --------------------------------
              E |- e1 e2 : t2
(Notice that, if we focus only on the types, this rule is just the rule of logic known as modus ponens.)

Finally we have the rule for recursive terms:

      	      E[x : t] |- e : t
  (REC)       -------------------
              E |- rec x => e : t
If we remember that rec x => e defines a recursive function called x with definition e, then it makes sense to require x and e to have the same type.

It can be shown that these typing rules are sound in following sense: if e is a PCF program that is well typed under these rules, then e is guaranteed not to have any runtime type errors. More precisely, if e is well typed, then interp e never returns AST_ERROR s; it either successfully returns a value, or fails to terminate.

Here's an example typing derivation; we will derive the following typing for the twice function:

  [] |- fn f => fn x => f (f x) : ('a -> 'a) -> 'a -> 'a
(Note that [] denotes the empty environment.) By rule (ID), we have
(1)  [f : 'a -> 'a, x : 'a] |- f : 'a -> 'a
and
(2)  [f : 'a -> 'a, x : 'a] |- x : 'a
Hence by rule (-> ELIM) on (1) and (2) we have
(3)  [f : 'a -> 'a, x : 'a] |- f x : 'a
Then by rule (-> ELIM) on (1) and (3) we have
(4)  [f : 'a -> 'a, x : 'a] |- f (f x) : 'a
Now by rule (-> INTRO) on (4) we get
(5)  [f : 'a -> 'a] |- fn x => f (f x) : 'a -> 'a
Finally, by rule (-> INTRO) on (5) we get
(6)  [] |- fn f => fn x => f (f x) : ('a -> 'a) -> 'a -> 'a

Now we turn to the question of type inference. Given an environment E and a PCF expression e, how can we infer a principal type for e? For most of the typing rules, this is pretty straightforward---for example, (ID) says that we just look up the type of an identifier in the environment, and (NUM) says that the type of an integer literal is int. But (-> INTRO) is different. It says that to find the type of fn x => e in environment E, we first need to find the type of e in the updated environment E[x : t1]. But how do we know what t1 should be?

The answer is that we don't. So what we do in typing fn x => e is to update the environment with the assumption x : 'a, where 'a is a new type variable, and then try to find a type for e. But in the process of typing e, we may discover that 'a needs to be refined to some more specific type, such as bool -> 'b. (For example, we would make this refinement if e contained the application x true.) Hence our type inference algorithm will return not just a type, but also a substitution (which maps types to types) that reflects any of these discovered refinements. These substitutions are deduced by using an algorithm known as unification. In the example above, we initially assume that the type of x is 'a. If we see an application x true, then we know that the type of x must be of the form bool -> 'b, where 'b is a new type variable. So what we do is to call unify('a, bool -> 'b); this returns the most general substitution that makes these two types the same. (It raises an exception if no such substitution exists.)

This approach to type inference leads to an algorithm known in the literature as algorithm W. This algorithm was published by Robin Milner in 1978, but it is now usually credited also to Roger Hindley. As indicated above, algorithm W takes as input an environment E and an expression e, and produces as output a substitution s and a type t, where s includes any refinements that need to be made to E in order for e to be well typed.

For example, W([x : 'a], x true) returns (['a := bool -> 'b], 'b). This tells us that we need to refine the environment E to [x : bool -> 'b] in order for x true to be well typed:

  [x : bool -> 'b] |- x true : 'b
Formally, the soundness of algorithm W can be specified as follows: if W(E,e) returns (s,t), then
  s o E |- e : t
(Note that s o E denotes the composition of s and E; since E maps identifiers to types and s maps types to types, the composition maps identifiers to types, as an environment should.)

Your job is to implement algorithm W in SML. To do this, you first need an implementation of environments and substitutions. A particularly simple and elegant approach is to represent environments as SML functions of type string -> typ, and substitutions as SML functions of type typ -> typ; with this representation, algorithm W can be coded quite cleanly. To help you get started, here is the implementation of algorithm W on if e1 then e2 else e3:

  fun W (E, AST_IF (e1, e2, e3)) =
    let val (s1, t1) = W (E, e1)
        val s2 = unify(t1, BOOL)
        val (s3, t2) = W (s2 o s1 o E, e2)
        val (s4, t3) = W (s3 o s2 o s1 o E, e3)
        val s5 = unify(s4 t2, t3)
    in
      (s5 o s4 o s3 o s2 o s1, s5 t3)
    end
Study this code carefully, referring to rule (IF). We first recursively find the type of e1, and then unify this type with bool. We then find the types of e2 and e3, and then unify these two types. Notice that as we go along, we constantly refine the environment E with any instantiations discovered so far. (An example that illustrates the importance of doing this is fn x => if x then pred x else x. When we see x used as the guard of an if, we refine its type from 'a to bool, which then makes pred x ill typed.) In the end, we compose together all these instantiations and return them, along with the final type.

Here is a skeleton file to help you with this assignment: type.sml. (It is also available from my directory ~smithg.) The skeleton file includes quite a bit of SML code that you will find useful. In particular, I have included the unify function, a newtypevar function that lets you generate a new type variable whenever you need one, a typ2str function to convert a typ to a string, along with code for substitutions and environments. I encourage you to study the implementation of unify; unification is an important algorithm with many applications aside from type inference. (For example, unification is used crucially in the execution of the logic programming language Prolog.) Here's an example of what unify does. If we call unify on 'a -> (int -> 'b) and ('c -> bool) -> 'a, it returns a substitution that maps 'a to int -> bool, 'b to bool, and 'c to int; thus the two types are unified to (int -> bool) -> (int -> bool).

  - val t1=ARROW(VAR "a", ARROW(INT, VAR "b"));
  val t1 = ARROW (VAR "a",ARROW (INT,VAR "b")) : typ
  - val t2=ARROW(ARROW(VAR "c", BOOL), VAR "a");
  val t2 = ARROW (ARROW (VAR "c",BOOL),VAR "a") : typ
  - val s = unify(t1,t2);
  val s = fn : typ -> typ
  - s t1;
  val it = ARROW (ARROW (INT,BOOL),ARROW (INT,BOOL)) : typ
  - typ2str it;
  val it = "(int -> bool) -> int -> bool" : string

Once you have completed the implementation of algorithm W, you should try it out on a variety of PCF programs to see what types are inferred. Here are some interesting PCF programs to try:

In addition, you should try doing type inference on the sample PCF programs from HW5. But note that your type inference program may reject some of these! One cause of this is that we are treating let as syntactic sugar, which means that
  let
    twice = fn f => fn x => f (f x)
  in
    twice twice twice succ 0
  end
is treated as
  (fn twice => twice twice twice succ 0) (fn f => fn x => f (f x)).
But our type system will not allow twice to be used polymorphically within
  (fn twice => twice twice twice succ 0),
so the program is rejected. (In the actual SML type system, a let-bound identifier like twice can be given a universally quantified type, so that it can be used polymorphically within the body of the let.)

But even with the polymorphic let, there are still sensible programs (such as lists.pcf) that are rejected by the type system. This fact has spurred a great deal of research into more powerful, less restrictive type systems.

Finally, you will note that your implementation of algorithm W gives terrible error messages---when it rejects a PCF program, it raises an exception that gives almost no clue about what is wrong with the program and where the error is located. For extra credit, you may wish to try to enhance algorithm W to give decent error messages.


Back to
smithg@cs.fiu.edu