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?