Those of you who know me are probably aware of this: I was a TA for CMU’s 15-150 Functional Programming course, and that experience is one that is near and dear to my heart and central to my college experience. I TA’d for three semesters total, with my last semester in junior spring (S19) also being when I was one of our head TAs.

Joining 15-150 staff changed my life. I loved my time there, and I loved teaching the material. Now that I’ve graduated and I’ve started working, I was looking back and musing about how much this course and the material used to mean to me.

It’s still something important, and so I wanted to revisit it. I like to think I know the material very well, but now that I’m not using it everyday, I’m starting to definitely feel holes forming in my knowledge. So I’d like to get all of it out there. Think of these as recitations. I’m hoping to go through all of the material I can still remember from the course, and hopefully this is helpful to any student out there looking for some material on functional programming. And also hopefully this is helpful to me, as I go and understand how my background in functional programming can help me be a better software engineer now that I’m out of the academic world. It’s been a bit of a difficult spot right now as I try to understand functional programming in a non-pure and practical sense, and one of my coworkers who has been very kind in mentoring me and answering questions has inspired me to delve into reconciling that. So here goes.

These write-ups and videos will be in SML, and feel free to send me feedback by email. All of these are from my course notes. I’m assuming that the reader has basic programming knowledge.

Video (TBD)

I’ll also record a video soon. I promise. I’ll link it here when it’s finished.

On to the write-up!

A bit about SML and some of my thoughts about functional programming

SML is a functional programming language you’ve probably never heard of (other examples of functional programming languages you might have seen around include OCaml or Haskell) – and that probably makes sense, as its popularity is mostly among compiler writers, theorem provers, and programming language theory researchers. Why is that? It has a fully formalized specification with its typing rules and operational semantics. A language’s typing rules explain how the language’s type system assigns types to different expressions. It’s the grammar rules you have to follow in order to construct a valid sentence in your language. In type theory, we describe a type system through a set of inference rules which explain how that assigning happens. In contrast to thinking of the language’s typing rules as the language’s grammar, operational semantics are the meaning of the language. They are the way in which properties such as correctness or safety of a program can be formally verified – for example, I could tell you, once given an expression in SML, what are the next valid steps you can take to evaluate the expression (compute its value). If you were to give me 3 + 4, I will tell you that the next step is to evaluate to 7 – this is an example of structural operation semantics, which will again use inference rules to describe the individual steps of computation that can take place. The type systems and the operational semantics are not two divorced ideas: an example of where these two could overlap is with the concept of something being type safe. In a type-safe language, if a program is well-typed, it will not cause run-time errors – so look, a guarantee about a program’s behavior that comes from its type system! As a fun fact, SML is proven to be type safe.

This seems like a lot of jargon. And honestly, for the average person, it probably is. But, it’s a great language to start with because it’ll branch very naturally into more complicated topics in type theory, programming languages, compilers, and much more. I’ll go with SML though because it’s what I know. I am by no means an expert in functional programming; I only know the course material well. I’d like to learn more. Hopefully we can learn together.

Some other quick things about SML that I won’t delve into (but is fun to share if you did know these topics right now) is that it is statically-typed and has type inference, , pattern-matching, eager evaluation, currying, algebraic types, exception handling, and parametric polymorphism. SML is not a completely pure functional language and does allow some side-effects – side-effects being when a function or expression modifies a state value outside of its local environment (an example of side-effects include modifying global variables, mutating an argument that was passed by reference, or performing I/O operations). Side-effects are very powerful constructs, but should be used carefully: it makes a program’s behavior depend on when certain operations took place and will complicate debugging. In most cases, when you fully understand any side-effects your program incurs, using state-modifying expressions is straightforward. In complicated cases though, such as debugging concurrent code, you’ll be left scratching your head in wild bewilderment over Heisenbugs. So, side-effects do exist in SML but we typically will avoid them.

When I was first learning about SML and functional programming, it wasn’t ever apparent to me exactly what functional programming was. So let’s talk about that briefly, because I think it helps frame one’s mindset when trying to tackle these topics. It’s a programming paradigm. A style of programming. In this style, we treat computation as the evaluation of expressions (mathematical functions) – this is in contrast to statements in imperative programming languages which express some action to be carried out. Thinking of our tasks in terms of functions will allow us to add abstractions, which will often give us elegant solutions. Functional programming also avoids creating side-effects, so calling a function with the same arguments will always give us the same result (as Einstein supposedly once said: “The definition of insanity is doing the same thing over and over again, but expecting different results” – so this is very sane behavior, is it not?). I’m not going to sit here and be preachy about side-effects, because they absolutely are powerful and useful tools. But eliminations to changes in state that don’t depend on the function’s input does make programs written in this style much more straightforward to understand. Ease of understanding is a very practical and crucial value that’s often understated in the software development world. This is a good thing.

