In my earlier post, I talked about the basic of SML syntax and tried to give a bit of a set-up about functional programming in general. It’s unclear to me how effective it was, so please send me feedback on how to improve or what wasn’t clear (I’m already rereading and musing about various things I think I could have included, or better ways to explain a concept). It’s also been a while since I taught, so as I’m writing these up I’m revisiting and reviewing topics myself.

Anyways, so here’s the next part. This will review and go a bit deeper into evaluation and two key topics, extensional equivalence and referential transparency, and then will introduce patterns and pattern-matching.

Video (TBD)

Yes, yes. One day.

On to the write-up!

Definitions

Evaluation (revisited)

We talked last time about expressions being the most basic “unit” in SML – and talked about how declarative programming differed from imperative programming in that these expressions were not instructions, but mathematical statements. Expressions may or not be well-typed, and well-typed expressions may or may not evaluate to a value. This evaluation generally takes place left-to-right and occurs eagerly. For example, 3 + 4 evaluates to 7, 3 div 0 has well-typed and has type int but does not evaluate to a value (instead, this expression raises an exception).

We used this syntax, =>, to notate “stepping to”. So, this is honestly god-awful to write in Markdown (as opposed to in LaTeX) but alas – let’s talk a bit more formally about this. We write e for some arbitrary expression in SML and v for some arbitrary value (which are also expressions!). And, we use the following:

• e =>_v v means that expression e evaluates to value v (here I’m using the symbol =>_v – I’m trying my best)
• e =>_1 e' means that expression e reduces to expression e' in 1 step
• e =>_k e' means that expression e reduces to expression e' in k steps
• e => e' means that expression e reduces to e' in 0 or more steps

What we mean by steps here is a step in operational semantics, and is not what the actual operations are in SML. We’ll mostly just write e => e' for reduction when we’re concerned with correctness (and not looking at complexity, as we won’t be concerned with the number of steps the reduction took).

We also talked about how a value was an expression, but an expression was not necessarily a value. Let’s also look here at the relationship between reduction and evaluation. If e =>_v v, then that implies that e =>_1 e' =>_1 ... =>_1 v and vice versa. Also, values evaluate to themselves in 0 steps – so, we can write v => v (trivially) but there is no such e where v =>_1 e.

Extensional Equivalence

Let me first give the formal definition of extensional equivalence. We say that two expressions, e and e' of the same type are extensionally equivalent whenever one of the following is true:

1. Evaluation of e produces the same value as the evaluation of e'.
2. Evaluation of e and e' both loop forever.
3. Evaluation of e raises the same exception as does the evaluation of e'.

Extensional equivalence is an equivalence relation on well-typed SML expressions of the same type. So, for example, 3 + 7 and 10 are extensionally equivalent. Extensional equivalence gives us the basis to make “equals-for-equals” claims – it makes intuitive sense why 3 + 7 and 3 + (3 + 4) evaluate to the same value, as one way to look at it is 7 and 3 + 4 essentially “function in the same way” and we can replace one expression for the other in a larger expression to have the same outcome. Note that this “equals-for-equals” intuitive substitution as we know is only possible in a world without side-effects.

Extensional equivalence is a concept that comes from set theory, and we’ll be using it quite a bit in these functional programming notes to talk about correctness and reason about our programs. We’ll use the symbol ~= to denote extensional equivalence.

Referential Transparency

That “equals-for-equals” concept I mentioned earlier has a name! It’s called referential transparency. The concept is that in a functional program, we can replace any expression with another extensionally equivalent one without affecting the value of the program.

We seemingly do this “equals-for-equals” substitution all the time, but extensional equivalence and referential transparency are powerful constructs despite how intuitive they are. They can be leveraged in program optimization and simplifying steps in order to write better and cleaner programs.

Referential transparency is a property which still does exist in the imperative world with side-effects – we just have to take those side-effects into account in addition to values in what we define “equivalent” to be. Because in a functional program with no side-effects, we can evaluate an expression more than once and get the exact same outcome every time. Additionally then, the order in which we evaluate expressions has no difference in the value of the program which makes employing and reasoning about parallel evaluation strategies much more straightforward.

Totality

Another property I want to introduce is totality. A function f : t -> t' is total if for all possible values v of type t, f v evaluates to a value. So, if a function raises an exception on some inputs or loops forever, it is not total – the division function, for example, is not total because it raises an exception when dividing by 0. Totality is a useful tool for talking about correctness, as we could justify some expression x + f y as reducing to a value if they are all appropriately typed and x and y are values and f is total.

Functions are values!

A function value consists of an anonymous lambda expression and an environment of bindings for any non-local variables that are used in the scope of the function. This combination of a lambda expression and environment is a closure. We then often bind these function values to variables with the fun keyword.

