OCaml is a typed language. Its syntactic units are typed expressions, and evaluating a typed expression yields a value that has this type. The goal of this lecture note is to introduce OCaml expressions through their grammar, together with the corresponding grammar of types:
Each expression has a type, and satisfies the following typing judgment:
G |- e : t
In words: in the type environment G, the expression e has type t.
The rest of this lecture note incrementally defines G, e, and t.
The way to interact with OCaml is through a toplevel loop that prompts the user with #, reads an expression and, if this expression is both grammatically correct and type correct, evaluates it and prints the result, if there is one:
A comment is any sequence of characters that starts with (* and finishes with *). It is skipped by the OCaml lexical analyzer.
Also, comments can be nested, i.e., they can contain other comments.
OCaml features integers:
The corresponding typing rule reads as follows:
| INT | where n is an integer | |
| G |- n : int | ||
In words,
Furthermore,
For example, the following interactive session illustrates how to play with numbers:
# 0;;
- : int = 0
# 1;; (* an implicitly positive integer *)
- : int = 1
# +1;; (* an explicitly positive integer *)
- : int = 1
# -1;; (* a negative integer *)
- : int = -1
#
In words:
Food for thought:
By default, i.e., off the shelf, 4611686018427387903 and -4611686018427387904 are respectively the largest and the smallest integers that can be represented in OCaml. (For the cognoscenti, exponentiating 2 with 0 yields 1, exponentiating 2 with 1 yields 2, exponentiating 2 with 2 yields 4, exponentiating 2 with 3 yields 8, exponentiating 2 with 10 yields 1024, and exponentiating 2 with 62 yields 4611686018427387904. So the largest value of type int is 2^62 - 1 and the smallest value of type int is -2^62.)
OCaml also features Booleans:
The corresponding typing rule reads as follows:
| BOOL_TRUE | ||
| G |- true : bool | ||
| BOOL_FALSE | ||
| G |- false : bool | ||
In words,
Furthermore,
For example, the following interactive session illustrates how to play with Booleans:
# true;;
- : bool = true
# false;;
- : bool = false
#
In words:
Reminders:
OCaml also features characters:
The corresponding typing rule reads as follows:
| CHAR | where c is a character | |
| G |- c : char | ||
In words,
Furthermore,
For example, the following interactive session illustrates how to play with characters:
# 'a';;
- : char = 'a'
# 'b';;
- : char = 'b'
# 'c';;
- : char = 'c'
#
In words:
Harald: So the way to write a character in OCaml is to type a letter between two single quotes?
Alfrothul: I guess not just a letter – any character. Let me try:
# 'A';;
- : char = 'A'
# '3';;
- : char = '3'
#
Harald: So, anything we can type in one keystroke is a character? Let me try:
# ' ';;
- : char = ' '
# '.';;
- : char = '.'
# '(';;
- : char = '('
#
Loki: What about the single quote itself?
Alfrothul: Uh-oh:
# ''';;
Characters 0-1:
''';;
^
Error: Syntax error
#
Mimer: OCaml uses the convention to quote the single quote character, using backslash, as a parsing convention:
# '\'';;
- : char = '\''
#
Brynja: For consistency, the backslash character should be quoted using backslash as well:
# '\\';;
- : char = '\\'
#
Mimer: Yup.
OCaml also features strings:
The corresponding typing rule reads as follows:
| STRING | where s is a string | |
| G |- s : string | ||
In words,
Furthermore,
For example, the following interactive session illustrates how to play with strings:
# "hello world";;
- : string = "hello world"
#
In words:
Alfrothul: Let me guess – the way to write a string in OCaml that contains the double quote character is to quote this character with a backslash:
# "\"";;
- : string = "\""
#
Harald: Indeed. And the way to write a string in OCaml that contains the backslash character is to quote it with a backslash:
# "\\";;
- : string = "\\"
#
Loki: What about "\\\\\\"?
Brynja: Logically, it is a string that contains three consecutive occurrences of the backslash character. And I guess that we should be able to write the empty string with two consecutive occurrences of the string delimiter, i.e., the double quote character:
# "";;
- : string = ""
#
Vigfus: Wait – why does OCaml say that the type of "42" is string:
# "42";;
- : string = "42"
#
Vigfus: Shouldn’t it be, I don’t know, int or perhaps even "int" or something?
Alfrothul: Because this is not a pipe, remember?
Harald: "42" is a string that contains two characters that happen to be numerical ones.
Vigfus: So you mean that '4' and '2' don’t have type, I don’t know, int or perhaps even 'int'? OCaml says that they have type char.
Harald: Right. They are numerical characters.
Alfrothul: Also, "int" and 'int' are not grammatically correct types.
OCaml also features conditional expressions (or again: if-expressions):
The corresponding typing rule reads as follows:
| IF | G |- e1 : bool | G |- e2 : t | G |- e3 : t | |
| G |- if e1 then e2 else e3 : t | ||||
In words,
Furthermore,
Conditional expressions are polymorphic (i.e., can have any type) in that as long as the type of their consequent and their alternative are the same, they yield values of this type, no matter what it is.
For example, the following interactive sessions illustrate how to play with conditional expressions:
a conditional expression can yield an integer:
# if true then 1 else 2;;
- : int = 1
# if false then 1 else 2;;
- : int = 2
#
The corresponding two proof trees read as follows:
BOOL_TRUE ---------------- INT ------------ INT ------------
G |- true : bool G |- 1 : int G |- 2 : int
IF ------------------------------------------------------------------
G |- if true then 1 else 2 : int
BOOL_TRUE ----------------- INT ------------ INT ------------
G |- false : bool G |- 1 : int G |- 2 : int
IF ------------------------------------------------------------------
G |- if false then 1 else 2 : int
a conditional expression can yield a string:
# if true then "hello" else "world";;
- : string = "hello"
# if false then "hello" else "world";;
- : string = "world"
#
The corresponding two proof trees read as follows:
BOOL_TRUE ---------------- STRING --------------------- STRING ---------------------
G |- true : bool G |- "hello" : string G |- "world" : string
IF ------------------------------------------------------------------------------------------
G |- if true then "hello" else "world" : string
BOOL_TRUE ----------------- STRING --------------------- STRING ---------------------
G |- false : bool G |- "hello" : string G |- "world" : string
IF ------------------------------------------------------------------------------------------
G |- if false then "hello" else "world" : string
Conditional expressions can also be nested, e.g., occur as a test or as a consequent in another conditional expression:
# if (if true then true else false) then 'a' else 'b';;
- : char = 'a'
# if (if false then true else false) then 'a' else 'b';;
- : char = 'b'
# if true then (if true then 'c' else 'd') else 'e';;
- : char = 'c'
# if true then (if false then 'c' else 'd') else 'e';;
- : char = 'd'
# if false then (if true then 'c' else 'd') else 'e';;
- : char = 'e'
# if false then (if false then 'c' else 'd') else 'e';;
- : char = 'e'
#
When a conditional expression occurs as a test in another conditional expression, its type must be bool, independently of the type of this other conditional expression.
Play with
In each case, state what result you expect and verify that OCaml validates your prediction.
Also, draw the proof tree of either of these conditional expressions.
A key point in Week 02 was the notion of syntax correctness: if an expression is not syntactically (i.e., lexically and grammatically) correct, it is not correct. A key point in Week 03 is the notion of type correctness: if an expression is not type correct, it is not correct.
For a conditional expression to be syntactically correct, its 3 sub-expressions (the test, the consequent, and the alternative) must be syntactically correct. And for it to be type correct, the type of its test must be bool and the types of its consequent and of its alternative must be the same. Otherwise, this expression is not correct. To wit:
# if "true" then 'a' else 'b';;
Characters 3-9:
if "true" then 'a' else 'b';;
^^^^^^
Error: This expression has type string but an expression was expected of type
bool
# if true then 'a' else -1;;
Characters 22-24:
if true then 'a' else -1;;
^^
Error: This expression has type int but an expression was expected of type
char
#
Analysis:
In both cases, the error message is understandable.
If the expression contains several type errors, the error message is about the first error that is encountered:
# if "true" then 'a' else -1;;
Characters 3-9:
if "true" then 'a' else -1;;
^^^^^^
Error: This expression has type string but an expression was expected of type
bool
#
Often, though, and that is unfortunate, we don’t understand the error message, which is a cognitive bootstrapping problem because how can we understand what is wrong and why it is wrong when we are still learning what is right?
To wit:
In the following interaction, a light-hearted proof rule is expressed as an OCaml expression:
# if A then why not B else whatever;;
Characters 3-4:
if A then why not B else whatever;;
^
Error: The variant type bool has no constructor A
#
Not knowing about variant types nor about datatype constructors yet, we are not in position to understand this error message. So, patience, until Week 10.
In the following interaction, we ask for more trouble with a refinement of light-hearted proof rule:
# if A then why not B else your guess is as good as mine;;
Characters 39-41:
if A then why not B else your guess is as good as mine;;
^^
Error: Syntax error
#
The error message is dang uninformative. It hints that we are incorrectly using as, whatever that is and whatever that means.
In the following interaction, we valiantly tell OCaml that we mean your guess is as good as mine to be the alternative of the conditional expression by wrapping it into a pair of parentheses:
# if A then why not B else (your guess is as good as mine);;
Characters 40-42:
if A then why not B else (your guess is as good as mine);;
^^
Error: Syntax error: operator expected.
#
The error message is a bit more specific, but it still refers to something we do not know yet, namely as.
As now can’t reveal the mystery of tomorrow
OCaml also features pairs:
The corresponding typing rule reads as follows:
| PAIR | G |- e1 : t1 | G |- e2 : t2 | |
| G |- (e1, e2) : t1 * t2 | |||
In words,
Furthermore,
Pairs too are polymorphic in that given two components of any type t1 and t2, they yield values of type t1 * t2, no matter what t1 and t2 are.
For example, the following interactive sessions illustrate how to play with pairs:
# (1, 2);;
- : int * int = (1, 2)
# ("hello", "world");;
- : string * string = ("hello", "world")
#
The corresponding proof trees read as follows:
INT ------------ INT ------------
G |- 1 : int G |- 2 : int
PAIR ------------------------------------
G |- (1, 2) : int * int
STRING --------------------- STRING ---------------------
G |- "hello" : string G |- "world" : string
PAIR ------------------------------------------------------------
G |- ("hello", "world") : string * string
Harald: I guess the two components of a pair can be of distinct types:
# (1, "world");;
- : int * string = (1, "world")
# ("hello", 2);;
- : string * int = ("hello", 2)
#
Alfrothul: Hey, we can even nest pairs:
# ((1, "world"), ("hello", 2));;
- : (int * string) * (string * int) = ((1, "world"), ("hello", 2))
#
Brynja: We can even construct pairs conditionally:
# if true then (true, 22) else (false, 33);;
- : bool * int = (true, 22)
#
Harald: And we can prove that this particular expression has this particular type.
Alfrothul: Why don’t you go ahead and do that.
Harald: First of all, we start at the bottom with what we want to check, namely that in any type environment G, the expression if true then (true, 22) else (false, 33) has type bool * int:
G |- if true then (true, 22) else (false, 33) : bool * int
Alfrothul: Oh. There is only one typing rule we can apply, namely IF, where G is instantiated with G, e1 is instantiated with true, e2 is instantiated with (true, 22), e3 is instantiated with (false, 33), and t is instantiated with bool * int:
G |- true : bool G |- (true, 22) : bool * int G |- (false, 33) : bool * int
IF ---------------------------------------------------------------------------------
G |- if true then (true, 22) else (false, 33) : bool * int
Now what. There are three branches to consider.
Harald: Let’s consider the left branch. There is only one typing rule we can apply, namely BOOL_TRUE, since true is a Boolean:
BOOL_TRUE ----------------
G |- true : bool G |- (true, 22) : bool * int G |- (false, 33) : bool * int
IF ---------------------------------------------------------------------------------
G |- if true then (true, 22) else (false, 33) : bool * int
This completes the left branch.
Alfrothul: OK. Let’s consider the branch in the middle. There is only one typing rule we can apply, namely PAIR, where G is instantiated with G, e1 is instantiated with true, e2 is instantiated with 22, t1 is instantiated with bool, and t2 is instantiated with int:
G |- true : bool G |- 22 : int
BOOL_TRUE ---------------- PAIR ---------------------------------
G |- true : bool G |- (true, 22) : bool * int G |- (false, 33) : bool * int
IF -------------------------------------------------------------------------------------------
G |- if true then (true, 22) else (false, 33) : bool * int
Oh, man. Two new branches.
Brynja (jumping in): Let’s consider the left branch of the branch in the middle. There is only one typing rule we can apply, namely BOOL_TRUE, since true is a Boolean:
BOOL_TRUE ----------------
G |- true : bool G |- 22 : int
BOOL_TRUE ---------------- PAIR ---------------------------------
G |- true : bool G |- (true, 22) : bool * int G |- (false, 33) : bool * int
IF ------------------------------------------------------------------------------------------------
G |- if true then (true, 22) else (false, 33) : bool * int
This completes the left branch of the branch in the middle.
Harald: Let’s consider the right branch of the branch in the middle. There is only one typing rule we can apply, namely INT, since 22 is a integer:
BOOL_TRUE ---------------- INT -------------
G |- true : bool G |- 22 : int
BOOL_TRUE ---------------- PAIR -------------------------------------
G |- true : bool G |- (true, 22) : bool * int G |- (false, 33) : bool * int
IF ----------------------------------------------------------------------------------------------------
G |- if true then (true, 22) else (false, 33) : bool * int
This completes the right branch of the branch in the middle.
Alfrothul: Let’s consider the right branch. Again, there is only one typing rule we can apply, namely PAIR, where G is instantiated with G, e1 is instantiated with false, e2 is instantiated with 33, t1 is instantiated with bool, and t2 is instantiated with int:
BOOL_TRUE ---------------- INT -------------
G |- true : bool G |- 22 : int G |- false : bool G |- 33 : int
BOOL_TRUE ---------------- PAIR ------------------------------------- PAIR ----------------------------------
G |- true : bool G |- (true, 22) : bool * int G |- (false, 33) : bool * int
IF ---------------------------------------------------------------------------------------------------------
G |- if true then (true, 22) else (false, 33) : bool * int
Two new branches. Again.
Harald: Let’s consider the left branch of the right branch. There is only one typing rule we can apply, namely BOOL_FALSE, since false is a Boolean:
BOOL_TRUE ---------------- INT ------------- BOOL_FALSE -----------------
G |- true : bool G |- 22 : int G |- false : bool G |- 33 : int
BOOL_TRUE ---------------- PAIR ------------------------------------- PAIR ----------------------------------
G |- true : bool G |- (true, 22) : bool * int G |- (false, 33) : bool * int
IF ---------------------------------------------------------------------------------------------------------
G |- if true then (true, 22) else (false, 33) : bool * int
This completes the left branch of the right branch.
Alfrothul: Let’s consider the right branch of the right branch. There is only one typing rule we can apply, namely INT, since 33 is a integer:
BOOL_TRUE ---------------- INT ------------- BOOL_FALSE ----------------- INT -------------
G |- true : bool G |- 22 : int G |- false : bool G |- 33 : int
BOOL_TRUE ---------------- PAIR ------------------------------------- PAIR --------------------------------------
G |- true : bool G |- (true, 22) : bool * int G |- (false, 33) : bool * int
IF ---------------------------------------------------------------------------------------------------------------
G |- if true then (true, 22) else (false, 33) : bool * int
This completes the right branch of the right branch.
Harald: So the proof tree is complete, which proves that if true then (true, 22) else (false, 33) has type bool * int in any type environment G.
Mimer: It’s at moments like this that I wish for more punctuation marks.
Victor Borge (thoughtfully): Phonetic ones, even.
Mimer: Mr. Borge! Thank you so much for coming by!
Victor Borge (pragmatic): Let me give you a hand here.
Victor Borge: Better?
Mimer: Yes, thanks.
Victor Borge: You are most welcome.
Mimer: But the embellishments about exhibiting simple OCaml expressions?
Victor Borge: Let’s read these questions aloud.
More generally, OCaml also features tuples, of which pairs are a particular case:
The corresponding typing rule reads as follows:
| TUPLE | G |- e1 : t1 | ... | G |- eN : tN | |
| G |- (e1, ..., eN) : t1 * ... * tN | ||||
In words,
Furthermore,
Like pairs, tuples are polymorphic in that given N components of any type t1, ..., and tN, they yield values of type t1 * ... * tN, no matter what t1, ..., and tN are.
For example, the following interactive session illustrates how to play with tuples:
# (1, 2, 3);;
- : int * int * int = (1, 2, 3)
# (1, 2, 3, 4);;
- : int * int * int * int = (1, 2, 3, 4)
# (1, 2, 3, 4, 5);;
- : int * int * int * int * int = (1, 2, 3, 4, 5)
#
Henrik Nordbrandt (wistfully): Everywhere else in the world, the year has 12 months.
Brynja: Yes?
Henrik Nordbrandt: But in Denmark, the year has 15 months.
Brynja: 15 months?
Henrik Nordbrandt: Well yes, look: 1, November; 2, December; 3, January; 4, February; 5, March; 6, April; 7, May; 8, June; 9, July; 10, August; 11, September; 12, October; and then November, November, and November.
Brynja (kindly): But November has only 30 days.
Henrik Nordbrandt: I know, right?
OCaml does not feature a tuple of size 1, but it does feature the empty tuple, which has type unit:
| UNIT | ||
| G |- () : unit | ||
In words,
Furthermore,
For example, the following interactive session illustrates how to play with the empty tuple:
# ();;
- : unit = ()
#
What do the following expressions evaluate to? What is their type? Can they be written more simply?
Harald: So parentheses in OCaml are either used for tuples...
Alfrothul: ...or to disambiguate nested expressions.
Mimer: You got it.
Brynja: And OCaml does not feature a tuple of size 1.
Mimer: That too.
OCaml also features names (a.k.a. “identifiers” or “variables”), and their type is held in the type environment:
The type environment holds a collection of bindings in which names denote types. It is constructed like the proverbial onion:
So for example,
The binding of b in the extended type environment just above, i.e., (b : string), ((i : int), ((b : bool), ((c : char), .))), is said to “shadow” (i.e., to hide) the binding of b in the previous type environment just above, i.e., (i : int), ((b : bool), ((c : char), .)). In the previous type environment, b has type bool but in the extended type environment, b has type string.
The infix environment constructor , associates to the right, and therefore we omit parentheses on the right of ,:
Looking up for a binding x : t in a type environment G is carried out incrementally with the following two typing rules:
| LOOKUP_FOUND | ||
| (x : t), G |- x : t | ||
| LOOKUP_NOT_FOUND_YET | G |- x : t | where x and x' differ |
| (x' : t'), G |- x : t |
In words,
Put otherwise:
We use these lookup rules to look up names in environments. So for example,
In the last case, the first occurrence of x shadows its other occurrences.
Justify the examples above by drawing the corresponding proof trees.
Let us pick x as a name and let us look up x in ., the empty environment. The root of the tree reads:
. |- x : yut
for some yet-unspecified type yut.
We can apply neither LOOKUP_FOUND nor LOOKUP_NOT_FOUND_YET, and therefore we cannot construct a proof tree and specify a type: looking up any name is the empty environment is undefined.
Let us look up i in (i : int), (b : bool), (c : char), .. The root of the tree reads:
(i : int), (b : bool), (c : char), . |- i : yut
for some yet-unspecified type yut.
We can (only) apply LOOKUP_FOUND, where x is instantiated with i, t is instantiated with int, G is instantiated with (b : bool), (c : char), ., x is instantiated with i, and t is instantiated with yut:
LOOKUP_FOUND -----------------------------------------------
(i : int), (b : bool), (c : char), . |- i : yut
Since in the application of LOOKUP_FOUND, t is instantiated both with int and with yut, yut is constrained to be int.
The proof tree is complete. Let us draw it again by replacing yut with int:
LOOKUP_FOUND -----------------------------------------------
(i : int), (b : bool), (c : char), . |- i : int
The existence of this tree proves that in the type environment (i : int), (b : bool), (c : char), ., looking up i yields the type int.
Let us look up b in (i : int), (b : bool), (c : char), .. The root of the tree reads:
(i : int), (b : bool), (c : char), . |- b : yut
for some yet-unspecified type yut.
We can (only) apply LOOKUP_NOT_FOUND_YET, where x' is instantiated with i, t' is instantiated with int, G is instantiated with (b : bool), (c : char), ., x is instantiated with b, and t is instantiated with yut:
(b : bool), (c : char), . |- b : yut
LOOKUP_NOT_FOUND_YET -----------------------------------------------
(i : int), (b : bool), (c : char), . |- b : yut
We can (only) apply LOOKUP_FOUND, where x is instantiated with b, t is instantiated with bool, G is instantiated with (c : char), ., x is instantiated with b, and t is instantiated with yut:
LOOKUP_FOUND ------------------------------------
(b : bool), (c : char), . |- b : yut
LOOKUP_NOT_FOUND_YET -----------------------------------------------
(i : int), (b : bool), (c : char), . |- b : yut
Since in the application of LOOKUP_FOUND, t is instantiated both with bool and with yut, yut is constrained to be bool.
The proof tree is complete. Let us draw it again by replacing yut with bool:
LOOKUP_FOUND -------------------------------------
(b : bool), (c : char), . |- b : bool
LOOKUP_NOT_FOUND_YET ------------------------------------------------
(i : int), (b : bool), (c : char), . |- b : bool
The existence of this tree proves that in the type environment (i : int), (b : bool), (c : char), ., looking up b yields the type bool.
Let us look up c in (i : int), (b : bool), (c : char), .. The root of the tree reads:
(i : int), (b : bool), (c : char), . |- c : yut
for some yet-unspecified type yut.
We can (only) apply LOOKUP_NOT_FOUND_YET, where x' is instantiated with i, t' is instantiated with int, G is instantiated with (b : bool), (c : char), ., x is instantiated with c, and t is instantiated with yut:
(b : bool), (c : char), . |- c : yut
LOOKUP_NOT_FOUND_YET -----------------------------------------------
(i : int), (b : bool), (c : char), . |- c : yut
We can (only) apply LOOKUP_NOT_FOUND_YET, where x' is instantiated with b, t' is instantiated with bool, G is instantiated with (c : char), ., x is instantiated with c, and t is instantiated with yut:
(c : char), . |- c : yut
LOOKUP_NOT_FOUND_YET ------------------------------------
(b : bool), (c : char), . |- c : yut
LOOKUP_NOT_FOUND_YET -----------------------------------------------
(i : int), (b : bool), (c : char), . |- c : yut
We can (only) apply LOOKUP_FOUND, where x is instantiated with c, t is instantiated with char, G is instantiated with ., x is instantiated with c, and t is instantiated with yut:
LOOKUP_FOUND ------------------------
(c : char), . |- c : yut
LOOKUP_NOT_FOUND_YET ------------------------------------
(b : bool), (c : char), . |- c : yut
LOOKUP_NOT_FOUND_YET -----------------------------------------------
(i : int), (b : bool), (c : char), . |- c : yut
Since in the application of LOOKUP_FOUND, t is instantiated both with char and with yut, yut is constrained to be char.
The proof tree is complete. Let us draw it again by replacing yut with char:
LOOKUP_FOUND -------------------------
(c : char), . |- c : char
LOOKUP_NOT_FOUND_YET -------------------------------------
(b : bool), (c : char), . |- c : char
LOOKUP_NOT_FOUND_YET ------------------------------------------------
(i : int), (b : bool), (c : char), . |- c : char
The existence of this tree proves that in the type environment (i : int), (b : bool), (c : char), ., looking up c yields the type char.
Let us look up x in (i : int), (b : bool), (c : char), .. The root of the tree reads:
(i : int), (b : bool), (c : char), . |- x : yut
for some yet-unspecified type yut.
We can (only) apply LOOKUP_NOT_FOUND_YET, where x' is instantiated with i, t' is instantiated with int, G is instantiated with (b : bool), (c : char), ., x is instantiated with x, and t is instantiated with yut:
(b : bool), (c : char), . |- x : yut
LOOKUP_NOT_FOUND_YET -----------------------------------------------
(i : int), (b : bool), (c : char), . |- x : yut
We can (only) apply LOOKUP_NOT_FOUND_YET, where x' is instantiated with b, t' is instantiated with bool, G is instantiated with (c : char), ., x is instantiated with x, and t is instantiated with yut:
(c : char), . |- x : yut
LOOKUP_NOT_FOUND_YET ------------------------------------
(b : bool), (c : char), . |- x : yut
LOOKUP_NOT_FOUND_YET -----------------------------------------------
(i : int), (b : bool), (c : char), . |- x : yut
We can (only) apply LOOKUP_NOT_FOUND_YET, where x' is instantiated with c, t' is instantiated with char, G is instantiated with ., x is instantiated with x, and t is instantiated with yut:
. |- x : yut
LOOKUP_NOT_FOUND_YET ------------------------
(c : char), . |- x : yut
LOOKUP_NOT_FOUND_YET ------------------------------------
(b : bool), (c : char), . |- x : yut
LOOKUP_NOT_FOUND_YET -----------------------------------------------
(i : int), (b : bool), (c : char), . |- x : yut
We can apply neither LOOKUP_FOUND nor LOOKUP_NOT_FOUND_YET, and therefore we cannot construct a proof tree and specify a type: looking up for a given name that does not occur in a given environment is undefined.
Let us look up x in (x : int), (x : bool), (x : char), . The root of the tree reads:
(x : int), (x : bool), (x : char), . |- x : yut
for some yet-unspecified type yut.
We can (only) apply LOOKUP_FOUND, where x is instantiated with x, t is instantiated with int, G is instantiated with (x : bool), (x : char), ., x is instantiated with x, and t is instantiated with yut:
LOOKUP_FOUND -----------------------------------------------
(x : int), (x : bool), (x : char), . |- x : yut
Since in the application of LOOKUP_FOUND, t is instantiated both with int and with yut, yut is constrained to be int.
The proof tree is complete. Let us draw it again by replacing yut with int:
LOOKUP_FOUND -----------------------------------------------
(x : int), (x : bool), (x : char), . |- x : int
The existence of this tree proves that in the type environment (x : int), (x : bool), (x : char), ., looking up x yields the type int.
Vigfus: Tell me again why an environment is constructed like an onion bulb?
Brynja: Sure. The point is that they are constructed alike:
<onion-bulb> ::= bud | (<onion-bulb>)
<environment> ::= . | (<name> : <type>), <environment>
Brynja (continuing): An empty environment is like a bud, it contains nothing. And given an onion bulb, we construct a new onion bulb by wrapping a layer around it; here, the layer is represented with a pair of matching parentheses. Likewise, given an environment G, a name x, and a type t, we construct a new environment (x : t), G using the infix constructor , that adds the binding (x : t) in front of G. In this new environment, x has type t.
Vigfus: OK...
Brynja: Now imagine that on each layer of the onion, there is a name printed.
Vigfus: OK?
Brynja: Now I give you an onion and I ask you whether your name is printed on one of the layers of this onion. What do you do to answer this question?
Vigfus: Well, I suppose it depends whether the onion is a bud or has an outer layer.
Brynja: Yes.
Vigfus: If it is a bud, then it has no layer and so the answer is no.
Brynja: OK.
Vigfus: Otherwise it has an outer layer. This layer has a name printed on it. If it is my name, then the answer is yes.
Brynja: Indeed.
Vigfus: Otherwise I peel out this layer and I repeat the process on this smaller onion, either until I reach a layer with my name printed on it, or until the onion is a bud.
Halcyon (interjecting): But what if the onion is infinite?
Vigfus: Infinite?
Halcyon: Well, yes. You keep peeling layers and you will never reach a bud.
Brynja: That’s not possible because the onion was constructed.
Vigfus: Was constructed?
Brynja: Yes. An onion is the result of starting from a bud and adding layers around it, a finite process. To construct an infinite onion, the process would not terminate, so an infinite onion cannot be constructed.
Vigfus: I think I get it—an environment is constructed by successively extending the empty environment with bindings, and names are looked up in an environment by successively checking these bindings.
Brynja: Yes.
Vigfus: If we reach the empty environment, the name is not bound in the environment, and otherwise we stop at the first occurrence of this name, ignoring the rest of the bindings.
Brynja: Yes.
Vigfus: So if there are more occurrences of this name in the rest of the bindings, the first occurrence shadows the others.
Brynja: Yes.
Vigfus: Thank you.
Pile on many more layersand I’ll be joining you there.
Likewise, when a syntactically correct and type-correct expression is evaluated, this evaluation takes place in an environment where names denote (i.e., are bound to) values.
Therefore,
Evaluating a variable is carried out by looking it up in the current environment.
OCaml features names that are predeclared in the initial environment. For example, min_int and max_int exist and denote the smallest and the largest representable integers:
# min_int;;
- : int = -4611686018427387904
# max_int;;
- : int = 4611686018427387903
#
These names are bound in OCaml’s initial environment.
OCaml provides language support to declare our own variables to name the result of evaluating expressions at the toplevel and extend the current environment with the binding of these variables:
The subsequent iterations of the toplevel loop take place with an extended value environment where the name declared in a let-expression denotes the value of its definiens. The following interactive session illustrates how to introduce global names and use them in the ensuing interaction. At every iteration of the toplevel loop, the system prints (from right to left) the resulting value, its type, and its name (if there is one – so far there hasn’t been any) – or an error message:
at first, x does not denote anything:
# x;;
Characters 0-1:
x;;
^
Error: Unbound value x
#
in effect, the initial type environment (let’s call it Gt) and the corresponding initial (value) environment (let’s call it Gv) do not contain any binding for x;
let us declare x:
# let x = 1;;
val x : int = 1
#
in effect, the current type environment is now (x : int), Gt and the current environment now extends Gv with the binding of x to 1;
then we can use x to access the value it denotes:
# x;;
- : int = 1
#
we can even re-declare it to denote another value:
# let x = 100;;
val x : int = 100
#
in effect, the current type environment is now (x : int), (x : int), Gt and the current environment now extends the extension of Gv with the binding of x to 100, which shadows the previous binding of x;
we can still use x to access the value it denotes:
# x;;
- : int = 100
#
we can also re-declare x to denote a value of another type:
# let x = "world";;
val x : string = "world"
#
in effect, the current type environment is now (x : string), (x : int), (x : int), Gt and the current environment now extends the extension of the extension of Gv with the binding x to "world", which shadows the previous bindings of x;
again, we can use this name:
# x;;
- : string = "world"
#
if an error occurs when the definiens is evaluated, no naming takes place:
# say_what;;
Characters 0-8:
say_what;;
^^^^^^^^
Error: Unbound value say_what
# let say_what = if 0 then 1 else -1;;
Characters 18-19:
let say_what = if 0 then 1 else -1;;
^
Error: This expression has type int but an expression was expected of type
bool
# say_what;;
Characters 0-8:
say_what;;
^^^^^^^^
Error: Unbound value say_what
#
in effect, the current type environment is still (x : string), (x : int), (x : int), Gt and the current environment has not changed.
In OCaml, several (distinct) global names can be defined at once:
For example:
# let x = 10 and y = 100;;
val x : int = 10
val y : int = 100
#
This makes it simple, for example, to (re-)declare 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
#
Attempting to declare the same global name twice gives rise to an error:
# let same = true and same = false;;
Characters 20-24:
let same = true and same = false;;
^^^^
Error: Variable same is bound several times in this matching
#
Since the names are distinct, they cannot shadow each other, and the type environment and the (value) environment can be extended in any order.
OCaml also features functions and function applications:
The corresponding typing rules read as follows:
| FUN | (x1 : t1), G |- e2 : t2 | |
| G |- fun x1 -> e2 : t1 -> t2 |
| APP | G |- e0 : t1 -> t2 | G |- e1 : t1 | |
| G |- e0 e1 : t2 | |||
In words,
Furthermore,
Like conditional expressions and tuples, these two syntax constructs are polymorphic.
Vocabulary:
The expression fun x -> e is often referred to as a lambda-abstraction (or less often as a function abstraction), and accordingly fun is often read as “lambda”. Also, e is often referred to as the body of this lambda-expression while x is said to be its formal parameter.
The expression e0 e1 is referred to as a function application (or often just as an application), and e1 as the actual parameter.
When a lambda-abstraction such as fun x -> x, the identity function, is applied to an actual parameter such as 33, its body, i.e., x, is evaluated in an environment where x denotes 33, which is the topic of the next sections:
# (fun x -> x) 33;;
- : int = 33
That (fun x -> x) 33 has type int is proved using the following proof tree, where Gv denotes any value environment:
LOOKUP_FOUND ------------------------
(x : int), Gv |- x : int
FUN ----------------------------- INT --------------
Gv |- fun x -> x : int -> int Gv |- 33 : int
APP ---------------------------------------------------
Gv |- (fun x -> x) 33 : int
(See Solution for Exercise 09 below for a step-by-step construction of such a proof tree.)
Likewise, the lambda-abstraction fun b -> if b then "hello" else "world" has type bool -> string; applying it to true yields "hello" since its body if b then "hello" else "world" is evaluated in an environment where b denotes true, and applying it to false yields "world" since its body if b then "hello" else "world" is evaluated in an environment where b denotes false:
# fun b -> if b then "hello" else "world";;
- : bool -> string = <fun>
# (fun b -> if b then "hello" else "world") true;;
- : string = "hello"
# (fun b -> if b then "hello" else "world") false;;
- : string = "world"
#
Concretely:
that fun b -> if b then "hello" else "world" has type bool -> string is proved using the following proof tree, where Gv denotes any value environment:
LOOKUP_FOUND -------------------------- STRING ---------------------------------- STRING ----------------------------------
(b : bool), Gv |- b : bool (b : bool), Gv |- "hello" : string (b : bool), Gv |- "world" : string
IF ---------------------------------------------------------------------------------------------------------------------
(b : bool), Gv |- if b then "hello" else "world" : string
FUN --------------------------------------------------------------
Gv |- fun b -> if b then "hello" else "world" : bool -> string
that (fun b -> if b then "hello" else "world") true has type string is proved using the following proof tree, where Gv denotes any value environment:
...see just above...
FUN -------------------------------------------------------------- BOOL_TRUE -----------------
Gv |- fun b -> if b then "hello" else "world" : bool -> string Gv |- true : bool
APP ---------------------------------------------------------------------------------------------
Gv |- (fun b -> if b then "hello" else "world") true : string
and that (fun b -> if b then "hello" else "world") false has type string is proved using the following proof tree, where Gv denotes any value environment:
...see above...
FUN -------------------------------------------------------------- BOOL_FALSE ------------------
Gv |- fun b -> if b then "hello" else "world" : bool -> string Gv |- false : bool
APP -----------------------------------------------------------------------------------------------
Gv |- (fun b -> if b then "hello" else "world") false : string
(See Solution for Exercise 09 below for a step-by-step construction of such proof trees.)
OCaml comes with a mass of pre-existing functions such as not, which has type bool -> bool and negates its argument. Here is not at work:
# not;;
- : bool -> bool = <fun>
# not true;;
- : bool = false
# not false;;
- : bool = true
# not (not true);;
- : bool = true
# not (not false);;
- : bool = false
#
Many of OCaml’s pre-existing functions are declared separately in libraries. For example, definitions that pertain to strings are declared in the library for strings, String. Take the pre-existing function for computing the length of a string. This function
Here is String.length at work:
# String.length;;
- : string -> int = <fun>
# String.length "";;
- : int = 0
# String.length "a";;
- : int = 1
# String.length "ab";;
- : int = 2
# String.length "abc";;
- : int = 3
#
In words, String.length maps a string to its number of characters.
Alfrothul: Let me check something:
# String.length "\"";;
- : int = 1
#
Alfrothul: Yup. One character. The backslash is purely notational.
Brynja: Let me check something too:
# String.length "\\\\\\";;
- : int = 3
#
Brynja: Right. Three characters. Good.
Grammatically, nothing prevents us from writing functions that return functions, and then
applying such functions to a first argument, and
applying the result to a second argument:
# ((fun x -> fun y -> x) 1) 2;;
- : int = 1
# ((fun x -> fun y -> y) 1) 2;;
- : int = 2
#
Concretely:
that ((fun x -> fun y -> x) 1) 2 has type int is proved with the following proof tree:
LOOKUP_FOUND ------------------------
(x : int), Gv |- x : int
LOOKUP_NOT_FOUND_YET -----------------------------------
(y : int), (x : int), Gv |- x : int
FUN ----------------------------------------
(x : int), Gv |- fun y -> x : int -> int
FUN ----------------------------------------------- INT -------------
Gv |- fun x -> fun y -> x : int -> (int -> int) Gv |- 1 : int
APP -------------------------------------------------------------------- INT -------------
Gv |- (fun x -> fun y -> x) 1 : int -> int Gv |- 2 : int
APP -----------------------------------------------------------------------------------------
Gv |- ((fun x -> fun y -> x) 1) 2 : int
and that ((fun x -> fun y -> y) 1) 2 also has type int is proved with the following proof tree:
LOOKUP_FOUND -----------------------------------
(y : int), (x : int), Gv |- y : int
FUN ----------------------------------------
(x : int), Gv |- fun y -> y : int -> int
FUN ----------------------------------------------- INT -------------
Gv |- fun x -> fun y -> y : int -> (int -> int) Gv |- 1 : int
APP -------------------------------------------------------------------- INT -------------
Gv |- (fun x -> fun y -> y) 1 : int -> int Gv |- 2 : int
APP -----------------------------------------------------------------------------------------
Gv |- ((fun x -> fun y -> y) 1) 2 : int
(See Solution for Exercise 09 below for a step-by-step construction of such proof trees.)
Actually, function applications associate to the left, so the outermost parentheses are unnecessary:
# (fun x -> fun y -> x) 1 2;;
- : int = 1
# (fun x -> fun y -> y) 1 2;;
- : int = 2
#
Correspondingly, the function type associates to the right, so e.g., in int -> (int -> int), the parentheses are unnecessary and this type is written int -> int -> int.
As it turns out, OCaml comes with a plethora of such predeclared functions, as described next.
In practice, it is too verbose to write fun x -> fun y -> ... so this verbosity is alleviated with the short hand fun x y -> ...:
# (fun x -> fun y -> x) 1 10;;
- : int = 1
# (fun x y -> x) 1 10;;
- : int = 1
# (fun x -> fun y -> y) 1 10;;
- : int = 10
# (fun x y -> y) 1 10;;
- : int = 10
#
Such a short hand is referred to as “syntactic sugar” since Peter Landin.
Take the addition function, for example. OCaml provides the standard infix notation for it in the form of a + operator:
# 1 + 10;;
- : int = 11
#
This infix notation is left associative in that in, e.g., (1 + 10) + 100 and 1 + 10 + 100 are parsed into the same abstract-syntax tree:
# (1 + 10) + 100;;
- : int = 111
# 1 + 10 + 100;;
- : int = 111
#
What about right associativity, one might ask:
# 1 + (10 + 100);;
- : int = 111
#
The expression 1 + (10 + 100) is parsed into another abstract-syntax tree. And since addition is associative, both of (1 + 10) + 100 and 1 + (10 + 100) evaluate to the same result.
That being said, infix operators are only syntactic sugar, i.e., a notational convenience. The truth of the matter is that addition is implemented with a function named add which is defined in a library (i.e., a collection of definitions that are grouped separately) named Int. The type of Int.add is int -> int -> int and
To wit:
# Int.add 1 10;;
- : int = 11
# Int.add (Int.add 1 10) 100;;
- : int = 111
# Int.add (Int.add 1 10) 100;;
- : int = 111
# Int.add 1 (Int.add 10 100);;
- : int = 111
#
As such, the addition function is an example of a function that returns another function:
# Int.add;;
- : int -> int -> int = <fun>
# Int.add 1;;
- : int -> int = <fun>
# Int.add 1 10;;
- : int = 11
#
More syntactic sugar: for convenience, (+) is read as Int.add:
# (+);;
- : int -> int -> int = <fun>
# (+) 1;;
- : int -> int = <fun>
# (+) 1 10;;
- : int = 11
#
In other words, there is no need for a specialized typing rule such as
| ADD | G |- e1 : int | G |- e2 : int | |
| G |- e1 + e2 : int | |||
because OCaml’s initial type environment binds Int.add to int -> int -> int and the parser desugars an expression such as e1 + e2 into Int.add e1 e2.
Regarding the subtraction function, OCaml provides the standard infix notation for it in the form of a - operator:
# 10 - 1;;
- : int = 9
#
This infix notation is also left associative in that in, e.g., (100 - 10) - 1 and 100 - 10 - 1 are parsed into the same abstract-syntax tree:
# 100 - 10 - 1;;
- : int = 89
# (100 - 10) - 1;;
- : int = 89
#
Unlike addition, subtraction is not associative, and therefore not only are (100 - 10) - 1 and 100 - (10 - 1) not parsed into the same abstract-syntax tree, they do not evaluate to the same result:
# 100 - (10 - 1);;
- : int = 91
#
Harald: So syntax and semantics are not the same at all.Mimer: Yes. Syntax is about how things are written and semantics about what these things mean.Harald: So the infix operators for addition and subtraction...Alfrothul: ...are not the same as the addition and the subtraction functions.Mimer: Yes. Infix operations are desugared into nested applications of library functions.
Subtraction is implemented with a function named sub which is defined in the Int library. The type of Int.sub is int -> int -> int and
More syntactic sugar: for convenience, (-) is read as Int.sub:
# (-);;
- : int -> int -> int = <fun>
#
With the convenience of infix notation, OCaml provides a wealth of functions that return functions:
multiplication (Int.mul):
# 2 * 3;;
- : int = 6
#
N.B.:
quotient (Int.div):
# (/);;
- : int -> int -> int = <fun>
# 4 / 2;;
- : int = 2
# 5 / 2;;
- : int = 2
# 1 / 0;;
Exception: Division_by_zero.
#
N.B.:
Alfrothul: Look, an error!
Harald: You mean, the division by 0 just above?
Alfrothul: Yes!
Harald: Well, yes. Dividing any number by 0 is undefined, so it is good that OCaml is not making an exception here.
Loki: Actually, OCaml is taking an exception to that, or so the error message says.
Brynja: Guys, you are not seeing this. Most descriptions of how OCaml syntactic constructs are evaluated say “if evaluating blah raises an error” one way or another.
Alfrothul: Right. And this is the first time that we encounter a concrete situation where an error is raised.
Halcyon: Ah, I see. We can now exercise our critical sense and test the narrative:
# if 1 / 0 then "hello" else "world";;
Characters 3-8:
if 1 / 0 then "hello" else "world";;
^^^^^
Error: This expression has type int but an expression was expected of type
bool
#
Vigfus: Hum. This is not the error I was expecting, but an error it is.
Harald: It’s a type error.
Vigfus: This error needs to be fixed so that the correct error can take place:
# if 1 / 0 = 0 then "hello" else "world";;
Exception: Division_by_zero.
#
Alfrothul: All in a day’s work. Evaluating the test raised an error, and the whole evaluation stopped.
Halcyon: OK. I guess this matters if there are errors in your programs. Can we proceed now?
So, continuing—with the convenience of infix notation, OCaml provides a wealth of functions that return functions:
modulo (Int.rem):
# (mod);;
- : int -> int -> int = <fun>
# 12 mod 5;;
- : int = 2
#
N.B.:
comparison of two integers:
# (2 < 3, 3 < 3, 3 < 2);;
- : bool * bool * bool = (true, false, false)
#
Food for thought: is comparison associative and does this question make sense?
boolean conjunction:
# (&&);;
- : bool -> bool -> bool = <fun>
# (true && true, true && false, false && true, false && false);;
- : bool * bool * bool * bool = (true, false, false, false)
#
(Reminder: the conjunction of two Booleans is true if both of these Booleans are true; otherwise it is false.)
N.B.:
boolean disjunction:
# (||);;
- : bool -> bool -> bool = <fun>
# (true || true, true || false, false || true, false || false);;
- : bool * bool * bool * bool = (true, true, true, false)
#
(Reminder: the disjunction of two Booleans is false if both of these Booleans are false; otherwise it is true.)
N.B.:
string concatenation (String.concat):
# (^);;
- : string -> string -> string = <fun>
# "hello" ^ " " ^ "world";;
- : string = "hello world"
#
N.B.:
OCaml also features functions that return the smallest or the greatest of their two arguments:
minimum of two integers:
# (min 2 5, min 6 3);;
- : int * int = (2, 3)
#
maximum of two integers:
# (max 2 5, max 6 3);;
- : int * int = (5, 6)
#
And the String library function features a function to index a string:
# String.get;;
- : string -> int -> char = <fun>
# String.get "abc" 0;;
- : char = 'a'
# String.get "abc" 1;;
- : char = 'b'
# String.get "abc" 2;;
- : char = 'c'
# String.get "abc" 3;;
Exception: Invalid_argument "index out of bounds".
#
In words: given a string of length n and a non-negative integer i (the “index”) such that 0 <= i < n, String.get returns the i+1th character of the string, i.e., the first character if the index is 0, the second character if the index is 1, etc., reflecting the fact that 0 is the first natural number, 1 is the second natural number, etc.
Alfrothul: Look, another error!
Harald: You mean, the indexing out of bounds just above?
Alfrothul: Yes. Since the length of "abc" is 3, its bounds are 0 and 2. More generally, if the length of the given string is n, its bounds are 0 and n-1.
Harald: But what if the length of the given string is 0? Its bounds are 0 and -1?
Alfrothul: -1 doesn’t make sense. Surely OCaml raises an error. Let me try:
# String.get "" 0;;
Exception: Invalid_argument "index out of bounds".
#
Harald: Well, if the string is empty, it contains no characters, and so none can be indexed.
Alfrothul: And the set of non-negative integers between 0 and -1 is empty.
Harald: OK.
Alfrothul: Now that we here, why not check something.
Harald: You mean a string with a quoted character inside, right?
Alfrothul: Yup:
# String.get "\"" 0;;
- : char = '"'
# String.get "\\" 0;;
- : char = '\\'
#
Alfrothul and Harald: Yay!
Loki: So you can both make a \ disappear and you can keep it too. Can you make one appear?
Brynja: Sure thing:
# String.get "'" 0;;
- : char = '\''
#
Can you visualize the multiplication function hidden behind the infix notation *, as we did just above for addition (+), subtraction (-), quotient (/), modulo (mod), etc.? For example:
# 1 * 2;;
- : int = 2
# 1 * 2 * 3;;
- : int = 6
# 1 * 2 * 3 * 4;;
- : int = 24
# 1 * 2 * 3 * 4 * 5;;
- : int = 120
#
Loki: No comment.
This exercise is a followup to Exercise 07.
After typing (*);; at the toplevel, type *)33;;. What happens? Why does it happen?
Shouldn’t you write ( * ) instead?
The point of these exercises is the ambiguity of (* and *) as comment delimiters and of (*) as parenthesizing the infix operator *:
(* ) is ambiguous – is it the beginning of a comment or the multiplication function?
OCaml made a choice:
# (*) *);;
Characters 0-3:
(*) *);;
^^^
Warning 1: this is the start of a comment.
#
( *) is ambiguous – is it the end of a comment or the multiplication function?
OCaml made a choice:
# ( *);;
Characters 2-4:
( *);;
^^
Warning 2: this is not the end of a comment.
- : int -> int -> int = <fun>
#
Vigfus (fresh out of solving Exercise 08): See my nice ASCII art piece?:
+-------------------------------------+
| |
| |
| |
| ( *);; |
| |
| |
| |
| This is not the end of a comment. |
+-------------------------------------+
Alfrothul (admirative): Magritte lives.
Harald: You can say that again.
Alfrothul: Er... Sure. Magritte lives.
Brynja: You guys are so literal sometimes.
OCaml also provides a family of equality functions for each of the ground types (integers, Booleans, characters, and strings), each noted with the infix operator =:
# 1 = 1;;
- : bool = true
# 1 = 2;;
- : bool = false
# true = true;;
- : bool = true
# 'a' = 'b';;
- : bool = false
# "hello" = "world";;
- : bool = false
#
Such Boolean-valued functions are called “predicates”.
Accordingly, the equality predicate comes with a family of typing rules:
| equal_int | G |- e1 : int | G |- e2 : int | |
| G |- e1 = e2 : bool | |||
| equal_bool | G |- e1 : bool | G |- e2 : bool | |
| G |- e1 = e2 : bool | |||
| equal_char | G |- e1 : char | G |- e2 : char | |
| G |- e1 = e2 : bool | |||
| equal_string | G |- e1 : string | G |- e2 : string | |
| G |- e1 = e2 : bool | |||
Negated equality is noted with the infix operator <> (or again !=) and comes with a similar family of typing rules:
# 1 <> 1;;
- : bool = false
# 1 <> 2;;
- : bool = true
# true <> true;;
- : bool = false
# 'a' <> 'b';;
- : bool = true
# "hello" <> "world";;
- : bool = true
# "hello" != "world";;
- : bool = true
#
Say that we need to evaluate a series of expressions that only differ in part, e.g., to start enumerating the sequence of odd numbers:
# 2 * 0 + 1;;
- : int = 1
# 2 * 1 + 1;;
- : int = 3
# 2 * 2 + 1;;
- : int = 5
# 2 * 3 + 1;;
- : int = 7
# 2 * 4 + 1;;
- : int = 9
# 2 * 5 + 1;;
- : int = 11
#
The part that differs is 0, 1, 2, 3, 4, and 5. The part that remains the same is the template 2 * ... + 1, often referred to as a delimited context (an expression with a hole) and noted as [2 * [.] + 1] where the outer brackets delimit the outside of the context and the inside brackets mark the hole in the context. Filling this hole with 0, for example, yields the expression 2 * 0 + 1.
OCaml provides language support to represent this context: as a function, noted here fun x -> 2 * x + 1 where the hole is abstracted with an identifier that is declared as the formal parameter of the function. Applying this function is expressed by juxtaposing the function and its argument (a.k.a. its actual parameter):
# (fun x -> 2 * x + 1) 0;;
- : int = 1
# (fun x -> 2 * x + 1) 1;;
- : int = 3
# (fun x -> 2 * x + 1) 2;;
- : int = 5
# (fun x -> 2 * x + 1) 3;;
- : int = 7
# (fun x -> 2 * x + 1) 4;;
- : int = 9
# (fun x -> 2 * x + 1) 5;;
- : int = 11
#
In each of these interactions, x successively denotes 0, 1, ..., and 5 when the expression 2 * x + 1 is evaluated.
This way, in the expression that needs to be repeatedly evaluated (here: 2 * x + 1), the unchanging parts (here, the delimited context [2 * [.] + 1]) are factored away in the body of the function.
Assuming the following typing rule
| MUL | G |- e1 : int | G |- e2 : int | |
| G |- e1 * e2 : int | |||
and using the typing rule for addition mentioned above, i.e.,
| ADD | G |- e1 : int | G |- e2 : int | |
| G |- e1 + e2 : int | |||
find the type of the expression fun x -> 2 * x + 1, knowing that infix multiplication takes precedence over infix addition, i.e., the expression 2 * x + 1 actually reads (2 * x) + 1.
First of all, let us consult OCaml, just because it’s there and we can:
# fun x -> 2 * x + 1;;
- : int -> int = <fun>
#
Now all we need to do is construct a proof tree to the effect that the term fun x -> 2 * x + 1, or again to be precise, fun x -> (2 * x) + 1 has type int -> int in any type environment G:
Let us start at the root of the tree:
G |- fun x -> (2 * x) + 1 : int -> int
There is only one typing rule we can apply, namely FUN, where G is instantiated with the current type environment, i.e., G, x is instantiated with the formal parameter of the current function abstraction, i.e., x, e is instantiated with the body of the current function abstraction, i.e., (2 * x) + 1, t1 is instantiated with the domain of the current type (namely int -> int), i.e., int, and t2 is instantiated with the codomain of the current type (namely int -> int), i.e., int:
(x : int), G |- (2 * x) + 1 : int
FUN ------------------------------------
G |- fun x -> (2 * x) + 1 : int -> int
There is only one typing rule we can apply, namely ADD, where G is instantiated with the current type environment, i.e., (x : int), G, e1 is instantiated with the first operand in the current expression, i.e., (2 * x), and e2 is instantiated with the second operand in the current expression, i.e., 1:
(x : int), G |- 2 * x : int (x : int), G |- 1 : int
ADD ------------------------------------------------------
(x : int), G |- (2 * x) + 1 : int
FUN ------------------------------------
G |- fun x -> (2 * x) + 1 : int -> int
Let’s consider the left branch. There is only one typing rule we can apply, namely MUL, where G is instantiated with the current type environment, i.e., (x : int), G, e1 is instantiated with the first operand in the current expression, i.e., 2, and e2 is instantiated with the second operand in the current expression, i.e., x:
(x : int), G |- 2 : int (x : int), G |- x : int
MUL --------------------------------------------------
(x : int), G |- 2 * x : int (x : int), G |- 1 : int
ADD -----------------------------------------------------------------------------
(x : int), G |- (2 * x) + 1 : int
FUN ------------------------------------
G |- fun x -> (2 * x) + 1 : int -> int
Let’s consider the left branch of the left branch. There is only one typing rule we can apply, namely INT (where G is instantiated with (x : int), G and n is instantiated with 2), since 2 is an integer:
INT -----------------------
(x : int), G |- 2 : int (x : int), G |- x : int
MUL --------------------------------------------------
(x : int), G |- 2 * x : int (x : int), G |- 1 : int
ADD -----------------------------------------------------------------------------
(x : int), G |- (2 * x) + 1 : int
FUN ------------------------------------
G |- fun x -> (2 * x) + 1 : int -> int
This completes the left branch of the left branch.
Let’s consider the right branch of the left branch. There is only one typing rule we can apply, namely LOOKUP_FOUND, where x is instantiated with the first identifier in the current environment, i.e., x, t is instantiated with the type of the first identifier in the current environment, i.e., int, G is instantiated with the rest of the type environment, i.e., G, x is instantiated with the identifier to look up, i.e., x, and t is instantiated with the current type, i.e., int:
INT ----------------------- LOOKUP_FOUND -----------------------
(x : int), G |- 2 : int (x : int), G |- x : int
MUL ---------------------------------------------------------------
(x : int), G |- 2 * x : int (x : int), G |- 1 : int
ADD ------------------------------------------------------------------------------------------
(x : int), G |- (2 * x) + 1 : int
FUN ------------------------------------
G |- fun x -> (2 * x) + 1 : int -> int
This completes the right branch of the left branch.
Let’s consider the right branch. There is only one typing rule we can apply, namely INT (where G is instantiated with (x : int), G and n is instantiated with 1), since 1 is an integer:
INT ----------------------- LOOKUP_FOUND -----------------------
(x : int), G |- 2 : int (x : int), G |- x : int
MUL --------------------------------------------------------------- INT -----------------------
(x : int), G |- 2 * x : int (x : int), G |- 1 : int
ADD ----------------------------------------------------------------------------------------------
(x : int), G |- (2 * x) + 1 : int
FUN ------------------------------------
G |- fun x -> (2 * x) + 1 : int -> int
This completes the right branch.
The proof tree is complete, which proves that fun x -> 2 * x + 1 has type int -> int in any type environment G.
Under the same conditions as that in Exercise 09, find the type of the expression fun y -> fun x -> 2 * x + y.
Recommendation: first peruse both Exercise 09 and Exercise 21 and their solution.
Here, “briefly justify your answer” means “simply use OCaml for each justification”.
Draw a proof tree to justify your answer for Item e. of Exercise 11, under conditions similar to that in Exercise 09.
Evaluating a lambda-abstraction yields an anonymous function, which may be practical but not always, since indeed most of the time, functions are named:
# let make_odd_number = fun x -> 2 * x + 1;;
val make_odd_number : int -> int = <fun>
# make_odd_number 0;;
- : int = 1
# make_odd_number 1;;
- : int = 3
# make_odd_number 2;;
- : int = 5
# make_odd_number 3;;
- : int = 7
# make_odd_number 4;;
- : int = 9
# make_odd_number 5;;
- : int = 11
#
Harald: Do you know many programming languages where one can declare an anonymous function?Alfrothul: Er... No.
In practice, it is too verbose to write let f = fun x -> e so this verbosity is alleviated with the short hand let f x = e:
# let make_odd_number x = 2 * x + 1;;
val make_odd_number : int -> int = <fun>
# make_odd_number 6;;
- : int = 13
# let x x = 2 * x + 1;;
val x : int -> int = <fun>
# x 6;;
- : int = 13
# let make_odd_number make_odd_number = 2 * make_odd_number + 1;;
# make_odd_number 6;;
- : int = 13
#
We have met the enemy and [they are] us.—Pogo
The naming style of reusing x and make_odd_number, in the last two definitions, is chiefly used to confuse the enemy.
At any rate, this short hand is only a notation: the name that is declared still denotes a function:
# let make_even_number x = 2 * x;;
val make_even_number : int -> int = <fun>
# make_even_number;;
- : int -> int = <fun>
#
Harald: Does the name of a formal parameter matter, in a lambda-abstraction?
Mimer: Beg pardon?
Harald: Does it matter how we name it?
Alfrothul: For example, does it matter whether we write fun x -> x + 1 or fun y -> y + 1?
Mimer: No, it doesn’t matter. These two lambda-abstractions evaluate to the same function.
Brynja: What do you mean by “the same function”?
Mimer: I mean that the two resulting values behave the same. Applying them to the same input yields the same output, always. So they are undistinguishable.
Harald: You mean they are equal?
Alfrothul: Because somehow OCaml disagrees:
# (fun x -> x + 1) = (fun y -> y + 1);;
Exception: Invalid_argument "equal: functional value".
#
Mimer: Rightly so, since the only way to compare two functions is to test whether applying them to each of their possible input values yields the same output values. The equality predicate denoted by (=) cannot do that. Besides, as seen above, it is only defined for each of the ground types. In fact, ...
Brynja: Question.
Mimer: Yes?
Brynja: Didn’t you already make this point in the section about Program equivalence in Week 02?
Mimer: Matter of fact I did. Thanks, Brynja.
Suppose we need to define a function that maps a number i not to 2 * i + 1, but to 3 * i + 1, and another that maps a number i to 4 * i + 1. The same post-rationalization as above applies: we have a delimited context [fun i -> [.] * i + 1]] which we can represent as a function:
# let make_multiple_plus_one = fun m -> fun i -> m * i + 1;;
val make_multiple_plus_one : int -> int -> int = <fun>
# make_multiple_plus_one 2 10;;
- : int = 21
# make_multiple_plus_one 3 10;;
- : int = 31
# make_multiple_plus_one 4 10;;
- : int = 41
#
This function returns another function:
# let make_odd_number = make_multiple_plus_one 2;;
val make_odd_number : int -> int = <fun>
#
In practice, it is too verbose to write let bar = fun x y -> ... so this verbosity is alleviated with the short hand let bar x y = .... It is only a notation: bar still denotes a function, and so does the result of applying bar to one argument:
# let bar x y = x + y;;
val bar : int -> int -> int = <fun>
# bar;;
- : int -> int -> int = <fun>
# bar 1;;
- : int -> int = <fun>
#
That said, fully applying bar to two actual parameters “saturates” its two formal parameters and its body x + y is then evaluated in an environment where x denotes 1 and y denotes 10:
# bar 1 10;;
- : int = 11
#
This notation makes it easy to think of functions that return functions as functions that take two arguments, which is fine as long as these functions are fully applied:
# let make_multiple_plus_one m x = m * x + 1;;
val make_multiple_plus_one : int -> int -> int = <fun>
# let make_odd_number x = make_multiple_plus_one 2 x;;
val make_odd_number : int -> int = <fun>
#
On a related note, how would you characterize the sum of a non-negative integer and its successor in terms of this integer?
Vigfus: Related. How related?Brynja: Related to make_odd_number, I think.
Conversely to having functions return functions, we can also apply functions to other functions, which is ideal to write unit tests, as developed in the next chapter.
Refined the first mention of libraries and added the express interlude [13 Feb 2022]
Changed the statement of Exercise 10 from fun x -> fun y -> 2 * x + y to fun y -> fun x -> 2 * x + y to make it a natural extension of Exercise 09 [04 Feb 2022]
Fixed the name of a typing rule in a proof tree, thanks to Jiayi Jeanette Zhu’s eagle eye [02 Feb 2022]
Adjusted Exercise 02, with more punctuation marks [30 Jan 2022]
Created [29 Jan 2022]