I work as a software engineer, and I generally don’t ever program in SML. But, there are still aspects from the functional programming paradigm that I and others on my team use on a daily basis or see in other languages and can then quickly understand. I’d often have students who struggled with understanding why our course was useful especially if they didn’t plan on going down the hardcore PL theory route. To them, I’d say: learning functional programming is useful, because it will teach you how to be a better problem solver and a cleaner coder. It will give you solid foundations. I’m also trying to remind myself of this, so hopefully I’m also successful in proving to myself that this claim is true.

With that, let’s dive into some basics of SML.

Expressions

As I mentioned earlier, the basic unit in SML is an expression. An expression is different from an imperative statement (where an imperative statement conveys an intended action – expressions have no tie to instructions but are instead mathematical statements). Here are some examples of expressions:

• 3
• 3 + 7
• (3 + 7) * 10 div 3
• 100 div 0
• (3 + 7) * 10 / 3
• "100"
• "100" ^ "100"
• "100" + 100
• intToString 100
• if true then 3 else 5
• let val x = 3 in x + 5 end
• let val x = 3 in case x of 3 => 5 | _ => 10 end

Some of these expressions are more complicated than others. Anything which doesn’t include valid syntax such as lskjd30qjwrlaksdjlk or 3 dvi 0 is not a valid expression in SML.

Types

I mentioned earlier that SML is statically-typed. So, what this means is that the SML compiler will type-check all of your code at compile-type (and will also then fail to compile if it encounters any type errors). We also talked earlier about what being type-safe means, and since SML possesses that quality, a compiled SML program will never produce a type error. In contrast, C is not type-safe – with casting, we can enter areas where the compiler might have not noticed a type error (which also means C is statically-typed), but the program later crashes when running because of a type error.

So, let’s define what makes an expression in SML well-typed. Well, an expression in SML is well-typed if it doesn’t cause any type errors. I know, what a boring definition. But let’s dive a bit deeper into this.

At the first level, all values have a type – its type is the type that the value belongs to. So, for example, the value 0 has type int, and we would write this as 0 : int where e : t means the expression e has type t. From the examples given above, we then have:

• 3 : int
• "100" : string

The following types probably also make a lot of sense:

• (3 + 7) * 10 div 3 : int
• 100 div 0 : int
• "100" ^ "100" : string
• intToString 100 : string

Some of these are very straightforward and seem intuitive: for example, why 3 + 7 : int. But, let’s delve into details and understand how expressions beyond just values have their types. Let’s pretend to be a compiler trying to type-check an expression and consider intToString 100. The general pattern to the compiler will type-check an expression is it will recursively type-check its sub-expressions, and then figure out the type of the overall expression from the types of its sub-expressions (type-checking as a recursive construct matches neatly with the recursive structure of an abstract syntax tree). So, let’s try that.

1. This expression is an example of function application where intToString is a function and 100 is the argument.
2. Let’s look at intToString – it has type int -> string. This is a function type and follows the form t1 -> t2, where the function type has input type t1 and output type t2. In the case of int -> string, the input type is int and the output type is string. So, the input given to the function must be of type int, and the expression the function application evaluates to (function application here refers to applying arguments to a function) is of type string.
3. Let’s look at 100. It is a value of type int.
4. So, now we know the types of the two sub-expressions in this expression: intToString : int -> string and 100 : int. Let’s now look at the overall expression. There is a rule which describes how to type a function application: a function application e1 e2 (or alternatively, e1 (e2) – the parentheses are not necessary and we can just write the argument e2 right next to the function e1 to apply it) has type t2 if e1 : t1 -> t2 and e2 : t1. Let’s plug what we have into that rule. In intToString 100, we know that intToString (e1) has type int -> string (t1 -> t2) and 100 (e2) has type int (t1). Since the type int of 100 matches the input type of intToString, which is int in the overall type int -> string, we know that intToString 100 (e1 e2) has type string (t2).

