OCaml: a language with lexical scope and stuff¶
OCaml is a statically typed language. Its syntactic units are expressions, and evaluating a syntactically correct and type-correct expression yields a value that has the same type as this expression.
Resources¶
- The OCaml code for the present lecture note (latest version: 06 Feb 2020).
Recap¶
So OCaml is a language of algebraic expressions, and these expressions are evaluated in the OCaml toplevel loop, if they are syntactically correct and type correct:
# 1 + 10;;
- : int = 11
# 1 +;;
Characters 3-5:
1 +;;
^^
Error: Syntax error
# 1 + "10";;
Characters 4-8:
1 + "10";;
^^^^
Error: This expression has type string but an expression was expected of type
int
#
It is a language where we can name the result of evaluating an expression (using the let construct), and where we can write our own functions (using the fun construct). For example,
here is a function from integers to integers that squares its argument: fun n -> n * n:
# (fun n -> n * n) 0;; - : int = 0 # (fun n -> n * n) (-1);; - : int = 1 # (fun n -> n * n) 2;; - : int = 4 # (fun n -> n * n) (-3);; - : int = 9 # (fun n -> n * n) 4;; - : int = 16 # (fun n -> n * n) (-5);; - : int = 25 #
here is one way to name this squaring function:
# let square = fun n -> n * n;; val square : int -> int = <fun> # square 6;; - : int = 36 # square (-7);; - : int = 49 #
and here is a more concise way to name this function:
# let square n = n * n;; val square : int -> int = <fun> # square 8;; - : int = 64 # square (-9);; - : int = 81 #
Furthermore functions can take functions as arguments and return functions as results, and this ability lets us write unit-test functions. A unit-test function is used to test another function in predefined cases. For example, here is a unit-test function for a function that maps two integers to the square of their sum. So applying this function to 0 and 0 should return 0, applying this function to 0 and any integer should return the square of this integer, applying this function to any integer and 0 should return the square of this integer, applying this function to 1 and 2 should return 9, etc. All of these cases partially recapitulate in our mind what this function should do, and it is these partial cases that we put into our unit-test function, literally as we are thinking of them, for if we are thinking them, they are worth testing:
let test_squared_sum candidate =
(candidate 0 0 = 0)
&& (candidate 0 1 = 1)
&& (candidate 0 2 = 4)
&& (candidate 1 0 = 1)
&& (candidate 2 0 = 4)
&& (candidate 1 2 = 9)
&& (candidate 2 1 = 9)
&& (candidate 5 5 = 100)
(* etc. *);;
We can then implement squared_sum to our heart’s content:
let squared_sum_v1 i j =
square (i + j);;
let squared_sum_v2 i j =
(i + j) * (i + j);;
let squared_sum_v3 i j =
square i + 2 * i * j + square j;;
let squared_sum_v4 i j =
i * (i + 2 * j) + j * j;;
let squared_sum_v5 i j =
i * i + (2 * i + j) * j;;
(Version 3 is based on the binomial theorem at rank 2, Version 4 factors i on the left in the binomial expansion, and Version 5 factors j on the right in the binomial expansion.)
And then we can check whether they pass the unit test, which they all do:
# test_squared_sum squared_sum_v1;;
- : bool = true
# test_squared_sum squared_sum_v2;;
- : bool = true
# test_squared_sum squared_sum_v3;;
- : bool = true
# test_squared_sum squared_sum_v4;;
- : bool = true
# test_squared_sum squared_sum_v5;;
- : bool = true
#
Turning to code coverage, the bodies of square and squared_sum do not contain a conditional expression, and therefore these two OCaml functions are exhaustively tested with one application.
Summing up¶
So all in all, OCaml is (a superset of) the language of algebraic expressions from earlier math courses. The unknowns (i.e., the variables such as x, y, etc.) are names that are either
- predeclared (e.g., min_int and max_int),
- declared globally with a let construct, or
- as the formal parameter of a function.
In a functional language, like in mathematics and unlike in imperative programming languages, there is no assignment construct: once declared, variables are immutable. They can be re-declared, but they don’t vary. So we can reason about OCaml expressions the way we reason about algebraic expressions, and the OCaml implementation offers us a way to evaluate these expressions.
Harald: Ah, that’s why functional languages are so popular with students.Alfrothul: How’s that?Harald: No assignments.Alfrothul: No assignments?Harald: Yes. It’s, like, a pun.
Declaring a local variable with a local let-expression¶
OCaml also features local let-expressions to declare local variables:
- <expression> ::= ... | let <formal> = <definiens> in <expression>
The corresponding typing rule reads as follows:
| LET | G |- e1 : t1 | (x : t1), G |- e2 : t2 | |
| G |- let x1 = e1 in e2 : t2 | |||
In words: in any type environment G, the expression let x1 = e1 in e2 has type t2 whenever (1) in that environment, e1 has type t1 and (2) e2 has type t2 in an extension of this environment where x1 has type t1.
Whereas a toplevel let-expression let x = d declares x to be a global variable, a let-expression let x = d in e declares x to be local to e.
Vocabulary:
- x, d, and e are often referred to as the formal parameter, the definiens, and the body of let x = d in e.
When let x = d in e is evaluated, the definiens is first evaluated and yields a value v if this evaluation completes. The body is then evaluated in an environment where x denotes v, yielding a value w if this evaluation completes. The result of evaluating the let expression is w, i.e., the result of evaluating its body. The binding of x to v is local to the let-expression, and vanishes once the let-expression is evaluated.
Graphically:
Concretely, in the standard global environment (where the addition function is denoted by a name, and this name is implicitly referred to by the infix notation +):
# let x = 1;;
val x : int = 1
# x + 100;;
- : int = 101
# let x = 10 in x + 100;;
- : int = 110
# x;;
- : int = 1
#
In this interaction,
we declare x globally to denote 1, thereby extending the global environment with one more binding;
we verify that the expression x + 100, which refers to the global variable x, evaluates to 101:
LOOKUP_FOUND ----------------------- INT ------------------------- (x : int), G |- x : int (x : int), G |- 100 : int ADD -------------------------------------------------------- (x : int), G |- x + 100 : intwe declare x locally to denote 10, and we verify that the expression x + 100, which refers to the local variable x, evaluates to 110;
graphically:
the expression x + 100 is evaluated in an environment where x is bound to 10; this local binding shadows the global binding of x to 1:
LOOKUP_FOUND ---------------------------------- INT ------------------------------------ (x : int), (x : int), G |- x : int (x : int), (x : int), G |- 100 : int ADD ------------------------------------------------------------------------------ (x : int), G |- 10 : int (x : int), (x : int), G |- x + 100 : int LET ------------------------------------------------------------------------ (x : int), G |- let x = 10 in x + 100 : intwe verify that the global variable x is unaffected by the previous local declaration:
LOOKUP_FOUND ----------------------- (x : int), G |- x : int
Let-expressions can be nested. This nesting is regulated by lexical scope: the most recently declared variable is the one whose binding is in effect.
For example:
# let a = 1 in let b = 10 in a + b;; - : int = 11 #
Graphically:
The expression a + b is evaluated in an environment where b denotes 10, a denotes 1, and the addition function is globally declared:
LOOKUP_FOUND ----------------------- (a : int), G |- a : int LOOKUP_NOT_FOUND_YET ---------------------------------- LOOKUP_FOUND ---------------------------------- (b : int), (a : int), G |- a : int (b : int), (a : int), G |- b : int ADD ------------------------------------------------------------------------------------- (a : int), G |- 10 : int (b : int), (a : int), G |- a + b : int LET --------------------------------------------------------------------------------------- G |- 1 : int (a : int), G |- let b = 10 in a + b : int LET ------------------------------------------------------------- G |- let a = 1 in let b = 10 in a + b : int
When two nested let-expressions declare the same variable, the inner binding “shadows” the outer binding in the extended environment.
For example:
# let a = 1 in let a = 10 in a;; Characters 4-5: let a = 1 in let a = 10 in a;; ^ Warning 26: unused variable a. - : int = 10 #Graphically:
The expression a is evaluated in an environment where a denotes 10 and the addition function is globally declared. The inner binding of a (to 10) shadows its outer binding (to 1), which de facto becomes unused (which the implementation of OCaml kindly warned us):
LOOKUP_FOUND --------------------------------- (a : int), G |- 10 : int (a, int), (a : int), G |- a : int LET -------------------------------------------------------------------------- G |- 1 : int (a : int), G |- let a = 10 in a : int LET ---------------------------------------------------------- G |- let a = 1 in let a = 10 in a : intFor another example of nested let-expressions:
# let x = true;; val x : bool = true # let x = 10 in (let x = 1000 in x + 10000) + x;; - : int = 11010 # x;; - : bool = true #
In this interaction,
we (re-)declare x globally to denote true, thereby extending the global environment with one more binding (that shadows the previous bindings of x):
LOOKUP_FOUND -------------------------------------- (x : bool), (x : int), ... |- x : boolwe nest two let-expressions;
graphically:
the expression x + 10000 is evaluated in an environment where x is bound to 1000; this local binding shadows the outer bindings (both the local one to 10 and the global one to true);
the expression ... + x is evaluated in an environment where x is bound to 10; this local binding shadows the outer, global one to true:
LOOKUP_FOUND ---------------------------------------------- INT -------------------------------------------------- (x : int), (x : int), (x : bool), G |- x : int (x : int), (x : int), (x : bool), G |- 10000 : int INT -------------------------------------- ADD -------------------------------------------------------------------------------------------------------- (x : int), (x : bool), G |- 1000 : int (x : int), (x : int), (x : bool), G |- x + 10000 : int LET ------------------------------------------------------------------------------------------------------------- LOOKUP_FOUND ----------------------------------- (x : int), (x : bool), G |- let x = 1000 in x + 10000 : int (x : int), (x : bool), G |- x : int ADD ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- (x : bool), G |- 10 : int (x : int), (x : bool), G |- (let x = 1000 in x + 10000) + x : int LET -------------------------------------------------------------------------------------------------- (x : bool), G |- let x = 10 in (let x = 1000 in x + 10000) + x : int
we verify that the global variable x is unaffected by the previous nested local declarations:
LOOKUP_FOUND ------------------------- (x : bool), G |- x : bool
We can also name functions locally:
# let identity = fun x -> x
in (identity 1) + (identity 10);;
- : int = 11
# (let x = fun x -> x + 1 in x 10) + (let x = fun x -> x + 100 in x 1000);;
- : int = 1111
#
Food for thought:
Here is a graphical rendition of the first interaction:
Make sure you understand why the result is 11.
Here is a graphical rendition of the first interaction:
Make sure you understand why the result is 1111.
Here is the same scenario with the more concise way of declaring functions:
# let identity x = x in (identity 1) + (identity 10);; - : int = 11 # (let x x = x + 1 in x 10) + (let x x = x + 100 in x 1000);; - : int = 1111 #
The overloading of x makes the last expression unnecessarily hard to read. In practice, better use different names and write:
# (let f x = x + 1 in f 10) + (let g y = y + 100 in g 1000);; - : int = 1111 #
What’s in a name?—Juliet
Another example of shadowing¶
Harald: What if we shadowed a variable that has one type with a variable that has another type?
Alfrothul: Well, it should work.
Vigfus: Er... An example, perhaps?
Harald: How about something like this:
fun x n -> (let x = n in x > 0) || x
Alfrothul: OK, so since || is logical disjunction, x must have type bool.
Brynja: And since n is aliased to x and then x is compared to 0, n must have type int.
Harald: Right. So all it all, it should have type, well, bool -> int -> bool, right?
Vigfus (fast on his feet): Let’s ask OCaml:
# fun x n -> (let x = n in x > 0) || x;;
- : bool -> int -> bool = <fun>
#
Alfrothul: Yup, that does it.
Halcyon: But what does this OCaml function do?
Brynja (kindly): That doesn’t really matter. The point is that we now have an inner occurrence of x that shadows the outer one and has another type.
Halcyon: Ah, OK.
Alfrothul: The question is how OCaml comes up with this type.
Harald: And to answer this question, let’s construct the proof tree. Here is its root and two inference rules for disjunction and comparison:
. |- fun x n -> (let x = n in x > 0) || x : bool -> int -> bool
| DISJ | G |- e1 : bool | G |- e2 : bool | |
| G |- e1 || e2 : bool | |||
| GREATER | G |- e1 : int | G |- e2 : int | |
| G |- e1 > e2 : int | |||
Alfrothul: Either that, or bind the names of these operators in the given environment:
((||) : bool -> bool -> bool), ((>) : int -> int -> bool), . |- fun x n -> (let x = n in x > 0) || x : bool -> int -> bool
Harald: Right, and then using the APP rule. Let’s go with the two extra rules.
Alfrothul: Sure. Anyway, fun x n -> ... is syntactic sugar for fun x -> fun n -> ..., so let’s apply the FUN rule twice:
(n : int), (x : bool), . |- (let x = n in x > 0) || x : bool
FUN -----------------------------------------------------------------
(x : bool), . |- fun n -> (let x = n in x > 0) || x : int -> bool
FUN ----------------------------------------------------------------------
. |- fun x -> fun n -> (let x = n in x > 0) || x : bool -> int -> bool
Harald: And now for the DISJ rule, where G is instantiated with (n : int), (x : bool), ., e1 is instantiated with let x = n in x > 0, and e2 is instantiated with x:
(n : int), (x : bool), . |- let x = n in x > 0 : bool (n : int), (x : bool), . |- x : bool
DISJ ---------------------------------------------------------------------------------------------
(n : int), (x : bool), . |- (let x = n in x > 0) || x : bool
FUN -----------------------------------------------------------------
(x : bool), . |- fun n -> (let x = n in x > 0) || x : int -> bool
FUN ----------------------------------------------------------------------
. |- fun x -> fun n -> (let x = n in x > 0) || x : bool -> int -> bool
Alfrothul: OK, this is where the action is. We apply the LET rule on the left subtree, where G is instantiated with (n : int), (x : bool), ., x1 is instantiated with x, e1 is instantiated with n, t1 is instantiated with int, e2 is instantiated with x > 0, and t2 is instantiated with bool:
(n : int), (x : bool), . |- n : int (x : int), (n : int), (x : bool), . |- x > 0 : bool
LET ------------------------------------------------------------------------------------------
(n : int), (x : bool), . |- let x = n in x > 0 : bool (n : int), (x : bool), . |- x : bool
DISJ ----------------------------------------------------------------------------------------------------------------------------------
(n : int), (x : bool), . |- (let x = n in x > 0) || x : bool
FUN -----------------------------------------------------------------
(x : bool), . |- fun n -> (let x = n in x > 0) || x : int -> bool
FUN ----------------------------------------------------------------------
. |- fun x -> fun n -> (let x = n in x > 0) || x : bool -> int -> bool
Harald: The left subtree begs one to apply LOOKUP_FOUND:
LOOKUP_FOUND -----------------------------------
(n : int), (x : bool), . |- n : int (x : int), (n : int), (x : bool), . |- x > 0 : bool
LET ------------------------------------------------------------------------------------------
(n : int), (x : bool), . |- let x = n in x > 0 : bool (n : int), (x : bool), . |- x : bool
DISJ ----------------------------------------------------------------------------------------------------------------------------------
(n : int), (x : bool), . |- (let x = n in x > 0) || x : bool
FUN -----------------------------------------------------------------
(x : bool), . |- fun n -> (let x = n in x > 0) || x : int -> bool
FUN ----------------------------------------------------------------------
. |- fun x -> fun n -> (let x = n in x > 0) || x : bool -> int -> bool
Alfrothul: Next step, the comparison, for which we apply the GREATER rule:
(x : int), (n : int), (x : bool), . |- x : int (x : int), (n : int), (x : bool), . |- 0 : int
LOOKUP_FOUND ----------------------------------- GREATER ------------------------------------------------------------------------------------------------
(n : int), (x : bool), . |- n : int (x : int), (n : int), (x : bool), . |- x > 0 : bool
LET --------------------------------------------------------------------------------------------------
(n : int), (x : bool), . |- let x = n in x > 0 : bool (n : int), (x : bool), . |- x : bool
DISJ ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
(n : int), (x : bool), . |- (let x = n in x > 0) || x : bool
FUN -----------------------------------------------------------------
(x : bool), . |- fun n -> (let x = n in x > 0) || x : int -> bool
FUN ----------------------------------------------------------------------
. |- fun x -> fun n -> (let x = n in x > 0) || x : bool -> int -> bool
Harald: And now we can simply apply the LOOKUP_FOUND rule and the INT rule for the left subtree of the disjunction to be complete:
LOOKUP_FOUND ---------------------------------------------- INT ----------------------------------------------
(x : int), (n : int), (x : bool), . |- x : int (x : int), (n : int), (x : bool), . |- 0 : int
LOOKUP_FOUND ----------------------------------- GREATER ----------------------------------------------------------------------------------------------------
(n : int), (x : bool), . |- n : int (x : int), (n : int), (x : bool), . |- x > 0 : bool
LET -------------------------------------------------------------------------------------------------------
(n : int), (x : bool), . |- let x = n in x > 0 : bool (n : int), (x : bool), . |- x : bool
DISJ ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
(n : int), (x : bool), . |- (let x = n in x > 0) || x : bool
FUN -----------------------------------------------------------------
(x : bool), . |- fun n -> (let x = n in x > 0) || x : int -> bool
FUN ----------------------------------------------------------------------
. |- fun x -> fun n -> (let x = n in x > 0) || x : bool -> int -> bool
Vigfus: As for the right subtree of the disjunction, we need to apply LOOKUP_NOT_FOUND_YET and then LOOKUP_FOUND to complete it:
LOOKUP_FOUND ---------------------------------------------- INT ----------------------------------------------
(x : int), (n : int), (x : bool), . |- x : int (x : int), (n : int), (x : bool), . |- 0 : int
LOOKUP_FOUND ----------------------------------- GREATER ---------------------------------------------------------------------------------------------------- LOOKUP_FOUND -------------------------
(n : int), (x : bool), . |- n : int (x : int), (n : int), (x : bool), . |- x > 0 : bool (x : bool), . |- x : bool
LET ------------------------------------------------------------------------------------------------------- LOOKUP_NOT_FOUND_YET ------------------------------------
(n : int), (x : bool), . |- let x = n in x > 0 : bool (n : int), (x : bool), . |- x : bool
DISJ ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
(n : int), (x : bool), . |- (let x = n in x > 0) || x : bool
FUN -----------------------------------------------------------------
(x : bool), . |- fun n -> (let x = n in x > 0) || x : int -> bool
FUN ----------------------------------------------------------------------
. |- fun x -> fun n -> (let x = n in x > 0) || x : bool -> int -> bool
Harald: And now the proof tree is complete.
Alfrothul: It’s kind of a downer, isn’t it?
Harald: You mean there is nothing new here?
Alfrothul: Right. We just applied the rules, and once the environment was extended with a new binding for x, that was it, the previous occurrence of x was shadowed.
Brynja: Guys, the glass is also half full – if you can use what you already know to explain something new, it’s evidence that what you know is useful.
Mimer: Correct. It also means that not everything new is novel. It would be unsettling to always need new things to explain new things, wouldn’t it?
Loki: Self-reference and Aristotle in the same sentence, Mimer. You’re doing good!
Brynja (unfazed): So, Mimer, you prefer the other root, don’t you:
((||) : bool -> bool -> bool), ((>) : int -> int -> bool), . |- fun x n -> (let x = n in x > 0) || x : bool -> int -> bool
Vigfus: Ah, right, because then we use the APP rule twice, instead of needing two new rules.
Mimer: Yup.
Loki (indefatigable): Well, you have to use the APP rule four times, instead of each DISJ and GREATER once, so there is that too.
Harald: True, but that is because one is general, and the two others are specialized.
Alfrothul: Wait. I guess we could derive the two other in terms of APP, couldn’t we?
Harald: Let’s try. Here is the root:
(b2 : bool), (b1 : bool), . |- b1 || b2 : bool
Alfrothul: Well, actually, (||) is a name, so here is the root:
(b2 : bool), (b1 : bool), ((||) : bool -> bool -> bool). |- (||) b1 b2 : bool
Vigfus (jumping in): Ah, right, we should apply the APP rule:
(b2 : bool), (b1 : bool), ((||) : bool -> bool -> bool). |- (||) b1 : bool -> bool (b2 : bool), (b1 : bool), ((||) : bool -> bool -> bool). |- b2 : bool
APP -----------------------------------------------------------------------------------------------------------------------------------------------------------
(b2 : bool), (b1 : bool), ((||) : bool -> bool -> bool). |- (||) b1 b2 : bool
Harald: Right. And we can take care of the right subtree straight off, using the LOOKUP_FOUND rule:
LOOKUP_FOUND ---------------------------------------------------------------------
(b2 : bool), (b1 : bool), ((||) : bool -> bool -> bool). |- (||) b1 : bool -> bool (b2 : bool), (b1 : bool), ((||) : bool -> bool -> bool). |- b2 : bool
APP ------------------------------------------------------------------------------------------------------------------------------------------------------------------------
(b2 : bool), (b1 : bool), ((||) : bool -> bool -> bool). |- (||) b1 b2 : bool
Vigfus: For the left subtree, we should apply the APP rule again:
(b2 : bool), (b1 : bool), ((||) : bool -> bool -> bool). |- (||) : bool -> bool -> bool (b2 : bool), (b1 : bool), ((||) : bool -> bool -> bool). |- b1 : bool
APP ---------------------------------------------------------------------------------------------------------------------------------------------------------------- LOOKUP_FOUND ---------------------------------------------------------------------
(b2 : bool), (b1 : bool), ((||) : bool -> bool -> bool). |- (||) b1 : bool -> bool (b2 : bool), (b1 : bool), ((||) : bool -> bool -> bool). |- b2 : bool
APP ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
(b2 : bool), (b1 : bool), ((||) : bool -> bool -> bool). |- (||) b1 b2 : bool
Alfrothul: Now we just need to apply LOOKUP_NOT_FOUND_YET and LOOKUP_FOUND, and we are done.
Brynja: So yes, DISJ and GREATER are derived rules, and yes, for each of them, we need to apply APP twice.
Mimer: It’s a tradeoff.
Exercise 3¶
Consider the following series of definitions:
let g = 1;; let foo h = g + h;; let g = true;; let z = foo 10;;
What is the value of z? Why is it so?
Consider the following expression:
let g = 1 in let foo h = g + h in let g = true in foo 10;; What does this expression evaluate to? Why is it so?
Declaring several variables with a local let-expression¶
In OCaml, several (distinct) local names can be defined at once:
- <expression> ::= ... | let <formal> = <definiens> {and <formal> = <definiens>}+ in <expression>
When let x1 = d1 and x2 = d2 and ... and xN = dN in e is evaluated, each of d1, d2, ..., and dN is evaluated, yielding the values v1, v2, ..., and vN if these evaluations complete. The body is then evaluated in an environment where x1, x2, ..., and xN, which must be all distinct, respectively denote v1, v2, ..., and vN, yielding a value w if this evaluation completes. The result of evaluating the let expression is w. The bindings of the formals are local to the let-expression, and vanish once the let-expression is evaluated.
The corresponding typing rule reads as follows:
| LET+ | G |- e1 : t1 | ... | G |- eN : tN | (x1 : t1), ..., (xN : tN), G |- e0 : t0 | |
| G |- let x1 = e1 and ... and xN = eN in e0 : t0 | |||||
In words: in any type environment G, the expression let x1 = e1 and ... xN = eN in e0 has type t0 whenever (1) in that environment, e1 has type t1, e2 has type t2, ..., and eN has type tN, and (2) e0 has type t0 in an extension of this environment where x1 has type t1, x2 has type t2, ..., and xN has type tN.
For example:
# let x = 1;; val x : int = 1 # let x = 10 and y = 100 in x + y;; - : int = 110 # x;; - : int = 1 # y;; Characters 0-1: y;; ^ Error: Unbound value y #
Graphically:
Naturally, let-expressions that declare several variables can be nested:
# let a = 1 and b = 10 and c = 100 in let c = b in a + b + c;; Characters 25-26: let a = 1 and b = 10 and c = 100 in let c = b in a + b + c;; ^ Warning 26: unused variable c. - : int = 21 #The result is 21 because the inner declaration of c binds it to the denotation of b, which is 10. The inner binding of c (to 10) “shadows” its outer binding (to 100), which de facto becomes unused, which the implementation of OCaml kindly tells us with a warning.
Graphically:
The expression a + b + c is evaluated in an environment where c denotes 10, b denotes 10, a denotes 1, and the addition function is globally declared. (The outer binding of c to 100 is shadowed.)
In the previous example, even if b is re-declared in the scope of c, the denotation of c is unaffected:
# let a = 1 and b = 10 and c = 100 in let c = b in let b = 1000 in a + b + c;; Characters 25-26: let a = 1 and b = 10 and c = 100 in let c = b in let b = 1000 in a + b + c;; ^ Warning 26: unused variable c. - : int = 1011 #Graphically:
The expression a + b + c is evaluated in an environment where b denotes 1000, c denotes 10, a denotes 1, and the addition function is globally declared. (The outer bindings of c to 100 and of b to 10 are shadowed.)
Each of the definienses is independent of the others and of the formals. In the following example, we put this independence to use:
# let x = 10 and y = 100 in let x = y and y = x in y - x;; - : int = -90 #
Graphically:
Environment extensions co-exist without interference. For example:
# let x = 10 in (let y = 100 in x + y) + (let y = 1000 in x + y);; - : int = 1120 #
Graphically:
- The first occurrence of x + y is evaluated in an environment where y denotes 100, x denotes 10, and the addition function is globally declared.
- The second occurrence of x + y is evaluated in an environment where y denotes 1000, x denotes 10, and the addition function is globally declared.
Note: the order in the boxes does not matter, what matters is their nesting. For example, the boxes above can be drawn just as well as follows:
Likewise, the OCaml expression could also have been variously written as follows:
let x = 10 in (let y = 100 in x + y) + (let y = 1000 in x + y);; let x = 10 in (let y = 100 in x + y) + (let y = 1000 in x + y);; let x = 10 in (let y = 100 in x + y) + (let y = 1000 in x + y);;One should write and draw whatever is simplest and most readable.
Finally, shadowed bindings in lexical scope and non-interfering co-existence of environment extensions combine harmoniously. So for example, an expression such as:
let x = 1 in (let y = 10 in let x = 100 in x + y) + x + (let y = 1000 in let y = 10000 in x + y);;
evaluates to 10112.
Graphically:
- The first occurrence of x + y, on the left, is evaluated in an environment where x denotes 100, y denotes 10, and the addition function is globally declared. (The outer binding of x to 1 is shadowed.)
- The expression x, in the middle, is evaluated in an environment where x denotes 1 and the addition function is globally declared.
- The second occurrence of x + y, on the right, is evaluated in an environment where y denotes 10000, x denotes 1, and the addition function is globally declared. (The outer binding of y to 1000 is shadowed.)
Pairs, revisited¶
Two values can be grouped into a pair of values:
Introduction:
A pair is constructed by grouping its components between parentheses and separating them with a comma:
# (1, 10);; - : int * int = (1, 10) #
Pairs can be nested:
# (1, (10, 100));; - : int * (int * int) = (1, (10, 100)) # ((1, 10), 100);; - : (int * int) * int = ((1, 10), 100) #
Elimination:
A pair is deconstructed (or again: destructured) using a mild notational extension of the formals in a let-expression:
# let (a, b) = (1, 10) in a + b;; - : int = 11 # let p = (1, 10);; val p : int * int = (1, 10) # let (a, b) = p in a + b;; - : int = 11 # let (a, (b, c)) = (1, (10, 100)) in a + b + c;; - : int = 111 # let ((a, b), c) = ((1, 10), 100) in a + b + c;; - : int = 111 #
This notational extension scales to the formals in functions:
# (fun (a, b) -> a + b) (1, 10);; - : int = 11 # let plus (a, b) = a + b;; val plus : int * int -> int = <fun> # plus (1, 10);; - : int = 11 #
So formals can reflect the structure of the domain of a function:
# (fun (a, (b, c)) -> a + b + c) (1, (10, 100));; - : int = 111 # (fun ((a, b), c) -> a + b + c) ((1, 10), 100);; - : int = 111 #
For example, the following function maps pairs of integers and Booleans to pairs of Booleans and integers:
# let swap_pair_of_int_and_bool (i, b) = (not b, i + 1);; val swap_pair_of_int_and_bool : int * bool -> bool * int = <fun> #
Tuples, revisited¶
Any number (greater than 2) of values can be grouped into a tuple of values:
Introduction:
A tuple is constructed by grouping its components between parentheses and separating them with a comma:
# (1, 10, 100);; - : int * int * int = (1, 10, 100) # (1, 10, 100, 1000);; - : int * int * int * int = (1, 10, 100, 1000) #
Tuples can be nested:
# ((1, 10), (2, 20, 200));; - : (int * int) * (int * int * int) = ((1, 10), (2, 20, 200)) # ((1, 10), (2, 20, 200), (3, 30, 300, 3000));; - : (int * int) * (int * int * int) * (int * int * int * int) = ((1, 10), (2, 20, 200), (3, 30, 300, 3000)) #
Elimination:
A tuple is deconstructed (or again: destructured) using a similar notational extension of the formals in a let-expression:
# let (a, b, c) = (1, 10, 100) in a + b + c;; - : int = 111 # let t3 = (1, 10, 100);; val t3 : int * int * int = (1, 10, 100) # let (a, b, c) = t3 in a + b + c;; - : int = 111 # let (a, b, c, d) = (1, 10, 100, 1000) in a + b + c + d;; - : int = 1111 # let t4 = (1, 10, 100, 1000);; val t4 : int * int * int * int = (1, 10, 100, 1000) # let (a, b, c, d) = t4 in a + b + c + d;; - : int = 1111 #
Again, this notational extension scales to the formals in functions:
# let foo (a, b, c, d) = a + b + c + d;; val foo : int * int * int * int -> int = <fun> # foo t4;; - : int = 1111 #
The empty tuple, revisited¶
The empty tuple has the singleton type unit:
# ();;
- : unit = ()
#
(“Singleton” because there is only one value of that type.)
Both let-expressions and functions admit an empty tuple as formal:
# let the_empty_tuple = ();;
val the_empty_tuple : unit = ()
# let () = the_empty_tuple in 42;;
- : int = 42
# let the_ultimate_answer = fun () -> 42;;
val the_ultimate_answer : unit -> int = <fun>
# the_ultimate_answer the_empty_tuple;;
- : int = 42
# let the_ultimate_answer' () = 42;;
val the_ultimate_answer' : unit -> int = <fun>
# the_ultimate_answer' the_empty_tuple;;
- : int = 42
#
Formals, formally¶
The mild notational extension of the formals in lambda-abstractions and in let expressions is accounted for by the following refined BNF:
For example, this extension provides an alternative to declaring several global variables at once using a single declaration instead of a double one:
# let x = 10 and y = 100;;
val x : int = 10
val y : int = 100
# let (x, y) = (10, 100);;
val x : int = 10
val y : int = 100
#
Likewise for (re-)declaring each of x and y to denote the previous value of the other:
# let x = y and y = x;;
val x : int = 100
val y : int = 10
# let (x, y) = (y, x);;
val x : int = 100
val y : int = 10
#
Interlude¶
Alfrothul: Neat extension.
Harald: Right. It makes it possible to write a swap function really concisely:
# fun (x, y) -> (y, x);;
- : 'a * 'b -> 'b * 'a = <fun>
#
Brynja: Not just that – we can also program functions that curry and uncurry other functions.
Harald (o_o): Curry and uncurry.
Mimer: The names come after Haskell Curry, and are due to Christopher Strachey.
Brynja: An uncurried function of arity 2 has type 'a * 'b -> 'c whereas the corresponding curried function has type 'a -> 'b -> 'c.
Alfrothul: So you mean that the curry function has type ('a * 'b -> 'c) -> 'a -> 'b -> 'c?
Harald: And that the uncurry function has type (a -> 'b -> 'c) -> 'a * 'b -> 'c?
Brynja: Yes I do.
Vigfus: I think I know how to construct the corresponding OCaml function.
Halcyon: You do?
Vigfus: I think so, yes. We just need to construct a proof tree. Here is its root, writing ? to stand for the expression we are looking for:
G |- ? : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
Alfrothul: Right. Since the type is that of a function, we have no other choice but using the FUN rule, which forces ? to be fun ... -> .... Since the type in the domain of this function is that of a function, let us name the corresponding formal parameter something intuitive, like, f, and write ?? to stand for the sub-expression we are looking for:
(f : 'a * 'b -> 'c), G |- ?? : 'a -> 'b -> 'c
FUN ----------------------------------------------------
G |- fun f -> ?? : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
Harald: Well, since 'a -> 'b -> 'c is the type of a function, we have no other choice but using the FUN rule, which forces ?? to be fun ... -> ....
Vigfus (judiciously): Actually, we have no other choice but using the FUN rule twice in a row, since the codomain of 'a -> 'b -> 'c is 'b -> 'c, i.e., the type of other function. So ?? is forced to be fun ... -> fun ... -> ....
Halcyon: Can I choose the name of the two formal parameters?
Brynja: Pray do.
Halcyon: How about a and b? We could also write ??? to stand for the sub-expression we are looking for.
Vigfus: That’s pretty intuitive indeed. All in all, fun a -> fun b -> ??? replaces ??:
(f : 'a * 'b -> 'c), G |- fun a -> fun b -> ??? : 'a -> 'b -> 'c
FUN -----------------------------------------------------------------------
G |- fun f -> fun a -> fun b -> ??? : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
Halcyon: Thank you.
Vigfun: So let’s use the FUN rule twice in a row:
(b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- ??? : 'c
FUN -----------------------------------------------------------
(a : 'a), (f : 'a * 'b -> 'c), G |- fun b -> ??? : 'b -> 'c
FUN ----------------------------------------------------------------
(f : 'a * 'b -> 'c), G |- fun a -> fun b -> ??? : 'a -> 'b -> 'c
FUN -----------------------------------------------------------------------
G |- fun f -> fun a -> fun b -> ??? : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
Harald: Now we need to conjure up an expression of type 'c in the stead of ???.
Alfrothul: We need to apply f to something – which we can write ???? – so let’s replace ??? by f ???? and use the APP rule:
(b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c (b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- ???? : 'a * 'b
APP -------------------------------------------------------------------------------------------------------------------------------
(b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- f ???? : 'c
FUN --------------------------------------------------------------
(a : 'a), (f : 'a * 'b -> 'c), G |- fun b -> f ???? : 'b -> 'c
FUN -------------------------------------------------------------------
(f : 'a * 'b -> 'c), G |- fun a -> fun b -> f ???? : 'a -> 'b -> 'c
FUN --------------------------------------------------------------------------
G |- fun f -> fun a -> fun b -> f ???? : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
Vigfus: The left branch is easy to build:
LOOKUP_FOUND -------------------------------------------
(f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c
LOOKUP_NOT_FOUND_YET -----------------------------------------------------
(a : 'a), (f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c
LOOKUP_NOT_FOUND_YET ---------------------------------------------------------------
(b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c (b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- ???? : 'a * 'b
APP -------------------------------------------------------------------------------------------------------------------------------
(b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- f ???? : 'c
FUN --------------------------------------------------------------
(a : 'a), (f : 'a * 'b -> 'c), G |- fun b -> f ???? : 'b -> 'c
FUN -------------------------------------------------------------------
(f : 'a * 'b -> 'c), G |- fun a -> fun b -> f ???? : 'a -> 'b -> 'c
FUN --------------------------------------------------------------------------
G |- fun f -> fun a -> fun b -> f ???? : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
Harald: As for ????, it has the type of a pair, so we need to a pair constructor. Let’s write (?????, ??????) in the stead of ????:
LOOKUP_FOUND -------------------------------------------
(f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c
LOOKUP_NOT_FOUND_YET -----------------------------------------------------
(a : 'a), (f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c
LOOKUP_NOT_FOUND_YET ---------------------------------------------------------------
(b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c (b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- (?????, ??????) : 'a * 'b
APP -------------------------------------------------------------------------------------------------------------------------------------------
(b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- f (?????, ??????) : 'c
FUN -------------------------------------------------------------------------
(a : 'a), (f : 'a * 'b -> 'c), G |- fun b -> f (?????, ??????) : 'b -> 'c
FUN ------------------------------------------------------------------------------
(f : 'a * 'b -> 'c), G |- fun a -> fun b -> f (?????, ??????) : 'a -> 'b -> 'c
FUN -------------------------------------------------------------------------------------
G |- fun f -> fun a -> fun b -> f (?????, ??????) : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
Alfrothul: Well, we have no other choice but using the PAIR rule:
LOOKUP_FOUND -------------------------------------------
(f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c
LOOKUP_NOT_FOUND_YET -----------------------------------------------------
(a : 'a), (f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c (b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- ????? : 'a (b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- ?????? : 'b
LOOKUP_NOT_FOUND_YET --------------------------------------------------------------- PAIR ---------------------------------------------------------------------------------------------------------------------
(b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c (b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- (?????, ??????) : 'a * 'b
APP -----------------------------------------------------------------------------------------------------------------------------------------------
(b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- f (?????, ??????) : 'c
FUN -------------------------------------------------------------------------
(a : 'a), (f : 'a * 'b -> 'c), G |- fun b -> f (?????, ??????) : 'b -> 'c
FUN ------------------------------------------------------------------------------
(f : 'a * 'b -> 'c), G |- fun a -> fun b -> f (?????, ??????) : 'a -> 'b -> 'c
FUN -------------------------------------------------------------------------------------
G |- fun f -> fun a -> fun b -> f (?????, ??????) : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
Alfrothul: So we need something of type 'a and something of type 'b.
Vigfus: According to the type environment, a and b fit the bill, so let’s replace ????? by a and ?????? by b:
LOOKUP_FOUND -------------------------------------------
(f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c
LOOKUP_NOT_FOUND_YET -----------------------------------------------------
(a : 'a), (f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c (b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- a : 'a (b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- b : 'b
LOOKUP_NOT_FOUND_YET --------------------------------------------------------------- PAIR ------------------------------------------------------------------------------------------------------------
(b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c (b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- (a, b) : 'a * 'b
APP --------------------------------------------------------------------------------------------------------------------------------------
(b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- f (a, b) : 'c
FUN ----------------------------------------------------------------
(a : 'a), (f : 'a * 'b -> 'c), G |- fun b -> f (a, b) : 'b -> 'c
FUN ---------------------------------------------------------------------
(f : 'a * 'b -> 'c), G |- fun a -> fun b -> f (a, b) : 'a -> 'b -> 'c
FUN ----------------------------------------------------------------------------
G |- fun f -> fun a -> fun b -> f (a, b) : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
Harald: And now we only need to use LOOKUP_NOT_FOUND_YET and LOOKUP_FOUND to complete the proof tree:
LOOKUP_FOUND ------------------------------------------- LOOKUP_FOUND ------------------------------------------
(f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c (a : 'a), (f : 'a * 'b -> 'c), G |- a : 'a
LOOKUP_NOT_FOUND_YET ----------------------------------------------------- LOOKUP_NOT_FOUND_YET ---------------------------------------------------- LOOKUP_FOUND ----------------------------------------------------
(a : 'a), (f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c (b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- a : 'a (b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- b : 'b
LOOKUP_NOT_FOUND_YET --------------------------------------------------------------- PAIR -------------------------------------------------------------------------------------------------------------------------
(b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- f : 'a * 'b -> 'c (b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- (a, b) : 'a * 'b
APP ------------------------------------------------------------------------------------------------------------------------------------------------------
(b : 'b), (a : 'a), (f : 'a * 'b -> 'c), G |- f (a, b) : 'c
FUN ----------------------------------------------------------------
(a : 'a), (f : 'a * 'b -> 'c), G |- fun b -> f (a, b) : 'b -> 'c
FUN ---------------------------------------------------------------------
(f : 'a * 'b -> 'c), G |- fun a -> fun b -> f (a, b) : 'a -> 'b -> 'c
FUN ----------------------------------------------------------------------------
G |- fun f -> fun a -> fun b -> f (a, b) : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
Alfrothul: The proof tree is complete, we are done. This is the expression we were looking for.
Vigfus: Let me check, let me check:
# fun f -> fun a -> fun b -> f (a, b);;
- : ('a * 'b -> 'c) -> 'a -> 'b -> 'c = <fun>
#
Mimer: Meet the curry function.
Brynja (all of a sudden): Do we really need to construct a proof tree to devise the definition?
Harald: It sure would be nice if we didn’t.
Brynja: Let’s try. The given type is ('a * 'b -> 'c) -> 'a -> 'b -> 'c, or again ('a * 'b -> 'c) -> ('a -> ('b -> 'c)) since the arrow associates to the right. So the term must start with 3 consecutive occurrences of fun:
fun ... -> fun ... -> fun ... -> ...
Alfrothul: The first formal parameter has type 'a * 'b -> 'c, which is the type of a function, so let’s pick f, and for the two others, let’s pick a and b since their type is 'a and 'b:
fun f -> fun a -> fun b -> ...
Brynja: The body of the function, i.e., ..., must have type 'c so that the overall type of this expression is the given type.
Harald: We could apply f to something, and the result would be of type 'c:
fun f -> fun a -> fun b -> f ...
Brynja: f expects a pair, so its argument should be one:
fun f -> fun a -> fun b -> f (..., ...)
Alfrothul: The first component of this pair must have type 'a, and the second 'b. Let’s just use a and b:
fun f -> fun a -> fun b -> f (a, b)
Harald: Look Ma, no proof tree.
Alfrothul: No explicit proof tree, yes, but this construction follows the shape of one.
Brynja: I guess we are building muscle memory.
Harald: So the same construction should work for the uncurry function, no?
Alfrothul: I guess. The given type is ('a -> 'b -> 'c) -> 'a * 'b -> 'c, or again ('a -> 'b -> 'c) -> ('a * 'b -> 'c) since the arrow associates to the right. So the term must start with 2 consecutive occurrences of fun:
fun ... -> fun ... -> ...
Harald: the first formal parameter has type 'a -> 'b -> 'c, which is the type of a function, so let’s pick f, and for the other, it’s a pair, so how about we use p:
fun f -> fun p -> ...
Brynja: Well, we could be more precise, since the type is 'a * 'b:
fun f -> fun (a, b) -> ...
Alfrothul: Good point. And from then on it’s the same story: the body of the function must have type c, so let’s apply f:
fun f -> fun (a, b) -> f ... ...
Harald: And since the first argument of f must be of type 'a and the second of type 'b, it’s not like we have any choice:
fun f -> fun (a, b) -> f a b
Alfrothul: I am liking this muscle memory.
Vigfus (out of the blue): I think the curry function can be written more concisely:
# fun f a b -> f (a, b);;
- : ('a * 'b -> 'c) -> 'a -> 'b -> 'c = <fun>
#
Halcyon (fast on his feet too): So, the uncurry function...
Vigfus: ...can be similarly written, yes:
# fun f (a, b) -> f a b;;
- : ('a -> 'b -> 'c) -> 'a * 'b -> 'c = <fun>
#
Halcyon (making sure): And what about functions of arity 3?
Vigfus: Same same:
# fun f a b c -> f (a, b, c);;
- : ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd = <fun>
# fun f (a, b, c) -> f a b c;;
- : ('a -> 'b -> 'c -> 'd) -> 'a * 'b * 'c -> 'd = <fun>
#
Alfrothul: Neat extension.
Exercise 4¶
- Exhibit an expression of type 'a * 'b -> 'b * 'a. Justify your answer.
- Exhibit an expression of type ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd. Justify your answer.
Resources¶
- The OCaml code for the present lecture note (latest version: 06 Feb 2020).
Version¶
Completed the proof tree in Another example of shadowing, thanks to Choi Bin’s eagle eye [01 Mar 2020]
Added the other example of shadowing [12 Feb 2020]
Fixed a pervasive typo when applying the LET rule, thanks to Choi Bin’s eagle eye [11 Feb 2020]
Adjusted the proof tree for the curry function and extended the interlude [11 Feb 2020]
Fixed a typo in Declaring a local variable with a local let-expression (an application of the ADD rule), thanks to Rayner Ng Jing Kai’s eagle eye [09 Feb 2020]
Created [06 Feb 2020]