This week: what do they mean?

• What does a type tell us?
• How is an expression evaluated?

Typing rules and evaluation rules.

Rules have the following form where premises are above and conclusion is below the bar.

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

Program text in teletype, metavariables in italics: \(\mathtt{if}\ b\ \mathtt{then}\ e_1\ \mathtt{else}\ e_2\).

Some expressions do not reduce any further: the values. f 0 is not a value; 1 is.

Evaluation terminates with a value.

Not every expression is sensible. What is f f? What is 3 3?

A type system excludes certain syntactically correct expressions.

For every type, a designated set of expressions are its values (including the literals: 0, true, "abc", 1.0, …).

Which of the following are values?

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

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

\[\text{if } e : t \text{, then } e \text{ is a value, or } e \leadsto e' \text{ for some } e'.\]

Evaluation does not get stuck (append s : string to a function f : int -> int).

Well-typed programs don’t go wrong.

In e', occurrences of x are bound (no longer free) as the let introduces x. (Says nothing about e.)

Substituting for x does not touch e' as those occurrences are bound (but not those in e):

\((\mathtt{let}\ x = e\ \mathtt{in}\ e')[v/x]\)   is   \(\mathtt{let}\ x = e[v/x]\ \mathtt{in}\ e'\)

Binding expression is not yet a value: it takes a step.

\[\dfrac{e \leadsto e''}{\mathtt{let}\ x = e\ \mathtt{in}\ e' \;\leadsto\; \mathtt{let}\ x = e''\ \mathtt{in}\ e'}\]

1. Evaluate e to v.
2. Substitute v for x in e'.
3. Evaluate e'[v/x] to v'. The overall result is v'.

Note that e and x have the same type. Recall that the evaluation rule substitutes the value of e for x.

In F#, the keyword in may be replaced by a newline. Then the scope extends to the rest of the enclosing block.

Recall that we substitute into free occurrences of variables.

(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

The body of the let (since it introduces r) is not affected.

The result of evaluating (r + let r = 2.0 in 3.14 * r * r)[1.0/r] is 13.56.

One rule when 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}\]

1. Evaluate b to a value
2. Evaluate the branch dictated by b. The other branch is not evaluated.

Both branches have the same type, and that is the type of the whole expression.

Type information is static. Before we execute the program, we do not know whether b is going to be true or false.

Recall preservation: whichever evaluation rule applies, the type stays the same.

Tuples are also called product types.

The Cartesian product of two sets \(A\) and \(B\), denoted \(A \times B\), is the set of all ordered pairs \((a, b)\) where \(a \in A\) and \(b \in B\).

\[ A \times B = \{ (a, b) \mid a \in A \land b \in B \} \]

Example: \(\{ A, 2, 3, 4, 5, 6, 7, 8, 9, 10, J, Q, K \} \times \{ ♡, ♢, ♧, ♤ \}\).

Values are tuples of the form \((v_1, ..., v_k)\) where each \(v_i\) is a value.

The rule fixes a left-to-right order: to evaluate \(e_i\), everything to its left must already be a value.

t1 * (t2 * t3), t1 * t2 * t3 and (t1 * t2) * t3 are "almost" the same, but not equal.

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

unit is the 0-tuple type. It has exactly one value, ().

let unitValue : unit = ()

1. Evaluate e to a value v. Discard v.
2. Evaluate e' to a value v'. Final result: v'

Typing rule:

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

fun x -> e introduces the variable x with scope e (similar to let). Occurrences of x in e are no longer free.

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

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

No evaluation rules: fun x -> e is a value.

Note that there are two different arrows here.

• In fun x -> e, the -> constructs a function value.
• In s -> t, the -> constructs a function type.

Function or argument not yet a value: they take a step, function first.

\[\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'}\]

1. Evaluate f to fun x -> e.
2. Evaluate a to v.
3. Evaluate e[v/x].

If f : int -> bool and x : int, then f x : bool.

If f : int -> bool, then f "5" is a typing error. The function f expects an argument of type int but the provided argument is a string.

Typing errors are static.

In F#, the function f needs to be in scope in its definition. This requires the keyword rec.

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

Without rec, the factIf in the else branch is undefined (or worse, refers to something else).

Typically, we want the step case to take as "closer" to the base case. When we reach the base case, the recursion terminates.

In this example, we only move closer to the base case when n > 0.

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

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

// foo 3 = 9

With and: we define both simultaneously; each may refer to the other.

Application is left-associative:

\[f\ a\ b \quad\text{stands for}\quad (f\ a)\ b\]

Formally, every function takes one argument. The ability to return a function gives the impression of several arguments.

At the moment, for us it is essentially a switch.

\[\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}\]

Patterns \(p_i\) may introduce bindings that are in scope for \(c_i\) and \(e_i\).

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

• \(v\) matches \(p_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\).

(0, 0) — matches when both components zero, introduces no bindings.

(x, y) when … — matches any pair; binds x and y to first and second component. What is their scope?

w — any pair; binds w to the whole pair.

(0, 0) fails. (x, y) matches with x = 2, y = 4; the guard (x % 2 = 0)[2/x][4/y] ~> 2 % 2 = 0 ~> true.

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

mystery is a function. U = S -> T, x : S, and not b, i + 1 : T.

x matched against a pair pattern. S = S1 * S2, i : S1, b : S2.

Result is a pair: T = T1 * T2, not b : T1, i + 1 : T2.

not : bool -> bool, so T1 = bool and S2 = bool.

(+) : int -> int -> int, so T2 = int and S1 = int.