Lecture 2

Introduction

Let’s consider a simple definition of a (mathematical) function that takes a natural number as an argument and produces a natural number as a result. The function f is given by two equations:

f 0       = 1
f (n + 1) = (n + 1) * f n

A function is used by applying it to an argument. These equations define what is the result of applying f to an argument.

The equations are read top-to-bottom and left-to-right. This way the equations define a set of reduction rules. If an expression matches the left-hand side of an equation, it reduces to the right-hand side of that equation.

• f 0 reduces to 1 (we have defined f 0 to be 1)
• If m = n + 1, then f m reduces to (n + 1) * f n

We write e ~> e' to say that the expression e reduces (according to the specified rules) to e'.

Example. According to the given reduction rules we have the following reduction sequence:

f 3                    // n is 2 since 3 is 2 + 1
~> 3 * f 2
~> 3 * (2 * f 1)
~> 3 * (2 * (1 * f 0))
~> 3 * (2 * (1 * 1))
~> 6

Types, expressions, values

Programs in functional programming are expressions and programs are executed (evaluated) by reduction.

For example, f 3 is an expression. Furthermore, it is a reducible expression as it can take a step of reduction. It reduces to 3 * f 2 (which is again reducible).

Some expressions are called values. These are expressions that do not reduce any further. f 0 is not a value, but f 0 ~> 1 and 1 is a value. Expression evaluation terminates with a value.

We would like to exclude certain expressions from consideration. For example, we have seen the expression f 3 and we can evaluate it to a value. What about f f (i.e., f applied to f)? What about 3 3 (i.e., 3 applied to 3)?

F# (and many other languages) use a type system as the mechanism to exclude certain syntactically correct expressions.

Expressions and types are brought together by the typing relation which is denoted by the symbol :. We write e : t to say that the expression e is of type t. For example, 5 : int.

The type system is designed in such a way that for the expressions we wish to exclude (like f f) there exists no suitable type. In other words, for an undesirable expressions e there is no t such that e : t.

It is also true that 3 + 2 : int. The expression 5 is a value, but 3 + 2 is not. Intuitively, 5 is a value as there is nothing left to compute while 3 + 2 can still compute (perform the addition).

More formally, for every type there is a designated set of expressions that are values. These include the literals (0, true, "abc", 1.0, …) in the language.

Example. Which of the following expressions are values?

• 2 + 2 : int
• 4 : int
• 4 % 2 = 0 : bool
• 4 % 2 : int
• sqrt 2.0 : float

Type safety of a language

1. If e : t and e ~> e', then e' : t.

2. If e : t, then either e is a value, or there exists e' s.t. e ~> e'.

(1.) is called preservation and says that reduction (evaluation) steps preserve the type. In a type-safe language it is not possible to take an e : int, start evaluating it and end up with a value of type string as the result.

(2.) is called progress and says that a well-typed expression is either a value (nothing left to compute) or it can be further evaluated. Evaluation of a well-typed expression does not get stuck.

Variables

We can compute the area of a circle with radius 2.0 by evaluating the expression

3.14 * 2.0 * 2.0

We don’t want to write another program (expression) for computing the area for radius 3.0. Instead, we would like to capture the pattern of computing the area of a circle without referring to any concrete radius.

To allow this, expressions can contain “holes” into which we can plug in the concrete values for which we wish to compute the result. Such an expression for the area of a circle is

3.14 * r * r

If we plug in a value, say 2.0, to the holes named r we get

3.14 * 2.0 * 2.0

More formally, the “holes” are variables that occur in an expression.

The “plugging in” operation is called substitution. We write e[v/x] to denote the substitution of v for x in the expression e.

We only substitute into those variable occurrences that are free. The occurrences of the variable r in the expression 3.14 * r * r are considered free since there is nothing in that expression that introduces the variable r.

If e is the expression 3.14 * r * r, then e[2.0/r] is the expression

3.14 * 2.0 * 2.0

Note that once we substitute a value for a variable the variable occurrence disappears.

((3.14 * r * r)[2.0/r])[3.0/r]

is

(3.14 * 2.0 * 2.0)[3.0/r]

which is

3.14 * 2.0 * 2.0

Substitution has to be done consistently: every free occurrence of a variable must receive the same value. In other words, for the expression 3.14 * r * r, it is wrong to substitute 2.0 for the first r and 3.0 for the second r. To do that you can start with the expression 3.14 * r * s.

let expressions

The syntax of let expressions is

