LET REC recursive expression static typing rule

Question

I'm taking a programming languages course and had a question regarding the typing rules for a recursive let rec expression in a static typing system.

To be more specific, we're using the textbook Essentials of Programming Languages (3e) - Friedman & Wand.

To give some rough background, here's how the author describes the typing rule for a normal let binding expression:

To briefly describe it for anybody unfamiliar with the notation, type-of is a function used to evaluate the type of the given expression.

According to the typing rule, we evaluate exp1 first, which would give us type $t_1$. Then we extend our current environment so $var$ is mapped to $t_1$. Using this new environment, we evaluate the $body$ of the expression which gives us our final type.

Here's a typical let binding example in the OCaml programming language:

let func (x) = x + 1 in (func 3);; (* Outputs -: int=4 *)

let func = fun (x -> x + 1) in (func 3);;
(* Equivalent but better aligned with given typing rule. *)

Here's how a let-rec recursive binding's typing rule is defined:

The main problem that I'm having is how to understand the order of evaluation. According to the typing rule, it seems as though we're extending the environment first with $var$ and $p$, but where are we getting the types to map them to from?

Answer 1

It seems you discovered the difference between a set of typing rules and an algorithm for type inference.

Typing rules only define a relation among 1) a type environment, 2) a term, and 3) a type. Their purpose is only to precisely define a mathematical relation $\Gamma \vdash t: \tau$.

Once we have such definition, we do not automatically get a type checking algorithm. That is, in general, there is no algorithm described by the rules which, given $\Gamma,t,\tau$, is able to test whether $\Gamma \vdash t: \tau$ holds. (In some cases, such an algorithm could even fail to exist!)

Similarly, we do not automatically obtain a type inference algorithm, which given $\Gamma,t$ is able to find a related $\tau$ (when it exists).

The type checking/type inference algorithm must be devised independently.

Now, it is true that in many cases the algorithms can follow the rules quite closely. The rule for non-recursive LET you mention is one nice example, since it is clear how to turn it into an algorithm. For recursive LETs, we are not that lucky.

A typical strategy to type check/infer recursive LETs is to introduce a fresh type variable in the environment, and then perform type checking on the body while generating a set of constraints. For instance, consider this example

let-rec f (x: int) = 1 + f(x) in f(0)

We discover immediately that f : int -> ???. Let's introduce a fresh type variable R for the result, and say f : int -> R.

We then type check 1 + f(x) assuming the environment f: int -> R , x: int. Here + is applied to arguments 1: int and f(x): R. Assuming + requires its arguments to be of the same type, this forces the constraint int = R. If + also returns the same type, we obtain another constraint int = R (redundant, in this case).

Finally, we solve the constraints, discovering R = int.

Note that in the general case we might be less lucky, since more complex types could be involved.

let-rec f(x: int) = (2, fst(f(x-1)))

Here, we discover f: int -> R, then we see that R must be a pair type R = A*B, then A=int (because of the 2). Moreover, we get f(x-1):R so fst(f(x-1)): A, hence B=A. We conclude f: int->(int*int).

It is not trivial to generate these constraints, or to solve them (usually through a unification algorithm). In the scientific literature we can find several algorithms which perform this, but they are not obvious at first.

Answer 2

Typing rules are not "code". There is no "evaluation order". All the rule is saying is: if we're given some $t_{res}$ and $t_{var}$ (and $t$ and $tenv$ and ...) such that the first two equations hold, then we can conclude the bottom equation. How you come up with the $t_{res}$ and $t_{var}$ is out of scope and not specified.

That said, often we can read these types of rules as programs, but they are logic programs. In this context, the answer to your question is easy: you simply stick logic variables everywhere. Unification will handle the data transfer in whatever direction is needed.