Lecture 2 — Types, expressions, values and functions

Last week's lightning tour gave an introduction to F#. This week we ask what do these basic constructs mean: how an expression is evaluated and what a type tells us about an expression.

Introduction

Here is the definition of a function f 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. We can read the above equations as specifying what is the result of applying f to an argument n.

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: What is the result of evaluating f 3? According to the definition of f 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

Notation

• Reduction. \(e \leadsto e'\) means that expression \(e\) reduces to \(e'\). In the traces we write the same thing as ~>
• Substitution. \(e[v/x]\) is the expression obtained from \(e\) by replacing the variable \(x\) with the value \(v\) (precisely which occurrences get replaced is the subject of the section on variables).
• Typing. \(e : t\) means that expression \(e\) is of type \(t\).

Rules consist of premises and conclusions. Whenever the premises hold, so does the conclusion. A rule without premises is an axiom.

\[\dfrac{\text{premise}_1 \qquad \text{premise}_2}{\text{conclusion}}\]

Keywords of F# are set in teletype inside the rules, e.g. \(\mathtt{if}\ b\ \mathtt{then}\ e_1\ \mathtt{else}\ e_2\), so that you can tell the program text from the metavariables \(b\), \(e_1\), \(e_2\) that stand for arbitrary expressions.

Types, expressions, values