let x = e in e'

where x is an identifier, e is the binding expression and e' is the body expression.

The let expression declares a variable x with the scope e' and binds the variable to the expression e.

In the expression let x = e in e', the occurrences of x in e' (the body) are no longer free: they are bound by the let. Note that we did not say anything about the occurrences of x in e.

What does this mean for substitution? Recall that we only substitute into free occurrences. Thus, in any expression of the form let x = e in e' substituting for x has no effect on e'. In other words,

• (let x = e in e')[v/x] is let x = e[v/x] in e'
• (let x = e in e')[v/y] is let x = e[v/y] in e'[v/y]

A more concrete example:

(let x = y + 1 in x + y)[1/y]
~> let x = ((y + 1)[1/y]) in (x + y)[1/y]
~> let x = 1 + 1 in x + 1
~> let x = 2 in x + 1

(let x = x + 1 in x + y)[1/x]
~> let x = ((x + 1)[1/x]) in x + y
~> let x = 1 + 1 in x + y
~> let x = 2 in x + y

What is the meaning of a let expression? We describe the meaning of a let expression by saying how it is evaluated.

The main rule for evaluating a let is:

• let x = v in e' ~> e'[v/x] (for v value)

The other rule is for the case when the binding expression is not a value:

• If e ~> e'',
  then let x = e in e' ~> let x = e'' in e'

Together these rules say that to evaluate let x = e in e':

1. Evaluate e to a value v.
2. Substitute v for x in e'. That is e'[v/x].
3. Evaluate e'[v/x] to a value v'.
4. The result of the let expression is v'.

Here is a concrete example.

let r = 1.0 + 1.0 in 3.14 * r * r
~> let r = 2.0 in 3.14 * r * r
~> (3.14 * r * r)[2.0/r]
~> 3.14 * 2.0 * 2.0
~> 12.56

When is a let-expression well-typed? The typing rule for let is the following:

• If e : t and,
  assuming x : t, it is the case that e' : t',
  then (let x = e in e') : t'

Notice how e and x must be of the same type. Consider the evaluation rules. We evaluate e to a value v and then substitute that value for x. Hence e and x should be of the same type.

In F# we can replace the in keyword with a newline in which case the scope for the binding (the e') extends to the rest of the enclosing scope. A let expression requires the e' part (if it is missing, you will see “the block following this let is unfinished” error).

Compare (let x = 1) + 1 and (let x = 1 in x + x) + 1.

Shadowing

It is possible to have overlapping bindings for the same name (shadowing). What is the result of evaluating the following?

let r = 1.0 in r + let r = 2.0 in 3.14 * r * r

Every let x = ... binds a new variable. If the name happens to be the same as another variable currently in scope, then the new variable shadows the old one in the new scope. The old variable is still there in the surrounding scope.

Example. In the (sub)expression r + let r = 2.0 in 3.14 * r * r above, the let r = ... binds a new variable for its body 3.14 * r * r and this r is different from the r that is outside this let expression.

Recall that we only substitute into variables that are free (i.e., not bound in the given expression). The result of the substitution

(r + let r = 2.0 in 3.14 * r * r)[1.0/r]

is

1.0 + let r = 2.0 in 3.14 * r * r

because the first r is free and the two others are not (they are in the scope of let r = 2.0 in ...).

The result of the substitution is not

1.0 + let r = 2.0 in 3.14 * 1.0 * 1.0

let definitions

The keyword let is also used for making definitions. This construct does not have the in part.

For example, writing

let pi = 3.14

at the toplevel of the module defines pi to be 3.14.

Conditionals (if-then-else)

The conditional has the form

if b then e1 else e2

where b is the condition, e1 is the true branch and e2 is the false branch.

The entire conditional if b then e1 else e2 is an expression and can thus be used anywhere an expression is expected. This is different from many imperative languages where conditionals are statements.

1 + if true then 0 else 1

The evaluation of a conditional is dictated by the condition b. There are two main rules.

• if true then e1 else e2 ~> e1
• if false then e1 else e2 ~> e2

The third rule is for the case when the condition is not yet a value.

• if b ~> b'
  then if b then e1 else e2 ~> if b' then e1 else e2

Together these rules say that to evaluate a conditional if b then e1 else e2:

1. Evaluate b to a value v.
2. If v is true, evaluate e1 to a value v'.
   If v is false, evaluate e2 to a value v'.
3. The result of the if-then-else expression is v'.

An example.

if 5 % 2 = 0 then 1 + 1 else 2 + 2
~> if 1 = 0 then 1 + 1 else 2 + 2
~> if false then 1 + 1 else 2 + 2
~> 2 + 2
~> 4

The typing rule of an if-then-else expression is:

• If b : bool and e1 : t and e2 : t,
  then if b then e1 else e2 : t

Both branches of an if-then-else must have the same type and that is the type of the entire expression.

Recall preservation: evaluation steps preserve the type.

Note that while we had one evaluation rule for b = true and one for b = false, we have just one typing rule altogether.

Typing information is a static property of the program and type checking occurs before we run the program. Thus, we cannot know whether b will be true or false.

Tuples

A tuple is a language construct for grouping together values of different type. The syntax for a k-tuple is (e_1, ..., e_k).

The evaluation rule for tuples is the following:

• If e_i ~> e'_i, then

  (v_1, ..., v_{i-1}, e_i,  ..., e_k) ~>
  (v_1, ..., v_{i-1}, e'_i, ..., e_k)

Thus, to evaluate (e_1, ..., e_k) we must evaluate each e_i to a value v_i (that is e_i ~> v_i) and the result is (v_1, ..., v_k).

Note that this rule enforces a left-to-right evaluation order on the components of the tuple. To evaluate component e_i all components to its left have to be values.

Example:

(1 + 1, "a" + "b", true || false)
~> (2, "a" + "b", true || false)
~> (2, "ab", true || false)
~> (2, "ab", true)

The type of a tuple is the list of its component types where the list elements are separated by *.

• If t_1, …, t_k are types,
  then so is t_1 * ... * t_k.

The typing rule for tuples is:

• If e_1 : t_1, …, e_k : t_k,
  then (e_1, ..., e_k) : (t_1 * ... * t_k)

Note that the types

• t1 * (t2 * t3)
• t1 * t2 * t3
• (t1 * t2) * t3

are “almost” the same, but they are not equal. We cannot use one in place of another.

The type t1 * (t2 * t3) is a 2-tuple type where the second component happens to be a 2-tuple itself. The type t1 * t2 * t3 is a 3-tuple type.

Tuples are also known as product types.

Pairs

A 2-tuple is also called a pair. Thus, a pair of a string and an int is a value of type string * int.

"ab", 1 : string * int

Unit

The unit type can also be seen as a special case of tuples: it is a 0-tuple type (a tuple with 0 components). It is a type with exactly one value:

() : unit

Sequential composition

The sequential composition of expressions e and e' is e; e'. Read it as: e then e'. The ; is typically replaced with a semicolon.

The main evaluation rule for sequential composition is

• v; e' ~> e' (for v value)

The other rule is for the case where e is not a value.

• If e ~> e'',
  then e; e' ~> e''; e'

Together these rules say that to evaluate e; e':

1. Evaluate e to a value v.
2. Discard v.
3. Evaluate e' to a value v'.
4. v' is the result.

Example:

2 + 2; 1 + 1
~> 4; 1 + 1
~> 1 + 1
~> 2

Why evaluate the expression e in e; e' at all if are going to discard the result anyway? Sometimes we do not care about the result, we are interested in the side effect instead. For example, e might write something to a file.

Related: Why do certain functions produce a result of type unit?

The typing rule for sequential composition is:

• If e : t and e' : t',
  then (e; e') : t'.

Functions

Functions are things that take an input and produce an output. For example, a function that computes the length of a string takes something of type string as input and produces something of type int as output.

The simplest functions are anonymous: we don’t even need to give a name to a function, we only have to specify how the output (the result) is computed from the input. The syntax for creating an anonymous function is

fun x -> e

where x is the argument and e is the body of the function. Here is a concrete example.

fun r -> 3.14 * r * r

This describes how to compute the result from the given input: whatever the given input r is, the result is 3.14 multiplied by the square of the input.

Similarly to let, a function fun x -> e introduces the variable x for the body e. This means that the occurrences of x are not free in fun x -> e.

• (fun x -> x + y)[2/x] is fun x -> x + y
• (fun x -> x + y)[2/y] is fun x -> x + 2

We do not have any evaluation rules for expressions of the form

fun x -> e

as these are values. There is nothing left to evaluate in such an expression.

For any types s and t, s -> t is the type of functions from s to t.

The typing rule for functions is:

• If, assuming x : s, we have e : t,
  then (fun x -> e) : s -> t.

Note the double usage of ->: it is used in the expression fun x -> e and also in the type s -> t. The meaning of these two uses are different as on the left it constructs a function, but on the right it constructs the type of all functions from s to t.

Function application

Functions are used by applying them to arguments.

The main evaluation rule for function application is

• (fun x -> e) v ~> e[v/x] (for v value; recall that fun x -> e is also a value)

The two other rules are for the case where the function or the argument are not values

• If f ~> f', then f a ~> f' a
• If a ~> a', then (fun x -> e) a ~> (fun x -> e) a'

Together these rules say that to evaluate function application f a:

1. Evaluate f to a value, i.e., something of the form fun x -> e.
2. Evaluate a to a value v.
3. Substitute v for x in e.
4. Evaluate the expression e[v/x] to a value v'.
5. v' is the result.

Example:

(fun r -> 3.14 * r * r) (1.0 + 1.0) 
~> (fun r -> 3.14 * r * r) 2.0      
~> (3.14 * r * r)[2.0/r]             
~> 3.14 * 2.0 * 2.0                 
~> 12.56

The typing rule for function application is

• If f : s -> t and a : s,
  then f a : t

Consider the evaluation rules for function application and let-expressions.

let x = e in e'
~> let x = v in e'  // e ~> v
~> e'[v/x]


(fun x -> e') e
~> (fun x -> e') v   // e ~> v
~> e'[v/x]

Functions are values like any other. In particular, we can give them names:

let f = fun r -> 3.14 * r * r in f 2.0
~> (f 2.0)[(fun r -> 3.14 * r * r)/f]
~> (fun r -> 3.14 * r * r) 2.0

This creates a function that is only available for the body f 2.0. Similarly, we can do this at the toplevel by omitting the in part:

let f = fun r -> 3.14 * r * r

There is also a more concise syntax for giving a name to a function as a let-definition. Instead of

let circle = fun r -> 3.14 * r * r

we can write

let circle r = 3.14 * r * r

In other words, we move the argument to the left of = and to the right of = we leave only the body of the function.

We can also add type annotations to be explicit.

fun (r : float) -> 3.14 * r * r : float

let circle (r : float) : float = 3.14 * r * r

Evaluating a function application is still the same.

circle (1.0 + 1.0)
~> (fun r -> 3.14 * r * r) (1.0 + 1.0)
~> (fun r -> 3.14 * r * r) 2.0
~> (3.14 * r * r)[2.0/r]

Recursive definitions

We already saw the factorial function:

f 0       = 1
f (n + 1) = (n + 1) * f n

and how evaluation of, say, f 3 would progress. Note that it is a recursive definition: f (n + 1) is defined in terms of f itself.

To define a recursive function we need a mechanism to allow us to refer to the function that we are currently defining in the definition of that same function.

A possible definition of factorial in F# is

let rec fact n =
  if n = 0
  then 1
  else n * fact (n - 1)

The keyword rec is necessary. Otherwise the function fact we are defining is not in scope in the body of the function (in the else branch).

Here are some of the steps of evaluating fact 3.

fact 3
~> (if n = 0 then 1 else n * fact (n - 1))[3/n]
~> if 3 = 0 then 1 else 3 * fact (3 - 1)
~> if false then 1 else 3 * fact (3 - 1)
~> 3 * fact (3 - 1)
~> 3 * fact 2
~> ...
~> 3 * (2 * fact 1)
~> ...
~> 3 * (2 * (1 * fact 0))
~> 3 * (2 * (1 * (if n = 0 then 1 else n * fact (n - 1))[0/n]))
~> 3 * (2 * (1 * (if 0 = 0 then 1 else fact (0 - 1))))
~> 3 * (2 * (1 * (if true then 1 else fact (0 - 1))))
~> 3 * (2 * (1 * 1))
~> 6

When defining functions by recursion, we should try to formulate them in terms of base case(s) and step case(s). In the base case there is no recursive call. In the step case there is a recursive call.

For the definition of fact above, n = 0 is the base case as the result is just 1. If n <> 0, then there is a recursive call fact (n - 1).

In the step case we should think how to solve the problem given that we know the solutions to the smaller subproblems: I don’t know what fact n should be, but, if someone told me that fact (n - 1) is some number x, then I know that fact n should be n * x.

let rec fact n =
  if n = 0
  then 1
  else n * x // what is x?

We obtain the number x by doing a recursive call.

let rec fact n =
  if n = 0
  then 1
  else n * fact (n - 1)

To avoid infinite recursion, we should ensure that in the step case the recursive call takes us closer to the base case (so that the recursion eventually terminates). In the definition of fact, the recursive call in the step case, fact (n - 1), takes us closer to the base case, fact 0, but only when n > 0.

Mutually recursive definitions

If we define two functions like this

let rec foo x = ...
let rec bar y = ...

then bar can refer to foo in its body, but not the other way around (going top-to-bottom, when we are in the body of bar, foo is already defined).

We can define the two functions simultaneously by using the keyword and as follows:

let rec foo x = ...
and     bar y = ...

in which case both can refer to the other.

let rec foo x = x * bar (x - 1)

and     bar y = if y <= 0 then 1 else y + foo (y - 1)

Functions again

s -> t is the type of functions taking arguments of type s and producing results of type t. Both s and t can be any types. In particular, both can be function types themselves.

• If s is s1 -> s2, then s -> t is (s1 -> s2) -> t.
• If t is t1 -> t2, then s -> t is s -> (t1 -> t2).

The (binary) type constructor -> is right-associative:

s -> t -> u is syntactic sugar for s -> (t -> u).

s -> t -> u -> v is syntactic sugar for s -> (t -> (u -> v)).

Function application, on the other hand, associates to the left:

f a b is syntactic sugar for (f a) b.

f a b c is syntactic sugar for ((f a) b) c.

Formally, every function takes one argument. But since a function may return a function as a result, it gives the impression that we are applying a function to multiple arguments.

Example:

fun x -> (fun y -> x + y) : int -> int -> int

(fun x -> (fun y -> x + y)) 2
~> (fun y -> x + y)[2/x]
~> fun y -> 2 + y : int -> int

(fun y -> 2 + y) 3
~> (2 + y)[3/y]
~> 2 + 3
~> 5 : int

Thus:

(fun x -> (fun y -> x + y)) 2 3
~> (fun y -> 2 + y) 3
~> 5

fun x y -> x + y is just sugar for fun x -> (fun y -> x + y).

(fun x y -> x + y) 2 3
~> 5

If

f : S -> T -> U
s : S
t : T

then

f s t : U

Note that f s : T -> U which is why f s can be applied to t : T.

Pattern matching

There is a construct in F# that is somewhat similar to if-then-else conditionals but is more powerful. This is the match expression. The general idea is that we can match an expression against a list of patterns and what we do next depends on which pattern we match.

With if-then-else we have two patterns: true and false. With match we get to define the patterns.

For now, our matches will look similar to switch statements from other languages. In future lectures we will introduce additional language features that will make match much more useful.

The general form of a match is:

match e with
| p_1 [when c_1] -> e_1
...
| p_n [when c_n] -> e_n

Here the p_i are the patterns against which we match the expression e, the c_i are (optional) Boolean guards and e_i are the body expressions.

A simplified evaluation rule for

match v with
| p_1 [when c_1] -> e_1
...
| p_n [when c_n] -> e_n

where v is a value:

• If i is the smallest integer s.t. v matches the pattern p_i
  and the condition c_i evaluates to true,
  then match v with ... ~> e_i.

The other rule is for the case where e is not a value.

• If e ~> e',
  then match e with ... ~> match e' with ....

Here is a concrete example.

match 0 = 1 with
| true  -> "It was true!"
| false -> "It was false."
~>
match false with
| true  -> "It was true!"
| false -> "It was false."
~>
"It was false."

A simplified typing rule:

• If e : t,
  each p_i is a pattern for type t,
  each c_i : bool,
  and each e_i : u,
  then the entire match expression is of type u.

Why do we say that the evaluation and typing rules are simplified?

An important feature of the patterns p_i is that they can also introduce bindings. The bindings introduced by p_i are in scope only for the guard c_i and the body e_i.

If the pattern p_i matches, then what we evaluate next is not the guard c_i but

c_i[v_1/x_1]...[v_k/x_k]

where all the x_j, v_j pairs are the bindings introduced by the pattern p_i. Similarly, if this guard (with the substitutions) evaluates to true, then the result is not the body e_i but

e_i[v_1/x_1]...[v_k/x_k]

Our simplified typing rule also ignored the fact that patterns can introduce bindings.

The evaluation rules thus say that to evaluate match e with ...:

1. Evaluate e to a value v.
2. Find the first pattern p_i that matches v for which also the guard c_i (with the appropriate substitutions) evaluates to true.
3. Evaluate e_i (with the appropriate substitutions) to a value v_i.
4. v_i is the result of the match expression.

Consider the following example.

let foo p =
  match p with
  | (0, 0)                -> "Both zero"
  | (x, y) when x % 2 = 0 -> "x even, y is: " + string y
  | w                     -> "Whatever: " + string p

We have three patterns.

• The first pattern matches those pairs where both the first and second component are 0. It does not introduce any bindings.
• The second pattern matches any pair and binds x to the first component and y to the second component of p. (What is the scope of x and y?)
• The third pattern matches any pair and binds w to the pair p.

What is foo (1 + 1, 2 + 2)?

foo (1 + 1, 2 + 2)
~> foo (2, 4)
~> match (2, 4) with
   | (0, 0)                -> "Both zero"
   | (x, y) when x % 2 = 0 -> "x even, y is: " + string y
   | w                     -> "Whatever: " + string (2, 4)

The first pattern (0, 0) does not match. The second pattern matches and binds x to 2 and y to 4. To check the Boolean guard for this case we need to evaluate the following expression:

(x % 2 = 0)[2/x][4/y]
~> (2 % 2 = 0)[4/y]
~> 2 % 2 = 0
~> true

Thus the result is

match (2, 4) with
| (0, 0)                -> "Both zero"
| (x, y) when x % 2 = 0 -> "x even, y is: " + string y
| w                     -> "Whatever: " + string (2, 4)

~> ("x even, y is: " + string y)[2/x][4/y]
~> ("x even, y is: " + string y)[4/y]
~> "x even, y is: " + string 4
~> "x even, y is: 4"

Here is a non-example.

let s = 100

let isEqualTo100 x =
  match x with
  | s -> "Yes!"
  | _ -> "No."

What is isEqualTo100 1?

Any valid identifier can be used as a pattern. Identifiers are used in patterns for introducing bindings. If we do not refer to a variable that we bind in a pattern, then we can replace it with _. What we wrote above is equivalent to

let isEqualTo100 x =
  match x with
  | _ -> "Yes!"

Finally, here is the factorial function defined using patterns.

let rec fact n =
  match n with
  | 0  -> 1
  | n' -> n' * fact (n' - 1)

fact 3
~> match 3 with
   | 0  -> 1
   | n' -> n' * fact (n' - 1)
~> (n' * fact (n' - 1))[3/n']
~> 3 * fact (3 - 1)
~> ... 

We can also use patterns in let bindings.

let (x, y) = (1, 3)

Or in the parameters of a function.

let fst (x, y) = x
let snd (_, y) = y

Some operations on basic types

abs   : int -> int
(+)   : int -> int -> int
not   : bool -> bool
(&&)  : bool -> bool -> bool
(||)  : bool -> bool -> bool
float : int -> float

By writing a binary operator in parentheses we can use it as a (prefix) function. For example: 1 + 2 vs (+) 1 2.

Evaluation rules of &&:

• false && b2 ~> false
• true && b2 ~> b2
• if b1 ~> b1'
  then b1 && b2 ~> b1' && b2

Type aliases

Similarly to how we can give names to values using let, we can also give names to types.

type Position = int * int

This is just an alias. When we have

e : Position

then this really is

e : int * int

but the former might be more readable.

Type inference by example

What is the type of foo below? In other words, find a type U such that foo : U if such a type exists.

let foo x =
  let (i, b) = x in
  not b, i + 1

We can see that foo takes an argument x and thus it is a function. It must be that U = S -> T for some types S and T. Or, foo : S -> T.

Since x is the argument, we have x : S.

Furthermore, we can see that x is matched against a pattern for pairs, hence S must be of the form S1 * S2 with i : S1 and b : S2 for some types S1 and S2.

The result type T must be the type of not b, i + 1 (Why?) and thus T must be of the form T1 * T2 for some T1 and T2 with not b : T1 and i + 1 : T2.

We know that not : bool -> bool. For not b to type check it must be that b : bool. Since b : S2, we have S2 = bool. Since not b : T1 and not b : bool, we have T1 = bool.

We know that (+) : int -> int -> int. For i + 1 : int to type check, it must be that i : int. Since i : S1, we have S1 = int. Since i + 1 : T2 and i + 1 : int, we have T2 = int.

Putting things together, we started from

foo : U

and by analysing the definition of foo we made the following observations

U = S -> T
S = S1 * S2
T = T1 * T2
S2 = bool
T1 = bool
S1 = int
T2 = int

and thus

foo : int * bool -> bool * int