Patterns

A pattern is either a constant (e.g. 0, true), variable (e.g. x : int), wildcard (_), or a tuple of patterns. Patterns are linear (so each variable can only occur at most once) and are also recursively defined. Additionally, when we talk about datatype declarations, we’ll also see that datatype constructors applied to an argument is also another type of pattern.

Pattern-matching is the process by which a value matches a pattern, and the bindings this matching produces. Each pattern has a set of values that it matches with, and a value successfully matches a pattern if it is a member of that set. Additionally, different patterns also have special rules about what bindings occur with that matching.

• Constant patterns are matched by values that are that constant. For example, the pattern 0 will only match the value 0 (and trying to match 1 with the pattern 0 will fail).
• Variable patterns are matched by all values of the respective type, and will also bind the matched value to that variable. For example, matching 0 to x : int will succeed and also create the binding [0 / x]. All values of type int will match this pattern. Values not of that type, like true, will fail though.
• Wildcard patterns are matched by all values of its respective type like the variable pattern. However, wildcard patterns do not create any bindings.
• Tuples of patterns are then matched by tuples of respective values that match those patterns. So for example, (0, true) will match the pattern (0, x : bool).

Using Patterns

Functions

Patterns can be used in clausal function definitions. So, the general form of a function definition is:

1
2
3
4
(fn p1 => e1
  | p2 => e2
  ...
  | p_n => e_n)

So, such a function will have type t1 -> t2 if every pattern p_i matches type t1 and every expression e_i matches type t2. For example, (fn (x : int, y : int) => (x + 1) * (y - 1)) has type int * int -> int since (x + 1) * (y - 1) has type int assuming x and y are both of type int, so then the pattern (x, y) must match type int * int. Here I explicitly typed it, but if I didn’t and just wrote (fn (x, y) => (x + 1) * (y - 1)) this would still hold.

So then when evaluating the application of an argument to a function, we are actually pattern-matching. Note that we eagerly evaluate here as well, and we only apply values to patterns after we’ve reduced all expressions. We first evaluate the expression, then evaluate the argument, and if both of these evaluations produce values, the resulting expression (where v is some generic value)

1
2
3
4
(fn p1 => e1
  | p2 => e2
  ...
  | p_n => e_n) v

takes place by trying to match v which each pattern in order, starting with p1 and going to p_n. If the value matches a pattern and nothing prior, it will create any bindings according to that pattern and then reduce to the respective expression.

Note – if we apply an argument to a function and the value fails to match any of the function’s clauses (patterns), he evaluation results in a “non-exhaustive match failure”, an error raised at run-time.

Cases

I gave an example of cases in the last post, but I’ll visit them again now that we’ve discussed patterns. A case expression has the form

1
2
3
4
5
(case e of
  p1 => e1
| p2 => e2
...
| p_n => e_n)

Note that this is an expression, not a statement. A well-formed expression has a type and can be evaluated. A case expression is well-typed if the following holds:

• e is of type t and each p_1, …, p_n is also of type t
• e_1, …, e_n are all of some type t'

Then, the case expression has type t'. Similarly to earlier, the pattern-matching in the case expression also produces bindings that exist in the scope of each clause.

For example, case 3 of 0 => "hi" | x => "bye" | _ => "was this clause necessary?" will evaluate to [3 / x] "bye". Note that we didn’t evaluate to the first clause because trying to match 3 to 0 failed! If it did succeed (if the pattern was 0, note that this pattern-matching does not create any bindings whereas the variable pattern does). Additionally, the last clause is redundant because no value will fail to match the variable pattern but successfully match to the wildcard pattern. Also just to emphasize again: a wildcard pattern and variable pattern match the same set of values, but a variable pattern creates bindings whereas a wildcard pattern does not!

An example

We talked about the factorial function earlier. Let’s step through an example evaluation with it again.

1
2
fun fact 0 = 1
  | fact n = n * fact (n-1)

So, let’s look at fact 3. Note that when we evaluate this, we are first reducing the function and 3 to a value, and then trying to pattern-match. So, 3 will fail the pattern match to 0, but then succeed to n and also create the binding [3 / n] and reduce to the expression [3 / n] n * fact (n-1).

1
2
3
4
5
6
7
8
9
fact 3
~=[3 / n] n * fact (n-1)
~= 3 * fact 2
~= 3 * [2 / n] n * fact (n - 1)
~= 3 * 2 * fact 1
~= 3 * 2 * [1 / n] n * fact (n - 1)
~= 3 * 2 * 1 * fact 0
~= 3 * 2 * 1 * 1
~= 6