Let’s also consider 3 + 7. This expression is also an example of function application as + is a function – it looks different because it is infixed. Essentially an infixed function is placed between its arguments as opposed to where its arguments follow after the function. So, for example, we write 3 + 4 instead of + 3 4 and put the operator between the operands. So, + is a function (an infixed one) of type int * int -> int (here, the * represents a tuple type – in SML, we pass in multiple arguments by applying a tuple to the function) and is read as a function type (or “arrow type” as it is sometimes called) has the input type of int * int, a singular tuple of two integers, and has an output type of int. We then have the types of the operands, 3 : int and 7 : int, and so therefore 3 + 7 : int following our function application typing rule. Finally, as a last example, 7 div 0 has type int because div : int * int -> int, 7 : int, and 0 : int just as before, again according to the function application typing rule.

Note that we did not have to evaluate an expression to determine its type. We did not have to know that 3 + 7 evaluated to 10 in order to understand that 3 + 7 : int. The only thing we need in order to figure out an expressions type is the type of its subexpressions, or if it is a value (like 3 or "hello"), its intrinsic type. Note that in this sense, types follow inductive rules – which reflects how you can define SML’s type system through a set of inference rules.

Consider "100" + 100. We know that + : int * int -> int, "100" : string, and 100 : int. So, the tuple being applied to + has type string * int, not int * int – so even though this is a function application, this fails the function application typing rule. Therefore this expression is not well-typed and the type-checker would raise an error.

There are more complicated expressions in SML that have other typing rules. For example, consider if true then 3 else 5. This control-flow pattern can be generalized as following if e1 then e2 else e3, where if e1 then e2 else e3 : t if e1 : bool, e2 : t, and e3 : t. So, let’s look at if true then 3 else 5. In this case, e1 is true, e2 is 3, and e3 is 5. It is true that e1 : bool, e2 : t, and e3 : t where t is the type int, so therefore this overall expression has type int. But, if true then 3 else "5" is not well-typed.

Here’s a summary of some common types, example of values of that type, and some functions that involve that type.

• int
  • Examples of values: ~2, ~1, 0, 1, 2
  • Examples of functions: + : int * int -> int, - : int * int -> int, * : int * int -> int, div : int * int -> int, ~ : int -> int
• real
  • Examples of values: 0.0, 1.1, ~1.1
  • Examples of functions: + : real * real -> real, -: real * real -> real, * : real * real -> real, / : real * real -> real
• string
  • Examples of values: "hello", ""
  • Examples of functions: ^ : string * string -> string, intToString : int -> string
• bool
  • Examples of values: true, false
  • Examples of functions: not : bool -> bool

Note that functions between ints and reals are overloaded except for division: div is the name of the division for ints, and / is the name of the function for reals. So, note that the example expression given earlier, (3 + 7) * 10 / 3 is actually not well-typed.

Evaluation and an example

First, let’s talk about values. They’ve been mentioned quite a few times and you probably have an intuitive sense of them, but let’s talk about them explicitly for a bit. Values are expressions. Not all expressions are values. Values are defined as expressions which cannot be evaluated any further (or by some semantics, evaluate to itself). Examples of values include 3, "hello", false, or ~1.1.

Note how we said earlier that type-checking did not involve evaluation expressions. So, for example, 100 div 0 is actually an expression which does not have a value: but, it is well-typed. In order to evaluate an expression, it must be well-typed. Expressions that are not well-typed cannot be evaluated, and therefore have no value. But, even if an expression is well-typed, it might not evaluate to a value.

Different expressions have rules on how to evaluate them. We’ll talk more about some more complicated examples later, but to start, SML expressions are eagerly evaluated. Essentially, all arguments that are applied to a function must be a value. When we consider 3 + (7 + 4), we do not pass 3 and 7 + 4 to + in the outer function; instead, we will apply 3 and 11 to +. So, we had to evaluate the sub-expressions in the expression first to values, and then apply those values – so SML “eagerly” evaluates its sub-expressions before applying them in overall expressions. This is in contrast to lazy evaluation, where an expression is not evaluated until it is called. For example, consider this function (this is an example of a function declaration which we’ll jump into later, but this function should be simple enough to follow along):

1
fun evaluateToTwo (x : int) : int = 2