Programs in functional programming are expressions and programs (expressions) are evaluated by reducing them.

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 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 also 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 : \mathtt{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 expression \(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

Two properties connect evaluation and typing.

Preservation. Reduction steps preserve the type:

\[\text{if } e : t \text{ and } e \leadsto e' \text{, then } e' : t.\]

In a type-safe language it is not possible to take an expression of type int, evaluate it and end up with a value of type string as the result.

Progress. A well-typed expression is either a value or can take a step:

\[\text{if } e : t \text{, then either } e \text{ is a value, or there exists } e' \text{ such that } e \leadsto e'.\]

Evaluation of a well-typed expression does not get stuck. Either we have the result (a value) or the expression can reduce further.

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

If we plug in 3.0, then we get

3.14 * 3.0 * 3.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 we can take 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. It binds the identifier (name) x to the result (value) of evaluating e and then evaluates e' with the binding.

Thus, we can think of a let expression as declaring a local variable x with the scope e' where the value of x is the result of evaluating 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. (This does 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,

• \((\mathtt{let}\ x = e\ \mathtt{in}\ e')[v/x]\) is \(\mathtt{let}\ x = e[v/x]\ \mathtt{in}\ e'\)
• \((\mathtt{let}\ x = e\ \mathtt{in}\ e')[v/y]\) is \(\mathtt{let}\ x = e[v/y]\ \mathtt{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 an axiom: once the binding expression is a value \(v\), the let disappears and \(v\) is substituted into the body.

\[\mathtt{let}\ x = v\ \mathtt{in}\ e' \;\leadsto\; e'[v/x] \qquad (v \text{ a value})\]

The other rule is for the case where the binding expression is not yet a value: then that expression takes a step.

\[\dfrac{e \leadsto e''} {\mathtt{let}\ x = e\ \mathtt{in}\ e' \;\leadsto\; \mathtt{let}\ x = e''\ \mathtt{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

The same expression in F# and the result of evaluating it.

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

12.56

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

\[\dfrac{e : t \qquad e' : t' \ \text{ assuming } x : t} {(\mathtt{let}\ x = e\ \mathtt{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 rest of the enclosing scope becomes the body expression (e'). A let expression requires the e' part. If it is missing, the compiler will tell you. Compare (let x = 1) + 1 and (let x = 1 in x + x) + 1. The first is rejected:

> (let x = 1) + 1;;

  (let x = 1) + 1;;
  -^^^

error FS0588: The block following this 'let' is unfinished. Every
code block is an expression and must have a result. 'let' cannot be
the final code element in a block. Consider giving this block an
explicit result.

The second is a let expression with a body, used inside a larger expression:

let letInline = (let x = 1 in x + x) + 1

3

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

So the whole expression evaluates to 1.0 + 12.56:

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

13.56

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 and pi is in scope after it.

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.

let ifInline = 1 + if true then 0 else 1

1

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

\[\mathtt{if}\ \mathtt{true}\ \mathtt{then}\ e_1\ \mathtt{else}\ e_2 \;\leadsto\; e_1 \qquad \mathtt{if}\ \mathtt{false}\ \mathtt{then}\ e_1\ \mathtt{else}\ e_2 \;\leadsto\; e_2\]

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

\[\dfrac{b \leadsto b'} {\mathtt{if}\ b\ \mathtt{then}\ e_1\ \mathtt{else}\ e_2 \;\leadsto\; \mathtt{if}\ b'\ \mathtt{then}\ e_1\ \mathtt{else}\ e_2}\]

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

let ifExample = if 5 % 2 = 0 then 1 + 1 else 2 + 2

4

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

\[\dfrac{b : \mathtt{bool} \qquad e_1 : t \qquad e_2 : t} {\mathtt{if}\ b\ \mathtt{then}\ e_1\ \mathtt{else}\ e_2 : 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 a fixed number of values. The syntax for a k-tuple is (e_1, ..., e_k).

The (simplified) evaluation rule for tuples is the following:

\[\dfrac{e_i \leadsto e_i'} {(v_1, \ldots, v_{i-1}, e_i, \ldots, e_k) \;\leadsto\; (v_1, \ldots, v_{i-1}, e_i', \ldots, 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 simplified 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)

let tupleExample = (1 + 1, "a" + "b", 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 * \cdots * t_k\).

The typing rule for tuples is:

\[\dfrac{e_1 : t_1 \qquad \cdots \qquad e_k : t_k} {(e_1, \ldots, e_k) : t_1 * \cdots * 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. This is visible in the values too:

let flat : int * int * int = 1, 2, 3
let nested : int * (int * int) = 1, (2, 3)

(1, (2, 3))

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:

let unitValue : 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 newline.

The main evaluation rule for sequential composition is that if the first expression is a value, then discard that and continue with the second expression.

\[v;\ e' \;\leadsto\; e' \qquad (v \text{ a value})\]

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

\[\dfrac{e \leadsto e''}{e;\ e' \;\leadsto\; 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

As code:

// Deliberate warning FS0020: discarding the result of `2 + 2` is the
// point of this example. The warning is quoted in the notes below.
let seqExample = 2 + 2; 1 + 1

2

The compiler accepts this, but it is suspicious of it: computing 2 + 2 and then throwing the answer away is usually a mistake, so it warns.

> let seqExample = 2 + 2; 1 + 1;;

  let seqExample = 2 + 2; 1 + 1;;
  ------------------^^^^^

warning FS0020: The result of this expression has type 'int' and is
implicitly ignored. Consider using 'ignore' to discard this value
explicitly, e.g. 'expr |> ignore', or 'let' to bind the result to a
name, e.g. 'let result = expr'.

val seqExample: int = 2

Why evaluate the expression e in e; e' at all if we 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. That is also why the compiler does not warn when the discarded value has type unit: a unit result signals that the result is not interesting and we likely evaluated it for its effect.

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

The typing rule for sequential composition is:

\[\dfrac{e : t \qquad e' : t'}{(e;\ e') : t'}\]

Functions

Functions 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 give a name to the 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 in the expression e in fun x -> e are not free.

• \((\mathtt{fun}\ x \rightarrow x + y)[2/x]\) is \(\mathtt{fun}\ x \rightarrow x + y\)
• \((\mathtt{fun}\ x \rightarrow x + y)[2/y]\) is \(\mathtt{fun}\ x \rightarrow 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 \rightarrow t\) is the type of functions from \(s\) to \(t\).

The typing rule for functions is:

\[\dfrac{e : t \ \text{ assuming } x : s} {(\mathtt{fun}\ x \rightarrow e) : s \rightarrow 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 functions from s to t.

Function application

Functions are used by applying them to arguments.

The main evaluation rule for function application: applying a function value to an argument value substitutes the argument into the body.

\[(\mathtt{fun}\ x \rightarrow e)\ v \;\leadsto\; e[v/x] \qquad (v \text{ a value; recall that } \mathtt{fun}\ x \rightarrow e \text{ is also a value})\]

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

\[\dfrac{f \leadsto f'}{f\ a \;\leadsto\; f'\ a} \qquad \dfrac{a \leadsto a'} {(\mathtt{fun}\ x \rightarrow e)\ a \;\leadsto\; (\mathtt{fun}\ x \rightarrow 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, i.e., e[v/x].
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

let applyExample = (fun r -> 3.14 * r * r) (1.0 + 1.0)

12.56

The typing rule for function application is

\[\dfrac{f : s \rightarrow t \qquad a : s}{f\ a : t}\]

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

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]

Both evaluate e to a value and substitute it for x in e'. The expression fun x -> e' is a valid expression on its own (without applying it to e). The let without e is not.

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 circleFun = 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. In the anonymous form the annotations go on the argument and on the body, fun (r : float) -> 3.14 * r * r : float, and in the definition form they go on the argument and after the argument list:

let circleAnnotated (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]
~> 12.56

let circleExample = circle (1.0 + 1.0)

12.56

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 factIf n =
    if n = 0
    then 1
    else n * factIf (n - 1)

The keyword rec is necessary. Otherwise the function we are defining is not in scope in the body of the function (in the else branch). If there happens to be an older definition of the same name in scope, that is what the body refers to — and F# Interactive, which lets you re-enter a definition under the same name, will happily accept it:

> let bar n = -n;;
val bar: n: int -> int

> let bar n = if n = 0 then 1 else n * bar (n - 1);;
val bar: n: int -> int

> bar 3;;
val it: int = -6

No error, no warning. Without rec, the bar in the body is the first bar, so bar 3 is 3 * (-2). In a file, the second definition would be reported as a duplicate — but the missing rec would be reported first, as an undefined name. (We named our factorial factIf here because a second version, using match, follows in the pattern-matching section; a file cannot define fact twice.)

Here are some of the steps of evaluating fact 3.

fact 3
~> (fun n -> if n = 0 then 1 else n * fact (n - 1)) 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

let fact3If = factIf 3

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)

let mutualExample = foo 3

9

(Follow the calls by hand: foo 3 ~> 3 * bar 2, and bar 2 needs foo 1, which needs bar 0.)

Functions again

\(s \rightarrow 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 \(s_1 \rightarrow s_2\), then \(s \rightarrow t\) is \((s_1 \rightarrow s_2) \rightarrow t\).
• If \(t\) is \(t_1 \rightarrow t_2\), then \(s \rightarrow t\) is \(s \rightarrow (t_1 \rightarrow t_2)\).

The (binary) type constructor \(\rightarrow\) is right-associative:

\[s \rightarrow t \rightarrow u \quad\text{is syntactic sugar for}\quad s \rightarrow (t \rightarrow u)\]

\[s \rightarrow t \rightarrow u \rightarrow v \quad\text{is syntactic sugar for}\quad s \rightarrow (t \rightarrow (u \rightarrow v))\]

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

\[f\ a\ b \quad\text{is syntactic sugar for}\quad (f\ a)\ b\]

\[f\ a\ b\ c \quad\text{is syntactic sugar for}\quad ((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

The intermediate result is a function. Binding it to a name and asking F# Interactive for its type shows the second arrow of int -> int -> int still waiting for its argument:

> let addTwo = (fun x -> (fun y -> x + y)) 2;;
val addTwo: (int -> int)

let addTwo = (fun x -> (fun y -> x + y)) 2

let addTwoExample = addTwo 3

5

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

let curryExample = (fun x y -> x + y) 2 3

5

If

\[f : S \rightarrow T \rightarrow U \qquad s : S \qquad t : T\]

then

\[f\ s\ t : U\]

Note that \(f\ s : T \rightarrow 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 expressive. This is the match expression. The general idea is that we match an expression against a list of patterns and what we do next depends on which pattern we match first.

As an analogy, with if-then-else we have two fixed patterns: true and false. With match we get to choose the patterns (and how many there are).

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.

Simplified evaluation rules for match:

\[\dfrac{v \text{ matches } p_i \qquad c_i \leadsto \mathtt{true}}{\mathtt{match}\ v\ \mathtt{with}\ \ldots \;\leadsto\; e_i} \qquad \dfrac{e \leadsto e'}{\mathtt{match}\ e\ \mathtt{with}\ \ldots \;\leadsto\; \mathtt{match}\ e'\ \mathtt{with}\ \ldots}\]

Simplified in what way? 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]\ldots[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]\ldots[v_k/x_k]\]

In other words

\(\mathtt{match}\ v\ \mathtt{with}\ \ldots \;\leadsto\; e_i[v_1/x_1]\ldots[v_k/x_k]\) when

• \(v\) matches \(p_i\) (smallest such \(i\))
• \(c_i[v_1/x_1]\ldots[v_k/x_k] \leadsto \mathtt{true}\)

where \(x_i \mapsto v_i\) are the bindings introduced by \(p_i\).

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:

\[\dfrac{e : t \qquad p_i \text{ a pattern for } t \qquad c_i : \mathtt{bool} \qquad e_i : u}{(\mathtt{match}\ e\ \mathtt{with}\ \ldots) : u}\]

Our simplified typing rule also ignores 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 classify 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 classify (1 + 1, 2 + 2)?

classify (1 + 1, 2 + 2)
~> classify (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"

let classifyExample = classify (1 + 1, 2 + 2)

"x even, y is: 4"

Here is a non-example. We want a function that tells whether its argument equals 100, and we already have a name for that number:

let s = 100

// Deliberate warning FS0026: the pattern `s` is a fresh binding, not a
// comparison with the `s` above. The warning is quoted in the notes below.
let isEqualTo100 x =
    match x with
    | s -> "Yes!"
    | _ -> "No."

let isEqualTo100Example = isEqualTo100 1

"Yes!"

isEqualTo100 1 answers "Yes!". Any valid identifier can be used as a pattern, and identifiers are used in patterns for introducing bindings: the s in the pattern is a new variable that matches anything and shadows the s defined above. The compiler sees that the second rule can then never be reached and says so:

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

    | _ -> "No.";;
  ----^

warning FS0026: This rule will never be matched

val isEqualTo100: x: 'a -> string

Read the inferred type as well: 'a -> string, a function that accepts an argument of any type — another sign that nothing is being compared with an int. 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)
~> ...

let fact3 = fact 3

6

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.

let prefixPlus = (+) 1 2

3

Evaluation rules of &&:

\[\mathtt{false}\ \mathtt{\&\&}\ b_2 \;\leadsto\; \mathtt{false} \qquad \mathtt{true}\ \mathtt{\&\&}\ b_2 \;\leadsto\; b_2 \qquad \dfrac{b_1 \leadsto b_1'} {b_1\ \mathtt{\&\&}\ b_2 \;\leadsto\; b_1'\ \mathtt{\&\&}\ b_2}\]

Evaluation rules of ||:

\[\mathtt{false}\ \mathtt{||}\ b_2 \;\leadsto\; b_2 \qquad \mathtt{true}\ \mathtt{||}\ b_2 \;\leadsto\; \mathtt{true} \qquad \dfrac{b_1 \leadsto b_1'} {b_1\ \mathtt{||}\ b_2 \;\leadsto\; b_1'\ \mathtt{||}\ b_2}\]

Compare these with the rules for function application. When the first operand of && is false, the second operand is never evaluated — the axiom throws it away. Is there a difference between b1 && b2 and (fun x y -> x && y) b1 b2? There is, and an argument that refuses to evaluate to a value makes it visible.

let shortCircuit = false && (failwith "evaluated!" : bool)

false

With the function, the argument is evaluated first — and evaluation stops with the exception:

> (fun x y -> x && y) false (failwith "evaluated!");;
System.Exception: evaluated!
   at <StartupCode$FSI_0010>.$FSI_0010.main@()
Stopped due to error

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 : \mathtt{Position}\) then this really is \(e : \mathtt{int} * \mathtt{int}\), but the former might be more readable.

let origin : Position = (0, 0)

(0, 0)

Type inference by example

What is the type of mystery below? In other words, find a type \(U\) such that \(\mathtt{mystery} : U\) if such a type exists.

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

We can see that mystery takes an argument x and thus it is a function. It must be that U = S -> T for some types S and T. Or, mystery : 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

mystery : U

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

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

and thus

mystery : int * bool -> bool * int

We inferred the type of mystery via this informal argument. The compiler includes a type inference algorithm to infer the omitted types (if possible). We can see that we reached the right conclusion with out informal argument.

> let mystery x =
    let (i, b) = x in
    not b, i + 1;;
val mystery: int * bool -> bool * int

let mysteryExample = mystery (1, true)

(false, 2)

Futher materials

Mandatory reading: Hansen & Rischel, chapters 1 and 2.