LET REC recursive expression static typing rule

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?

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 = AB, 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->(intint).

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.

StackExchange Computer Science Q#101152, answer score: 6