Note that evaluateToTwo : int -> int and it takes an argument x : int, and… never uses it and evaluates to 2. Now, let’s consider two function applications of evaluateToTwo (3 div 0). Note that 3 div 0 : int, so this expression is well-typed and has type int.

First, let’s try to evaluate this eagerly. So, we have to first evaluate the function’s arguments to a value. But, when we try to evaluate 3 div 0, it raises an exception.

Second, let’s try to evaluate this eagerly. So, we step into the function body, 2, and we evaluate it (because we are now using this expression). 2 is a value, so the entire expression evalautes to 2.

So, this expression evaluates differently depending on whether the language eagerly evaluates or lazily evaluates. In conclusion, evaluation in SML goes from left-to-right and is eager, and we can only evalute well-typed expressions. Let’s go through one last simple example (mostly just to touch on the left-to-right part). In here, note that => means “steps to”.

1
2
3
4
(3 + 7) * (2 + 3)
=> 10 * (2 + 3)
=> 10 * 5
=> 50

There’s usually a distinction between “steps to (in one step)” or “steps to (in a finite number of steps)” and further breakdowns. I am honestly just being lazy and using => as the latter. We’ll go into this a bit more also when we talk about extensional equivalence and referential transparency.

Declarations

In addition to expressions, we can also create bindings through declarations. Bindings are couplings in our environment that will bind an expression (which is eagerly evaluated) to a variable. This is similar to the idea of variables in other languages, but the bindings that declarations make are immutable. We cannot “update” a variable in SML.

val

val is a keyword that lets us make declarations in the following way: val [variable] : [type] = [expression] where [variable] is the name of the variable you are declaring that has some type [type], and [expression] is the expression [variable] is being bound to. So, for example, we can do val x : int = 2 + 3. We represent bindings with the syntax [5/x], which means 5 is bound to the variable x.

Consider the let [declarations] in [expression] end syntax. This statement evaluates to the [expression] part with the bindings created in [declarations], but the scope of [declarations] is only in [expression]. What I mean by the scope of [declarations] is that the bindings created in [declarations] are only valid in [expression], and anywhere else they are invalid. Here’s an example:

1
2
3
let val x : int = 3 in x + 5 end
=> [3/x] x + 5
=> 8

But, if I later on have x + 6 after the above, there will be an error because the compiler will not know what the variable x is – because it is only in scope (or present in the environment) while we are in that [expression] block.

fun

We can create function declarations in SML with the fun keyword. Here’s an example of a function (it’s the factorial function)!

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

How this function works we’ll go into more next time (when we talk about pattern-matching), but in the meantime, this declaration binds the function value to the variable fact. So, fact : int -> int.

More examples of evaluation

Let’s look at the following function declaration and subsequent evaluation just to tie everything together.

1
fun addTwo (x : int) = x + 2

So, if we are evaluating the above, in a well-typed function application, we evaluate to the body of the function with the bindings created from applying the arguments to the parameters.

1
2
3
addTwo 5
=> [5 / x] x + 2
=> 7

I also said earlier that bindings are immutable. So, what happens if I do the following?

1
2
val x : int = 3
val x : int = 4

It doesn’t update x or bind values to that variable twice – instead, the second declaration shadows the earlier one. The earlier declaration still exists! It’s just been shadowed by the second one and isn’t accessible by any bindings that take place after the second declaration that collides with its namespace. Let’s make this a bit more complicated to see how that works.

1
2
3
4
5
6
7
val x : int = 3
fun addThree (y : int) = y + x
val a : int = addThree 3
val x : int = 4
fun addThreeAgain (y : int) = y + x
val b : int = addThree 3
val c : int = addThreeAgain 3

In this example, a has value 6 and c has value 7. But what about b? It has value 6, because at the time that addThree was declared, what was in scope is [3 / x], and when we create declarations, we also fold in any existing bindings at the time. To make this a bit clearer, I’ll rewrite the above with the bindings that are in-scope at that time:

1
2
3
4
5
6
7
val x : int = 3
[3/x] fun addThree (y : int) = [3/x] y + x
[3/x] val a : int = addThree 3
val x : int = 4
[4/x] fun addThreeAgain (y : int) = [4/x] y + x
[4/x] val b : int = addThree 3
[4/x] val c : int = addThreeAgain 3

But what happens in evaluating addThree 3 when declaring b is:

1
2
3
addThree 3
=> [3/x][3/y] y + x
=> 6