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:

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?

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?

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 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?

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:

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?