Preface
These are lecture notes for the "Programming Languages I" course at the University of Tübingen. These lecture notes have at some point started as a Scala version of a subset of the excellent book "Programming Languages: Application and Interpretation" by Shriram Krishnamurthi, but over the years they have been modified and extended considerably.
These lecture notes can be improved by your corrections, comments and amendments. Every page of these lectures notes comes with a link to the corresponding document hosted on Github in the top right corner. Please open a pull request for any changes that help us improve this script.
Klaus Ostermann
Introduction
Why are you here?
This is an advanced programming course that focuses on the design and semantics of programming languages. The goals of this course are:
- To change the way you solve problems in programming: By principled design, with a rich toolbox of abstract concepts, rather than by tinkering.
- Enable you to think beyond the currently fashionable programming languages.
- Enable you to evaluate and discuss programming languages in a principled way.
- To show you where computer languages come from and potential future directions.
- To demonstrate why languages should be regarded as the ultimate form of abstraction.
- To teach you how to recognize abstractions and how to turn them into a language design.
- Teach you different ways how to realize a language design and make it practically useful.
- To convey a sense of aesthetics in programming.
- To introduce you into one of the most beautiful theories in theoretical computer science.
- To turn you into a better programmer!
Non-goals of this course are:
- Learn X different programming languages. Rather, you'll learn to decompose a PL into its features and discuss the merits of the features independently of the concrete PL.
- Write parsers or implement full-fledged compilers (although we will touch some compiler issues).
- Turn you into an evangelist for a particular PL.
How will we get there?
We will typically explain language features in two steps. First, we'll give an informal introduction and discuss some examples to get some experience with it. Then we will distill the core of the feature into an executable interpreter. Later, when we have more experience in formalizing language design into interpreters, we will also use formal mathematical notation. We will not just present the design of these features as if it had appeared out of the blue sky. Rather, we will discuss the process and trade-offs (and potential mistakes and pitfalls) that led to these designs. We will also discuss how these features appear in various available programming languages. We will mainly use the programming language Scala to write interpreters. Scala is sufficiently powerful to allow concise and elegant interpreters; on the other hand, it is sufficiently mature and popular for industrial usage. It also has variants of many of the features we will discuss. The book by Krishnamurthi, on which we loosely base the first part of the course, uses a different language, Racket. You are also welcome to use Racket instead of (or in addition to) Scala. Racket embodies an important tradition of PL design that is worth knowing, hence we encourage you, independently of this course, to study it!
How we will study programming languages
Rather than use vague labels such as "object-oriented" or "functional", we will decompose languages into small features, similar to how matter can be explained and decomposed into atoms, cells into DNA fragments, or organisms into the biological taxonomy. In addition to the decomposition into small-grained features, we will use a conceptual technique called "desugaring" to distinguish essential from non-essential language parts and identify the core constructs of a language.
Topics for class discussion:
- How can programming languages be evaluated, classified and compared?
- Why are labels like "object-oriented", "declarative", or "functional" too coarse-grained to be useful?
- How can we turn programming language research into a science?
- What would you like to learn in this course? What are your expectations?
- Which programming languages do you know? Which features of these languages do you like or dislike, and why?
- Is the choice of programming language for a programming project significant?
- Are interpreters a good way to capture the meaning of a PL? How do they compare to informal descriptions, formal specifications, and compilers?
- How important is the syntax of a PL?
Scala Basics
The content of this chapter is available as a Scala file here.
val x = 2 + 2;
// x: Int = 4
// val für Konstanten
// def für Methoden
// var für Variablen
abstract class Person(val name: String) {
// String name
// val name: String
def sayHello = {
print("hello, " + name)
}
}
trait ByeBye {
def sayGoodbye = {
print("bye")
}
}
class Tillmann(name: String) extends Person(name) with ByeBye {
override def sayHello = {
print("hi")
}
}
object Me extends Tillmann("Tillmann")
trait UniPerson
case class Student(val matrikelnummer: Int) extends UniPerson
case class Professor(val fachgebiet: String) extends UniPerson
object PatternMatching {
def showUniPerson(p: UniPerson): String =
p match {
case Student(m) => "student nr " + m
case Professor(f) => "professor on " + f
}
def test = {
print(showUniPerson(Student(123)))
print(showUniPerson(Professor("programming languages")))
}
}
enum UniPersonEnum:
case StudentEnum(val matrikelnummer: Int)
case ProfessorEnum(val fachgebiet: String)
object PatternMatchingEnum {
import UniPersonEnum._
def showUniPerson(p: UniPersonEnum): String =
p match {
case StudentEnum(m) => "student nr " + m
case ProfessorEnum(f) => "professor on " + f
}
def test = {
print(showUniPerson(StudentEnum(123)))
print(showUniPerson(ProfessorEnum("programming languages")))
}
}
object AE {
// Abstract Syntax Tree
enum Exp:
case Num(n: Int)
case Add(lhs: Exp, rhs: Exp)
import Exp._
// Example
val onePlusEight = Add(Num(1), Add(Num(5), Num(3)))
// Interpreter
def eval(e: Exp): Int =
e match {
case Num(n) => n
case Add(lhs, rhs) =>
eval(lhs) + eval(rhs)
}
}
Arithmetic Expressions With Variables
The content of this chapter is available as a Scala file here.
Let us now consider an extension of the arithmetic expression language with variables. We do this by a new kind of expression, which we
call Identifier, or Id.
\[ \begin{array}{lclr} e & := & n & \textit{Numeric Literals} \\ & | & (e + e) & \textit{Addition} \\ & | & (e * e) & \textit{Multiplication} \\ & | & x & \textit{Identifier} \end{array} \]
object AEId {
enum Exp:
case Num(n: Int) extends Exp
case Add(lhs: Exp, rhs: Exp) extends Exp
case Mul(lhs: Exp, rhs: Exp) extends Exp
case Id(x: String) extends Exp
import Exp._
Here is a sample program written in this language, directly written down using constructors of the enum:
val test0 = Add(Mul(Id("x"), Num(2)), Add(Id("y"), Id("y")))
With a proper parser we could choose a syntax like x * 2 + y + y. We do not care much about concrete syntax and parsing, though.
That said, to make writing examples less verbose, Scala's implicits come to the rescue. Calls to implicit functions are inserted automatically by the compiler if they help to restore well-typedness. For instance, we can define
implicit def num2exp(n: Int): Exp = Num(n)
implicit def sym2exp(x: String): Exp = Id(x)
to lift integers and strings to expressions. Using these implicits, the example can be written as:
val test = Add(Mul("x", 2), Add("y", "y"))
To give meaning to identifiers, we use environments. Environments are mappings from identifiers (which we represent as strings) to values. In our simple language the only values are integers, hence:
type Env = Map[String, Int]
An evaluator (or interpreter) for this language takes an expression and an environment as parameter and produces a value - in this case
Int. This interpreter uses pattern matching over the constructors of enum Exp.
def eval(e: Exp, env: Env): Int = e match {
case Num(n) => n
case Id(x) => env(x)
case Add(l, r) => eval(l, env) + eval(r, env)
case Mul(l, r) => eval(l, env) * eval(r, env)
}
A different (and arguably more 'object-oriented') way to implement this evaluator would be to add an abstract eval method to an Exp
class and override it in all subclasses, each implementation corresponding to its corresponding case in the pattern match. The choice
between these alternatives matters, since they support different dimensions of extensibility.
We will mainly use the more functional style using pattern matching, because it matches better to the order in which we present these topics in the lecture. To try the example, we need a sample environment that gives values to the (free) variables in the sample expression.
The test environment also illustrates how Scala supports direct definitions of constant maps.
val testEnv = Map("x" -> 3, "y" -> 4)
We can automatically test our evaluator using assert:
val exa = eval(test, testEnv)
// exa: Int = 14
assert(eval(test, testEnv) == 14)
}
Internal Visitors
We will now learn a different way to encode algorithms that operate on expressions (like the evaluator). To this end, we will now use so-called "folds". Folds are well-known for lists, but the concept is more general and applies to arbitrary algebraic data types. We will present folds in such a style that they resemble visitors as known from the OO design pattern literature. They correspond to so-called "internal visitors" in which the traversal is encoded within the "accept" function. An internal visitor consists of one function for each syntactic construct of the language. It has a type parameter that determines the "return type" of invoking the visitor on an expression. This type parameter is used in all positions in which the original syntax specifies a subexpression. Internal visitors also correspond to a "bottom-up" traversal of the syntax tree.
object Visitors {
case class VisitorAE[T](num: Int => T, add: (T, T) => T)
The fold function below itself applies a visitor to an expression. Note that the recursion is performed in the fold function, hence all visitors are not recursive.
Also note that this design enforces that all algorithms specified via this visitor interface are compositional by design. This means that the recursion structure of the algorithm corresponds to the recursion structure of the expression. Put in another way, it means that the semantics (in terms of the meta-language) of a composite expression is determined by the semantics of the subexpressions; the syntax of the subexpressions is irrelevant.
Compositional specifications are particularly nice because they enable "equational reasoning": Subexpressions can be replaced by other subexpressions with the same semantics without changing the semantics of the whole.
enum ExpAE:
case NumAE(n: Int) extends ExpAE
case AddAE(lhs: ExpAE, rhs: ExpAE) extends ExpAE
import ExpAE._
def foldExp[T](v: VisitorAE[T], e: ExpAE): T = {
e match {
case NumAE(n) => v.num(n)
case AddAE(l, r) => v.add(foldExp(v, l), foldExp(v, r))
}
}
Here is our evaluator from above rephrased using the visitor infrastructure.
val evalVisitorAE = VisitorAE[Int](x => x, (a, b) => a + b)
We can of course restore the original interface of eval using foldExp:
def eval(e: ExpAE) = foldExp(evalVisitorAE, e)
Let's test whether it works.
val exaVisitorAE = eval(AddAE(AddAE(NumAE(1), NumAE(2)), NumAE(3)))
// exaVisitorAE: Int = 6
assert(exaVisitorAE == 6)
We can also apply other algorithms using visitors, such as counting the number of NumAE literals, or printing to a string:
val countVisitorAE = VisitorAE[Int](_ => 1, _ + _)
val printVisitorAE = VisitorAE[String](_.toString, "(" + _ + "+" + _ + ")")
}
Let's now try the same with the AE language with identifiers. It all works in the same way:
object AEIdVisitor {
import AEId._
case class Visitor[T](num: Int => T, add: (T, T) => T, mul: (T, T) => T, id: String => T)
val expVisitor = Visitor[Exp](Num(_), Add(_, _), Mul(_, _), Id(_))
val countVisitor = Visitor[Int](_ => 1, _ + _, _ + _, _ => 0)
val printVisitor = Visitor[String](_.toString, "(" + _ + "+" + _ + ")", _ + "*" + _, identity)
def foldExp[T](v: Visitor[T], e: Exp): T = {
e match {
case Num(n) => v.num(n)
case Add(l, r) => v.add(foldExp(v, l), foldExp(v, r))
case Mul(l, r) => v.mul(foldExp(v, l), foldExp(v, r))
case Id(x) => v.id(x)
}
}
def countNums(e: Exp) = foldExp(countVisitor, e)
val exaCount = countNums(test)
// exaCount: Int = 1
assert(exaCount == 1)
However, what about the evaluator? If we instantiate T = Int, then how can we access the environment? Insight: For evaluation, we must
instantiate T with a function type Env => Int! This way of transforming a multi-argument function into a single-argument
higher-order function is called currying.
val evalVisitor = Visitor[Env => Int](
env => _ ,
(a, b) => env =>
a(env) + b(env),
(a, b) => env =>
a(env) * b(env),
x => env =>
env(x))
}
Desugaring
The content of this chapter is available as a Scala file here.
Desugaring
You have already seen the basic structure of an interpreter by means of an interpreter for a language of arithmetic Exps:
object AE {
// Abstract Syntax Tree
enum Exp:
case Num(n: Int) extends Exp
case Add(lhs: Exp, rhs: Exp) extends Exp
import Exp._
// Example
val ex = Add(Num(1), Add(Num(5), Num(3)))
// Interpreter
def eval(e: Exp): Int =
e match {
case Num(n) => n
case Add(lhs, rhs) =>
eval(lhs) + eval(rhs)
}
}
In this lecture we want to study the technique of desugaring as a means to structure programming languages and decompose a language into a core language and syntactic sugar.
For illustration, consider the following proposed extensions to the language:
MultSub- Unary Negation
Extension number 1 is a good example for a core language extension. We have no way of expressing Mult in terms of the existing constructs
(if we had some looping construct we could express Mult as repeated Add but we do not have loops).
Hence we add this language construct to the (core) language:
object MAE {
// Abstract Syntax Tree
enum Exp:
case Num(n: Int) extends Exp
case Add(lhs: Exp, rhs: Exp) extends Exp
case Mult(lhs: Exp, rhs: Exp) extends Exp
import Exp._
// Example
val ex = Add(Num(1), Mult(Num(5), Num(3)))
// Interpreter
def eval(e: Exp): Int =
e match {
case Num(n) => n
case Add(lhs, rhs) => eval(lhs) + eval(rhs)
case Mult(lhs, rhs) => eval(lhs) * eval(rhs)
}
}
Let us now consider extension #2, Sub. One way to support sub is to add it to the core language, just like Mult:
object SMAE {
// Abstract Syntax Tree
enum Exp:
case Num(n: Int) extends Exp
case Add(lhs: Exp, rhs: Exp) extends Exp
case Mult(lhs: Exp, rhs: Exp) extends Exp
case Sub(lhs: Exp, rhs: Exp) extends Exp
import Exp._
// Example
val ex = Sub(Num(1), Mult(Num(5), Num(3)))
// Interpreter
def eval(e: Exp): Int =
e match {
case Num(n) => n
case Add(lhs, rhs) => eval(lhs) + eval(rhs)
case Mult(lhs, rhs) => eval(lhs) * eval(rhs)
case Sub(lhs, rhs) => eval(lhs) - eval(rhs)
}
}
However, another way of adding sub is to treat it as syntactic sugar using the fact that a - b = a + (-1 * b)
One way of expressing the desugaring is as a syntax transformation:
def desugarSMAE2MAE(e: SMAE.Exp): MAE.Exp = e match {
case SMAE.Exp.Num(n) => MAE.Exp.Num(n)
case SMAE.Exp.Add(lhs, rhs) => MAE.Exp.Add(desugarSMAE2MAE(lhs), desugarSMAE2MAE(rhs))
case SMAE.Exp.Mult(lhs, rhs) => MAE.Exp.Mult(desugarSMAE2MAE(lhs), desugarSMAE2MAE(rhs))
case SMAE.Exp.Sub(lhs, rhs) =>
MAE.Exp.Add(desugarSMAE2MAE(lhs),
MAE.Exp.Mult(MAE.Exp.Num(-1), desugarSMAE2MAE(rhs)))
}
With this desugaring in place, we do not need an interpreter for SMAE anymore; rather we can reuse the MAE interpreter:
val res = MAE.eval(desugarSMAE2MAE(SMAE.ex))
// res: Int = -14
If we had written other algorithms on MAE, or had proven properties of MAE, they'd be applicable to SMAE, too. Hence desugaring is a way of reusing code, proofs, ... . It is important, though, that the desugared language feature is gone after desugaring. For instance, a pretty printer would print the desugared code. A debugger would use the desugared code. This can be an important downside to desugaring. There are ways to avoid or mitigate these shortcomings, but they require additional work.
There is a second way of realizing desugaring which does not require the definition of a copy of the AST enums. We can desugar earlier, namely during the construction of the AST:
object SMAE2 {
// Abstract Syntax Tree
enum Exp:
case Num(n: Int) extends Exp
case Add(lhs: Exp, rhs: Exp) extends Exp
case Mult(lhs: Exp, rhs: Exp) extends Exp
object Exp:
def sub(e1: Exp, e2: Exp): Exp =
Add(e1, Mult(Num(-1), e2))
import Exp._
// Compared to SMAE, we only have to change upper case Sub by lower case sub
// when constructing examples.
val ex = sub(Num(1), Mult(Num(5), Num(3)))
// Interpreter - no case for sub needed
def eval(e: Exp): Int =
e match {
case Num(n) => n
case Add(lhs, rhs) => eval(lhs) + eval(rhs)
case Mult(lhs, rhs) => eval(lhs) * eval(rhs)
}
}
Let us now consider the third extension, unary minus. Here we have three choices:
- Add unary minus to the core language.
- Treat unary minus as syntactic sugar for the core language using
-x = (-1) * x. - Treat unary minus as syntactic sugar on top of the syntactic sugar using
-x = 0 - x.
We will use the third option to illustrate that one can build layers of syntactic sugar:
object USMAE {
// Abstract Syntax Tree
enum Exp:
case Num(n: Int) extends Exp
case Add(lhs: Exp, rhs: Exp) extends Exp
case Mult(lhs: Exp, rhs: Exp) extends Exp
object Exp:
def sub(e1: Exp, e2: Exp): Exp =
Add(e1, Mult(Num(-1), e2))
def unaryminus(e: Exp) = sub(Num(0), e)
import Exp._
// Compared to SMAE, we only have to change upper case Sub by lower case sub
// when constructing examples.
val ex = sub(unaryminus(Num(1)), Mult(Num(5), Num(3)))
// Interpreter - no case for sub needed
def eval(e: Exp): Int =
e match {
case Num(n) => n
case Add(lhs, rhs) => eval(lhs) + eval(rhs)
case Mult(lhs, rhs) => eval(lhs) * eval(rhs)
}
}
sub(unaryminus(Num(1)), Num(7))
sub(unaryminus(Num(1)), Num(7))
Num(-8)
sub(sub(Num(0), Num(1)), Num(7))
sub has to be desugared, too.
Add(Add(Num(0), Mult(Num(-1), Num(1))),
Mult(Num(-1), Num(7)))
Name Binding
The content of this chapter is available as a Scala file here.
import scala.language.implicitConversions
Name Binding
We want, step by step, to develop our primitive calculator language into a full-fledged PL.
One important milestone on this way is the ability to deal with names. While our previous language allowed expressions with identifiers
in them, it had no binders: Constructs that allow to give meaning to a new name.
In this variant of the language, called WAE, we introduce such a binder called "with" with which we can give an expression a name that
can be used in the body of the "with" expression. This intuition is captured in the definition of the With case below,
which extends our previous language.
We study this WAE language to better understand what names mean in programming languages, and how they can be implemented.
object Syntax {
enum Exp:
case Num(n: Int) extends Exp
case Add(lhs: Exp, rhs: Exp) extends Exp
case Mul(lhs: Exp, rhs: Exp) extends Exp
case Id(x: String) extends Exp
case With(x: String, xdef: Exp, body: Exp) extends Exp
}
import Syntax._
import Exp._
We use implicits again to make example programs less verbose.
implicit def num2exp(n: Int): Exp = Num(n)
implicit def string2exp(x: String): Exp = Id(x)
A first example program in WAE.
val test = With("x", 5, Add("x", "x"))
Note that we deal with two languages here:
- This Scala file with Scala code.
- Most of the functions work on programs written in the WAE language.
Most of the time, we concentrate on WAE, but sometimes, we also talk about Scala. We have not defined a concrete syntax for WAE, but it is a real language nevertheless. We sometimes use some made-up syntax for examples on the blackboard or in comments.
Substitution
Instead of dealing with identifiers as external entities as in AE, identifiers can now be defined within the language. This justifies a new treatment of identifiers. We will explain them in terms of substitution, a notion well-known informally from high school algebra. The idea is the following: The interpreter transforms the term
with (x = 5) {
x + x
}
into
5 + 5
before proceeding. That is, all occurrences of x have been replaced by 5.
Note that these two programs -- before and after the substitution -- are certainly not equal: They look quite different. However,
they are equivalent in the sense that when evaluated, they will produce the same number. Such transformations between different but
somehow equivalent programs are an important tool for the study of programs, and of programming languages. Often, if we know which
programs behave identically, we understand better how programs behave in general. We will see more examples of this in this lecture.
Hence, the implementation of the With-case of our interpreter should be something like:
case With(x, xdef, body) => eval(subst(body, x, Num(eval(xdef))))
for a function subst with signature
subst: (Exp, String, Num) => Exp
The type of the third parameter is Num instead of Exp because it is more difficult to get substitution correct when arbitrary
expressions can be inserted (accidential name capture problem, more about that later).
Since we want to experiment with different versions of substitution, we write the interpreter in such a way that we can parameterize
it with a substitution function:
def makeEval(subst: (Exp, String, Num) => Exp): Exp => Int = {
def eval(e: Exp): Int = e match {
case Num(n) => n
case Id(x) => sys.error("unbound variable: " + x)
case Add(l, r) => eval(l) + eval(r)
case Mul(l, r) => eval(l) * eval(r)
// take the Int and wrap it into a Num for substitution
case With(x, xdef, body) => eval(subst(body, x, Num(eval(xdef))))
}
eval
}
Substitution, take 1
To substitute identifier i in e with expression v, replace all identifiers in e that have the name i with the expression v.
Let's try to formalize this definition:
val subst1: (Exp, String, Num) => Exp = (e, i, v) => e match {
case Num(n) => e
case Id(x) => if (x == i) v else e
case Add(l, r) => Add(subst1(l, i, v), subst1(r, i, v))
case Mul(l, r) => Mul(subst1(l, i, v), subst1(r, i, v))
case With(x, xdef, body) => With(if (x == i) v else x,
subst1(xdef, i, v),
subst1(body, i, v))
}
Unfortunately this does not even type-check! And rightly so, because it might otherwise turn reasonable programs into programs that are not even syntactically legal anymore. Exercise for self-study: Find an expression that would be transformed into one that is not syntactically legal. To see the reason for this, we need to define some terminology (the word "instance" here means "occurence"):
Definition (Binding Instance): A binding instance of an identifier is the instance of the identifier that gives it its value. In WAE, the
xposition of aWithis the only binding instance.
Definition (Scope): The scope of a binding instance is the region of program text in which instances of the identifier refer to the value bound by the binding instance.
Definition (Bound Instance): An identifier is bound if it is contained within the scope of a binding instance of its name.
Definition (Free Instance): An identifier not contained in the scope of any binding instance of its name is said to be free.
Examples: In WAE, the String in Id("x") is a bound or free instance, and the String in With("x", ..., ...) is a binding instance.
The scope of this binding instance is the third sub-term of With.
Now the reason can be revealed. Our first attempt failed because we substituted the identifier occurring in the binding position in the
With-expression. This renders the expression illegal because after substitution the binding position where an identifier was expected
is now occupied by a Num.
To correct this mistake, we make another take at substitution:
Substitution, take 2
To substitute identifier i in e with expression v, replace all identifiers in e which are not binding
instances that have the name i with the expression v.
Here is the formalization of this definition.
val subst2: (Exp, String, Num) => Exp = (e, i, v) => e match {
case Num(n) => e
// Bound or free instance => substitute if names match
case Id(x) => if (x == i) v else e
case Add(l, r) => Add(subst2(l, i, v), subst2(r, i, v))
case Mul(l, r) => Mul(subst2(l, i, v), subst2(r, i, v))
// binding instance => do not substitute
case With(x, xdef, body) => With(x,
subst2(xdef, i, v),
subst2(body, i, v))
}
Let's create an interpreter that uses this substitution function.
def eval2 = makeEval(subst2)
assert(eval2(test) == 10) // it works!
val test2 = With("x", 5, Add("x", With("x", 3, 10))) // another test
assert(eval2(test2) == 15) // works as expected
val test3 = With("x", 5, Add("x", With("x", 3, "x"))) // another test
// assert(eval2(test3) == 8) // Bang! Result is 10 instead!
What went wrong here? Our substitution algorithm respected binding instances, but not their scope. In the sample expression, the With
introduces a new scope for the inner x. The scope of the outer x is shadowed or masked by the inner binding. Because substitution
doesn’t recognize this possibility, it incorrectly substitutes the inner x.
Substitution, take 3
To substitute identifier i in e with expression v, replace all non-binding identifiers in e having
the name i with the expression v, unless the identifier is in a scope different from that introduced by i.
val subst3: (Exp, String, Num) => Exp = (e, i, v) => e match {
case Num(n) => e
case Id(x) => if (x == i) v else e
case Add(l, r) => Add(subst3(l, i, v), subst3(r, i, v))
case Mul(l, r) => Mul(subst3(l, i, v), subst3(r, i, v))
case With(x, xdef, body) => With(x,
subst3(xdef, i, v),
// what if we forget to substitute into the body?
body)
}
def eval3 = makeEval(subst3)
assert(eval3(test) == 10)
assert(eval3(test2) == 15)
assert(eval3(test3) == 8) // Success!
val test4 = With("x", 5, Add("x", With("y", 3, "x")))
// assert(eval3(test4) == 10) // Bang! unbound variable: "x"
The inner expression should result in an error, because x has no value. Once again, substitution has changed a correct program into
an incorrect one!
Let’s understand what went wrong. Why didn’t we substitute the inner x? Substitution halts at the With because, by definition, every
With introduces a new scope, which we said should delimit substitution. But this With contains an instance of x, which we very much
want substituted! So which is it - substitute within nested scopes or not? Actually, the two examples above should reveal that our
latest definition for substitution, which may have seemed sensible at first blush, is too draconian: it rules out substitution within
any nested scopes.
Substitution, take 4
To substitute identifier i in e with expression v, replace all non-binding identifiers in e having
the name i with the expression v, except within nested scopes of i.
Finally, we have a version of substitution that works. A different, more succinct way of phrasing this definition is:
"To substitute identifier i in e with expression v, replace all free instances of i in e with v."
val subst4: (Exp, String, Num) => Exp = (e, i, v) => e match {
case Num(n) => e
case Id(x) => if (x == i) v else e
case Add(l, r) => Add(subst4(l, i, v), subst4(r, i, v))
case Mul(l, r) => Mul(subst4(l, i, v), subst4(r, i, v))
// do not substitute when shadowed
case With(x, xdef, body) => if (x == i) e
else With(x,
subst4(xdef, i, v),
subst4(body, i, v))
}
def eval4 = makeEval(subst4)
assert(eval4(test) == 10)
assert(eval4(test2) == 15)
assert(eval4(test3) == 8)
assert(eval4(test4) == 10) // Success!
val test5 = With("x", 5, With("x", "x", "x"))
// assert(eval4(test5) == 5) // Bang! unbound variable "x"
This program should evaluate to 5, but it too halts with an error. This is because we prematurely stopped substituting for x occuring in
a bound position. We should substitute in the named expression of a With even if the With in question defines a new scope for the identifier
being substituted, because its named expression is still in the scope of the enclosing binding of the identifier.
Substitution, take 5
We finally get a valid programmatic definition of substitution (relative to the language we have so far):
val subst5: (Exp, String, Num) => Exp = (e, i, v) => e match {
case Num(n) => e
case Id(x) => if (x == i) v else e
case Add(l, r) => Add(subst5(l, i, v), subst5(r, i, v))
case Mul(l, r) => Mul(subst5(l, i, v), subst5(r, i, v))
// handle shadowing correctly
case With(x, xdef, body) => With(x,
subst5(xdef, i, v),
if (x == i) body else subst5(body, i, v))
}
def eval5 = makeEval(subst5)
assert(eval5(test) == 10)
assert(eval5(test2) == 15)
assert(eval5(test3) == 8)
assert(eval5(test4) == 10)
assert(eval5(test5) == 5) // Success!
Summary
- Substitution can be used to understand the meaning of names in programming languages.
- Correct implementations of substitution need to handle free, bound, and binding instances of names and their scopes correctly.
First-Order Functions
The content of this chapter is available as a Scala file here.
First-Order Functions
In the last lecture we have seen how we can give commonly occuring (sub)expressions a name via the With construct. Often, however,
we can identify patterns of expressions that occur in many places, such as 5*5/2, 7*7/2 and 3*3/2, the common pattern
being x*x/2. In this case, the abstraction capabilities of With are not sufficient.
One way to enable more powerful abstractions are functions. Depending on the context of use and the interaction with other language
features (such as imperative features or objects), functions are also sometimes called procedures or methods.
Here we consider so-called first-order functions, that - unlike higher-order functions - are not expressions and can hence not be passed
to or be returned from other functions. First-order functions are simply called by name.
To introduce first-order functions, we need two new things: The possibility to define functions, and the possibility to call functions.
A call to a function is an expression, whereas functions are defined separately. Functions can have an arbitrary number of arguments.
The following definitions are the language we have analyzed so far together with the new language constructs for first-order functions:
object Syntax {
enum Exp:
case Num(n: Int) extends Exp
case Add(lhs: Exp, rhs: Exp) extends Exp
case Mul(lhs: Exp, rhs: Exp) extends Exp
case Id(x: String) extends Exp
case With(x: String, xdef: Exp, body: Exp) extends Exp
/** The new language constructs for first-order functions: */
case Call(f: String, args: List[Exp]) extends Exp // functions are called by name
object Exp:
/** The new language constructs for first-order functions: */
case class FunDef(args: List[String], body: Exp)
type Funs = Map[String, FunDef]
/** We use implicits again to make example programs less verbose. */
implicit def num2exp(n: Int): Exp = Num(n)
implicit def string2exp(x: String): Exp = Id(x)
}
import Syntax._
import Exp._
A function has a number of formal args and a body. Note that a first-order function also
has a name. To make the invariant that there can only be one function for each
name explicit, we have stored functions in the form of a map from function names to
FunDefs above.
The substitution for the new language is a straightforward extension of the former one.
def subst(e: Exp, i: String, v: Num): Exp = e match {
case Num(n) => e
case Id(x) => if (x == i) v else e
case Add(l, r) => Add(subst(l, i, v), subst(r, i, v))
case Mul(l, r) => Mul(subst(l, i, v), subst(r, i, v))
case With(x, xdef, body) => With(x,
subst(xdef, i, v),
if (x == i) body else subst(body, i, v))
case Call(f, args) => Call(f, args.map(subst(_, i, v)))
}
We will first study a "reference interpreter" based on substitution. We pass the map of functions as an additional parameter.
def eval(funs: Funs, e: Exp): Int = e match {
case Num(n) => n
case Id(x) => sys.error("unbound identifier: " + x)
case Add(l, r) => eval(funs, l) + eval(funs, r)
case Mul(l, r) => eval(funs, l) * eval(funs, r)
case With(x, xdef, body) => eval(funs, subst(body, x, Num(eval(funs, xdef))))
case Call(f, args) => {
val fd = funs(f) // lookup function definition
val vargs = args.map(eval(funs, _)) // evaluate function arguments
if (fd.args.size != vargs.size)
sys.error("number of paramters in call to " + f + " does not match")
// We construct the function body to be evaluated by subsequently substituting
// all formal arguments with their respective argument values.
// If we have only a single argument "fd.arg" and a single argument value "varg",
// the next line of code is equivalent to:
// val substbody = subst(fd.body, fd.arg, Num(varg))
val substbody = fd.args.zip(vargs).foldLeft(fd.body)((b, av) => subst(b, av._1, Num(av._2)))
eval(funs, substbody)
}
}
Is the extension really so straightforward? It can be seen in the last line of our
definition for subst that variable substitution deliberately ignores the function
name f. The substitution for f instead is handled separately inside eval.
We say in this case that function names and variable names live in different "name spaces".
An alternative would be to have them share one namespace. As an exercise, think about how
to support a common namespace for function names and variable names.
A test case:
val someFuns: Funs = Map("adder" -> FunDef(List("a", "b"), Add("a", "b")),
"doubleadder" -> FunDef(List("a", "x"), Add(Call("adder", List("a", 5)), Call("adder", List("x", 7)))))
val callSomeFuns = eval(someFuns, Call("doubleadder", List(2, 3)))
// callSomeFuns: Int = 17
assert(callSomeFuns == 17)
The scope of function definitions:
As can be seen in the example above, each function can "see" the other functions. We say that in this language functions have a global scope. Exercise: Can a function also invoke itself? Is this useful? We will now study an environment-based version of the interpreter. To motivate environments, consider the following sample program:
val testProg = With("x", 1, With("y", 2, With("z", 3, Add("x", Add("y", "z")))))
When considering the With case of the interpreter, the interpreter will subsequently produce and evaluate the following intermediate expressions:
val testProgAfterOneStep = With("y", 2, With("z", 3, Add(1, Add("y", "z"))))
val testProgAfterTwoSteps = With("z", 3, Add(1, Add(2, "z")))
val testProgAfterThreeSteps = Add(1, Add(2, 3))
At this point only pure arithmetic is left. But we see that the interpreter had to apply subsitution three times. In general, if the program size is n, then the interpreter may perform up to O(n) substitutions, each of which takes O(n) time. This quadratic complexity seems rather wasteful. Can we do better? We can avoid the redundancy by deferring the substitutions until they are really needed. Concretely, we define a repository of deferred substitutions, called environment. It tells us which identifiers are supposed to be eventually substituted by which value. This idea is captured in the following type definition:
type Env = Map[String, Int]
Initially, we have no substitutions to perform, so the repository is empty. Every time we encounter a construct (a With or an application Call)
that requires substitution, we augment the repository with one more entry, recording the identifier’s name and the value (if eager) or
expression (if lazy) it should eventually be substituted with. We continue to evaluate without actually performing the substitution.
This strategy breaks a key invariant we had established earlier, which is that any identifier the interpreter could encounter must be
free, for had it been bound, it would have already been substituted. Now that we’re no longer using the substitution-based model, we may
encounter bound identifiers during interpretation. How do we handle them? We must substitute them by consulting the repository.
def evalWithEnv(funs: Funs, env: Env, e: Exp): Int = e match {
case Num(n) => n
case Id(x) => env(x) // look up in repository of deferred substitutions
case Add(l, r) => evalWithEnv(funs, env, l) + evalWithEnv(funs, env, r)
case Mul(l, r) => evalWithEnv(funs, env, l) * evalWithEnv(funs, env, r)
case With(x, xdef, body) => evalWithEnv(funs, env + ((x, evalWithEnv(funs, env, xdef))), body)
case Call(f, args) => {
val fd = funs(f) // lookup function definition
val vargs = args.map(evalWithEnv(funs, env, _)) // evaluate function arguments
if (fd.args.size != vargs.size)
sys.error("number of paramters in call to " + f + " does not match")
// We construct the environment by associating each formal argument to its actual value
val newenv = Map() ++ fd.args.zip(vargs)
evalWithEnv(funs, newenv, fd.body)
}
}
val evalEnvSomeFuns = evalWithEnv(someFuns, Map.empty, Call("doubleadder", List(2, 3)))
// evalEnvSomeFuns: Int = 17
assert(evalEnvSomeFuns == 17)
In the interpreter above, we have extended the empty environment when constructing newenv. A conceivable alternative is to
extend env instead, like so:
def evalDynScope(funs: Funs, env: Env, e: Exp): Int = e match {
case Num(n) => n
case Id(x) => env(x)
case Add(l, r) => evalDynScope(funs, env, l) + evalDynScope(funs, env, r)
case Mul(l, r) => evalDynScope(funs, env, l) * evalDynScope(funs, env, r)
case With(x, xdef, body) => evalDynScope(funs, env + ((x, evalDynScope(funs, env, xdef))), body)
case Call(f, args) => {
val fd = funs(f)
val vargs = args.map(evalDynScope(funs, env, _))
if (fd.args.size != vargs.size)
sys.error("number of paramters in call to " + f + " does not match")
val newenv = env ++ fd.args.zip(vargs) // extending env instead of Map() !!
evalDynScope(funs, newenv, fd.body)
}
}
val evalDynSomeFuns = evalDynScope(someFuns, Map.empty, Call("doubleadder", List(2, 3)))
// evalDynSomeFuns: Int = 17
assert(evalDynSomeFuns == 17)
Does this make a difference? Yes, it does. Here is an example:
val funnyFun: Funs = Map("funny" -> FunDef(List("a"), Add("a", "b")))
val evalDynFunnyFun = evalDynScope(funnyFun, Map.empty, With("b", 3, Call("funny", List(4))))
// evalDynFunnyFun: Int = 7
assert(evalDynFunnyFun == 7)
Obviously this interpreter is "buggy" in the sense that it does not agree with the substitution-based interpreter. But is this semantics reasonable? Let's introduce some terminology to make the discussion simpler:
Definition (Static Scope): In a language with static scope, the scope of an identifier’s binding is a syntactically delimited region. A typical region would be the body of a function or other binding construct.
Definition (Dynamic Scope): In a language with dynamic scope, the scope of an identifier’s binding is the entire remainder of the execution during which that binding is in effect.
We see that eval and evalWithEnv give our language static scoping, whereas evalDynScope gives our language dynamic scoping.
Armed with this terminology, we claim that dynamic scope is entirely unreasonable. The problem is that we simply cannot determine what
the value of a program will be without knowing everything about its execution history. If a function f were invoked by some
sequence of other functions that did not bind a value for some parameter of f, then that particular application of f would result in an error, even though a
previous application of f in the very same program’s execution may have completed successfully! In other words, simply by looking at the
source text of f, it would be impossible to determine one of the most rudimentary properties of a program: whether or not a given
identifier was bound. You can only imagine the mayhem this would cause in a large software system, especially with multiple developers
and complex flows of control. We will therefore regard dynamic scope as an error. That said, there are facets of dynamic binding
that are quite useful. For instance, exception handlers are typically dynamically scoped: A thrown exception is dispatched to the
most recently encountered active exception handler for that exception type.
Higher-Order Functions
The content of this chapter is available as a Scala file here.
Higher-Order Functions
F1WAE, the language with first-order functions, lets us abstract over patterns that involve numbers. But what if we want to abstract over patterns that involve functions, such as the "list-fold" pattern, whose instantiations include summing or multiplying a list of integers?
To enable this kind of abstraction, we need to make functions "first-class", which means that they become values that can be passed to or returned from functions or stored in data structures. Languages with first-class functions enable so-called "higher-order functions", which are functions that accept or return a (possibly again higher-order) function.
We will see that this extension will make our language both simpler and much more powerful. This seeming contradiction is famously addressed by the first sentence of the Scheme language specification:
"Programming languages should be designed not by piling feature on top of feature, but by removing the weaknesses and restrictions that make additional features appear necessary."
The simplicity is due to the fact that this language is so expressive that many other language features can be "encoded", i.e., they do not need to be added to the language but can be expressed with the existing features.
This language, which we call "FAE", is basically the so-called "lambda calculus", a minimal but powerful programming language that has been highly influential in the design and theory of programming languages.
FAE is the language of arithmetic expressions, AE, plus only two additional language constructs: Function abstraction and function application.
object Syntax {
enum Exp:
case Num(n: Int)
case Id(name: String)
case Add(lhs: Exp, rhs: Exp)
// Both function definitions and applications are expressions.
case Fun(param: String, body: Exp)
case Ap(funExpr: Exp, argExpr: Exp)
object Exp:
implicit def num2exp(n: Int): Exp = Num(n)
implicit def id2exp(s: String): Exp = Id(s)
// "with" would be a better name for this function, but it is reserved in Scala
def wth(x: String, xdef: Exp, body: Exp): Exp = Ap(Fun(x, body), xdef)
}
import Syntax._
import Exp._
Due to the lambda calculus, the concrete syntax for function abstraction is often written
with a lambda, such as lambda x. x + 3, thus also called lambda abstraction. The Scala
syntax for lambda terms is (x) => x + 3, the Haskell syntax is \x -> x + 3.
The concrete syntax for function application is often either juxtaposition f a or
using brackets f(a). Haskell and the lambda calculus use the former, Scala uses the
latter.
The with construct is not needed anymore since it can be encoded using Ap and
Fun. For instance, with x = 7 in x + 3 can be encoded (using Scala syntax) as
((x) => x + 3)(7). We have made this idea explicit above by giving a constructive
translation. Remember that such translations are often called "desugaring".
As for F1WAE, we will at first define the meaning of FAE in terms of substitution. Here is the substitution function for FAE.
def subst0(e1: Exp, x: String, e2: Exp): Exp = e1 match {
case Num(n) => e1
case Add(l, r) => Add(subst0(l, x, e2), subst0(r, x, e2))
case Id(y) => if (x == y) e2 else Id(y)
case Ap(f, a) => Ap(subst0(f, x, e2), subst0(a, x, e2))
case Fun(param, body) =>
if (param == x) e1 else Fun(param, subst0(body, x, e2))
}
Let's try whether subst0 produces reasonable results.
assert(subst0(Add(5, "x"), "x", 7) == Add(5, 7))
assert(subst0(Add(5, "x"), "y", 7) == Add(5, "x"))
assert(subst0(Fun("x", Add("x", "y")), "x", 7) == Fun("x", Add("x", "y")))
Looks good. However, what happens if e2 contains free variables? The danger here is that they may be accidentially "captured" by the substitution.
For instance, consider
val subst0Test = subst0(Fun("x", Add("x", "y")), "y", Add("x", 5))
// subst0Test: Exp = Fun(
// param = "x",
// body = Add(
// lhs = Id(name = "x"),
// rhs = Add(lhs = Id(name = "x"), rhs = Num(n = 5))
// )
// )
The result is Fun("x", Add("x", Add("x", 5)))
This is not desirable, since it again violates static scoping.
Note that this problem did not show up in earlier languages, because there we only substituted variables by numbers, but not by
expressions that may contain free variables: The type of e2 was Num and not Exp.
Hence we are still not done with defining substitution. But what is the desired result of the substitution above?
The answer is that we must avoid the name clash by renaming the variable bound by the "lambda" if the variable name occurs free in e2.
This new variable name should be "fresh", i.e., not occur free in e2.
For instance, in the example above, we could first rename "x" to the fresh name "x0" and only then substitute, i.e.
subst(Fun("x", Add("x", "y")), "y", Add("x", 5)) == Fun("x0", Add("x0", Add("x", Num(5))))
Let's do this step by step.
def freshName(names: Set[String], default: String): String = {
var last: Int = 0
var freshName = default
while (names contains freshName) { freshName = default + last; last += 1; }
freshName
}
val freshNameExa1 = freshName(Set("y", "z"), "x")
// freshNameExa1: String = "x"
val freshNameExa2 = freshName(Set("x2", "x0", "x4", "x", "x1"), "x")
// freshNameExa2: String = "x3"
assert(freshNameExa1 == "x")
assert(freshNameExa2 == "x3")
def freeVars(e: Exp): Set[String] = e match {
case Id(x) => Set(x)
case Add(l, r) => freeVars(l) ++ freeVars(r)
case Fun(x, body) => freeVars(body) - x
case Ap(f, a) => freeVars(f) ++ freeVars(a)
case Num(n) => Set.empty
}
val freeVarsExa = freeVars(Fun("x", Add("x", "y")))
// freeVarsExa: Set[String] = Set("y")
assert(freeVarsExa == Set("y"))
def subst(e1: Exp, x: String, e2: Exp): Exp = e1 match {
case Num(n) => e1
case Add(l, r) => Add(subst(l, x, e2), subst(r, x, e2))
case Id(y) => if (x == y) e2 else Id(y)
case Ap(f, a) => Ap(subst(f, x, e2), subst(a, x, e2))
case Fun(param, body) =>
if (param == x) e1 else {
val fvs = freeVars(Fun(param, body)) ++ freeVars(e2) + x
val newvar = freshName(fvs, param)
Fun(newvar, subst(subst(body, param, Id(newvar)), x, e2))
}
}
assert(subst(Add(5, "x"), "x", 7) == Add(5, 7))
assert(subst(Add(5, "x"), "y", 7) == Add(5, "x"))
assert(subst(Fun("x", Add("x", "y")), "x", 7) == Fun("x", Add("x", "y")))
// test capture-avoiding substitution
assert(subst(Fun("x", Add("x", "y")), "y", Add("x", 5)) == Fun("x0", Add(Id("x0"), Add(Id("x"), Num(5)))))
assert(subst(Fun("x", Add(Id("x0"), Id("y"))), "y", Add(Id("x"), 5)) == Fun("x1", Add(Id("x0"), Add(Id("x"), Num(5)))))
OK, equipped with this new version of substitution we can now define the interpreter for this language. But how do we evaluate a function abstraction? Obviously we cannot return a number.
We realize that functions are also values! Hence we have to broaden the return type of our evaluator to also allow functions as values.
For simplicity, we use Exp as our return type since it allows us to return both numbers and functions. Later we will become more
sophisticated.
This means that a new class of errors can occur: A subexpression evaluates to a number where a function is expected, or vice versa. Such errors are called type errors, and we will talk about them in much more detail later.
For now, it means that we need to analyze (typically by pattern matching) the result of recursive invocations of eval to check whether the result has the right type.
The remainder of the interpreter is unsurprising:
def eval(e: Exp): Exp = e match {
case Id(v) => sys.error("unbound identifier: " + v)
case Add(l, r) => (eval(l), eval(r)) match {
case (Num(x), Num(y)) => Num(x + y)
case _ => sys.error("can only add numbers")
}
case Ap(f, a) => eval(f) match {
case Fun(x, body) => eval(subst(body, x, eval(a))) // call-by-value
// case Fun(x, body) => eval(subst(body, x, a)) // call-by-name
case _ => sys.error("can only apply functions")
}
case _ => e // numbers and functions evaluate to themselves
}
We can also make the return type more precise to verify the invariant that numbers and functions are the only values.
def eval2(e: Exp): Either[Num, Fun] = e match {
case Id(v) => sys.error("unbound identifier: " + v)
case Add(l, r) => (eval2(l), eval2(r)) match {
case (Left(Num(x)), Left(Num(y))) => Left(Num(x + y))
case _ => sys.error("can only add numbers")
}
case Ap(f, a) => eval2(f) match {
case Right(Fun(x, body)) => eval2(subst(body, x, eval(a)))
case _ => sys.error("can only apply functions")
}
case f@Fun(_, _) => Right(f)
case n@Num(_) => Left(n)
}
Let's test:
val test = Ap(Fun("x", Add("x", 5)), 7)
assert(eval(test) == Num(12))
FAE is a computationally (Turing-)complete language. For instance, we can define a non-terminating program. This program is commonly called Omega:
val omega = Ap(Fun("x", Ap("x", "x")), Fun("x", Ap("x", "x")))
// try eval(omega) to crash the interpreter ;-)
Omega can be extended to yield a fixed-point combinator, which can be used to encode arbitrary recursive functions. We'll come back to this topic later.
Let's now discuss what an environment-based version of this interpreter looks like. Here is a first attempt:
type Env0 = Map[String, Exp]
def evalWithEnv0(e: Exp, env: Env0): Exp = e match {
case Id(x) => env(x)
case Add(l, r) => {
(evalWithEnv0(l, env), evalWithEnv0(r, env)) match {
case (Num(v1), Num(v2)) => Num(v1 + v2)
case _ => sys.error("can only add numbers")
}
}
case Ap(f, a) => evalWithEnv0(f, env) match {
case Fun(x, body) => evalWithEnv0(body, Map(x -> evalWithEnv0(a, env)))
case _ => sys.error("can only apply functions")
}
case _ => e // numbers and functions evaluate to themselves
}
assert(evalWithEnv0(test, Map.empty) == Num(12))
However, consider the following example:
val test2 = wth("x", 5, Ap(Fun("f", Ap("f", 3)), Fun("y", Add("x", "y"))))
It works fine in the substitution-based interpreter,
val evalTest2 = eval(test2)
// evalTest2: Exp = Num(n = 8)
assert(evalTest2 == Num(8))
but
val evalEnv0Test2 = evalWithEnv0(test2, Map.empty)
// java.util.NoSuchElementException: key not found: x
// at scala.collection.immutable.Map$Map1.apply(Map.scala:243)
// at repl.MdocSession$MdocApp.evalWithEnv0(higher-order-functions.md:208)
// at repl.MdocSession$MdocApp.evalWithEnv0(higher-order-functions.md:210)
// at repl.MdocSession$MdocApp.evalWithEnv0(higher-order-functions.md:216)
// at repl.MdocSession$MdocApp.evalWithEnv0(higher-order-functions.md:216)
// at repl.MdocSession$MdocApp.evalWithEnv0(higher-order-functions.md:216)
// at repl.MdocSession$MdocApp.$init$$$anonfun$1(higher-order-functions.md:248)
// at repl.MdocSession$MdocApp.$init$$$anonfun$adapted$1(higher-order-functions.md:249)
yields a key not found: x error.
The problem is that we have forgotten the deferred substitutions to be performed in the body of the function.
What can we do to fix this problem?
We could try to replace the second line in the Ap case by
case Fun(x, body) => evalWithEnv0(body, env + (x -> evalWithEnv0(a, env)))
but this would again introduce dynamic scoping.
Hence, when we evaluate a function, we do not only have to store the function, but also the environment active when the function was created. This pair of function and environment is called a closure. The environment stored in the closure is used when the function is eventually applied.
Hint: If you cannot answer what a closure is and how it is used in the interpreter, you will be toast in the exam! Since closures are not expressible in the language syntax, we now come to the point where we need a separate category of values. The values in FAE can be either numbers or closures.
sealed abstract class Value
type Env = Map[String, Value]
case class NumV(n: Int) extends Value
case class ClosureV(f: Fun, env: Env) extends Value
The evaluator becomes:
def evalWithEnv(e: Exp, env: Env): Value = e match {
case Num(n: Int) => NumV(n)
case Id(x) => env(x)
case Add(l, r) => {
(evalWithEnv(l, env), evalWithEnv(r, env)) match {
case (NumV(v1), NumV(v2)) => NumV(v1 + v2)
case _ => sys.error("can only add numbers")
}
}
case f@Fun(param, body) => ClosureV(f, env)
case Ap(f, a) => evalWithEnv(f, env) match {
// Use environment stored in closure to realize proper lexical scoping!
case ClosureV(f, closureEnv) => evalWithEnv(f.body, closureEnv + (f.param -> evalWithEnv(a, env)))
case _ => sys.error("can only apply functions")
}
}
assert(evalWithEnv(test, Map.empty) == NumV(12))
assert(evalWithEnv(test2, Map.empty) == NumV(8))
Lazy Evaluation
The content of this chapter is available as a Scala file here.
Motivation for Lazy Evaluation
Read "Why Functional Programming Matters" by John Hughes available at https://www.cse.chalmers.se/~rjmh/Papers/whyfp.html.
What lazy evaluation means:
The choice of evaluation strategy is a purely semantic change that requires no change of the syntax. For this reason we reuse the syntactic definitions of FAE, hence load higher-order-functions.scala before executing this script. Before we discuss lazy evaluation, we will first discuss a related evaluation strategy, call-by-name.
Call-by-name can be explained very succintly in the substitution-based interpreter: Instead of evaluating the argument a in the
Ap case before substitution, we substitute the unevaluated argument into the body. The rest remains exactly the same.
def evalcbn(e: Exp): Exp = e match {
case Id(v) => sys.error("unbound identifier: " + v)
case Add(l, r) => (evalcbn(l), evalcbn(r)) match {
case (Num(x), Num(y)) => Num(x + y)
case _ => sys.error("can only add numbers")
}
case Ap(f, a) => evalcbn(f) match {
case Fun(x, body) => evalcbn(subst(body, x, a)) // no evaluation of a!
case _ => sys.error("can only apply functions")
}
case _ => e
}
Does this change the semantics, or is it just an implementation detail? In other words, is eval(e) == evalcbn(e) for all e ?
Let's try two former test cases.
assert(evalcbn(test) == eval(test))
assert(evalcbn(test2) == eval(test2))
One can formally prove that if eval and evalcbn both produce a number then the numbers are equal. Do they also agree if they produce
a function?
Not necessarily. Consider:
val test3 = Ap(Fun("f", Fun("x", Ap("f", "x"))), Add(1, 2))
assert(eval(test3) == Fun("x", Ap(Num(3), Id("x"))))
assert(evalcbn(test3) == Fun("x", Ap(Add(Num(1), Num(2)), Id("x"))))
However, if both produce a function, then the functions "behave" the same. More specifically, the function bodies produced by eval
may be "more evaluated" than those produced by evalcbn since for the latter the evaluation of the arguments substituted for the parameters
in the body is deferred. If we evaluated within function bodies (also called evaluation "under a
lambda") - which our interpreters do not do - we could produce the expression returned from eval from the expression returned by evalcbn.
This kind of equivalence is also called "beta-equivalence".
Most importantly, however, eval and evalcbn differ with regard to their termination behavior. We have seen that omega is a diverging
expression. In eval, the term
val test4 = Ap(Fun("x", 5), omega)
is hence also diverging. In contrast:
assert(evalcbn(test4) == Num(5))
Extra material: Infinite lists in FAE (not relevant for exam)
Using our call-by-name interpreter, we can express the same kinds of programming patterns that we have tried in Haskell, such as infinite lists.
We do not have direct support for lists, but we can encode lists. This kind of encoding is called Church encoding.
val nil = Fun("c", Fun("e", "e"))
val cons = Fun("x", Fun("xs", Fun("c", Fun("e", Ap(Ap("c", "x"), Ap(Ap("xs", "c"), "e"))))))
For instance, the list 1, 2, 3 is encoded as:
val list123 = Ap(Ap("cons", 1), Ap(Ap("cons", 2), Ap(Ap("cons", 3), "nil")))
The map function on lists becomes:
val maplist = Fun("f", Fun("l", Ap(Ap("l", Fun("x", Fun("xs", Ap(Ap("cons", Ap("f", "x")), "xs")))), "nil")))
For instance, we can map the successor function over the 1, 2, 3 list.
val test5 = wth("cons", cons,
wth("nil", nil,
wth("maplist", maplist,
Ap(Ap("maplist", Fun("x", Add("x", 1))), list123))))
Since it is somewhat difficult to print out the resulting list in our primitive language we construct the result we expect explicitly.
val test5res = wth("cons", cons,
wth("nil", nil,
Ap(Ap("cons", 2), Ap(Ap("cons", 3), Ap(Ap("cons", 4), "nil")))))
assert(eval(test5) == eval(test5res))
Using evalcbn instead of eval the assertion does not hold (why?), but the results are beta-equivalent.
We can also construct infinite lists. To this end, we need some form of recursion. We choose the standard fixed-point operator Y.
This operator only works under call-by-name or other so-called "non-strict" evaluation strategies.
val y = Fun("f", Ap(Fun("x", Ap("f", Ap("x", "x"))), Fun("x", Ap("f", Ap("x", "x")))))
Using Y, we can construct infinite lists, such as the list of all natural numbers.
val allnats = Ap(Ap("y", Fun("nats", Fun("n", Ap(Ap("cons", "n"), Ap("nats", Add("n", 1)))))), 1)
We can also perform standard computations on infinite lists, such as mapping the successor function over it.
val list2toinfty = wth("cons", cons,
wth("nil", nil,
wth("y", y,
wth("maplist", maplist,
Ap(Ap("maplist", Fun("x", Add("x", 1))), allnats)))))
Of course, list2toinfty diverges when we use eval, but it works fine with evalcbn. It is hard to verify the result due to
an almost unreadable output. Hence we propose the following
Exercise: Extend the language such that you can implement the "take" function as known from Haskell within the language
(if0-expressions or something like it are needed for that). Now add a "print" function that prints a number on the console.
Use it to display that the first 3 list elements of list2toinfty are 2, 3, 4.
end of extra material
Environment-based lazy evaluation
Let us now consider the question how we can implement call-by-name in the environment-based interpreter. Translating the idea of not evaluating the function argument to the environment-based version seems to suggest that the environment should map identifiers to expressions instead of values.
However, we run into the same problems that we had with first-class functions before we introduced closures: What happens to the deferred substitutions that still have to be applied in the function argument? If we discard the environment in which the function argument was defined we again introduce a variant of dynamic scoping.
Hence, like for closures, we need to store the environment together with the expression. We call such a pair a thunk. An environment thus becomes a mapping from symbols to thunks. Note that environments and thunks are hence mutually recursive. In Scala, we can hence not use type definitions of the form
type Thunk = (Exp, Env)
type Env = Map[String, Thunk]
Instead, we use a Scala class Env to express this recursion.
Since we want to experiment with different variants of how to generate and evaluate thunks we first create a parameterizable variant
of the evaluator that leaves open how to
- represent thunks (type
Thunk) - create thunks (method
delay) - evaluate thunks (method
force).
Hint: Research on the internet what abstract type members in Scala are. For instance, here.
trait CBN {
type Thunk
def delay(e: Exp, env: EnvThunk): Thunk
def force(t: Thunk): ValueCBN
case class EnvThunk(map: Map[String, Thunk]) {
def apply(key: String): Thunk = map.apply(key)
def +(other: (String, Thunk)): EnvThunk = EnvThunk(map + other)
}
// since values also depend on EnvThunk and hence on Thunk they need to
// be defined within this trait
sealed abstract class ValueCBN
case class NumV(n: Int) extends ValueCBN
case class ClosureV(f: Fun, env: EnvThunk) extends ValueCBN
def evalCBN(e: Exp, env: EnvThunk): ValueCBN = e match {
case Id(x) => force(env(x)) // force evaluation of thunk if identifier is evaluated
case Add(l, r) => {
(evalCBN(l, env), evalCBN(r, env)) match {
case (NumV(v1), NumV(v2)) => NumV(v1 + v2)
case _ => sys.error("can only add numbers")
}
}
case Ap(f, a) => evalCBN(f, env) match {
// delay argument expression and add it to environment of the closure
case ClosureV(f, cenv) => evalCBN(f.body, cenv + (f.param -> delay(a, env)))
case _ => sys.error("can only apply functions")
}
case Num(n) => NumV(n)
case f@Fun(x, body) => ClosureV(f, env)
}
}
Let's now create an instance of CBN that corresponds to the substitution-based call-by-name interpreter. A thunk is just a pair of expression and environment. Forcing a thunk just evaluates it in the stored environment. To understand what is going on during evaluation of tests we trace argument evaluation by a printout to the console.
object CallByName extends CBN {
type Thunk = (Exp, EnvThunk)
def delay(e: Exp, env: EnvThunk) = (e, env)
def force(t: Thunk) = {
println("Forcing evaluation of expression: " + t._1)
evalCBN(t._1, t._2)
}
}
assert(CallByName.evalCBN(test, CallByName.EnvThunk(Map.empty)) == CallByName.NumV(12))
// Forcing evaluation of expression: Num(7)
Call-by-need
Call-by-name is rather wasteful: If an argument is used n times in the body, the argument expression is re-evaluated n times. For instance, in
val cbntest = wth("double", Fun("x", Add("x", "x")),
Ap("double", Add(2, 3)))
the sum of 2 and 3 is computed twice. If the argument is passed again to another function, this may lead to an exponential blow-up.
Example:
val blowup = wth("a", Fun("x", Add("x", "x")),
wth("b", Fun("x", Add(Ap("a", "x"), Ap("a", "x"))),
wth("c", Fun("x", Add(Ap("b", "x"), Ap("b", "x"))),
wth("d", Fun("x", Add(Ap("c", "x"), Ap("c", "x"))),
wth("e", Fun("x", Add(Ap("d", "x"), Ap("d", "x"))),
wth("f", Fun("x", Add(Ap("e", "x"), Ap("e", "x"))),
Ap("f", Add(2, 3))))))))
Can we do better? Yes, by caching the value when the argument expression is evaluated for the first time. This evaluation strategy is called call-by-need.
Caching is easy to implement in Scala:
object CallByNeed extends CBN {
case class MemoThunk(e: Exp, env: EnvThunk) {
var cache: ValueCBN = null
}
type Thunk = MemoThunk
def delay(e: Exp, env: EnvThunk) = MemoThunk(e, env)
def force(t: Thunk) = {
if (t.cache == null) {
println("Forcing evaluation of expression: " + t.e)
t.cache = evalCBN(t.e, t.env)
} else {
println ("Reusing cached value " + t.cache + " for expression " + t.e)
}
t.cache
}
}
For instance, compare call-by-need and call-by-name in cbntest or blowup.
However, the meta-language (i.e., the subset of Scala features) used in the interpreter has become more complicated:
Since we are using mutation, the order of evaluation and aliasing of object references becomes important. Luckily, call-by-need agrees with call-by-name with regard to produced values and termination behavior, hence it is usually not necessary to reason about programs with the call-by-need semantics. If, however, one wants to reason about the performance of a program in a call-by-need setting, one has to take these additional complications into account. In practice, it is even worse, since languages like Haskell perform additional optimizations that, for instance, switch to call-by-value if an analysis can determine that an argument will definitely be used (look up "strictness analysis").
Topics for class discussion:
- Is it a good idea to mix a language with implicit mutation (such as Java, Scala, C++, Python, ...) with lazy evaluation?
- How can one simulate lazy evaluation in an eager language? Basic idea: 'Lambda' as evaluation firewall.
Recursive Functions
The content of this chapter is available as a Scala file here.
Recursion
Let's try to write a function that computes the sum of the first \( n \) integers. Let's pretend we do not know that the sum of the
first \( n \) integers is \( n * (n + 1) / 2 \) and instead compute the sum in a loop. Let's try to do this in FAE (with If0):
val sumattempt = wth("sum", Fun("n", If0("n", 0, Add("n", Ap("sum", Add("n", -1))))), Ap("sum", 10))
sumattempt won't work and yield an unbound identifier error (why?). An alternative would be to use a variant of the
y combinator to support recursion properly, but today we want to talk about direct support for recursion. More specifically,
we want a language construct Letrec that is similar to with, except that the bound String can be used in the expression
the String is bound to:
Letrec(x: String, e: Exp, body: Exp)
With this new construct our language looks like this:
object Syntax {
enum Exp:
case Num(n: Int)
case Id(name: String)
case Add(lhs: Exp, rhs: Exp)
case If0(cond: Exp, thenExp: Exp, elseExp: Exp)
case Fun(param: String, body: Exp)
case Ap(funExpr: Exp, argExpr: Exp)
case Letrec(x: String, e: Exp, body: Exp)
object Exp:
implicit def num2exp(n: Int): Exp = Num(n)
implicit def id2exp(s: String): Exp = Id(s)
def wth(x: String, xdef: Exp, body: Exp): Exp = Ap(Fun(x, body), xdef)
}
import Syntax._
import Exp._
Using Letrec, our example can be expressed as follows.
val sum = Letrec("sum", Fun("n", If0("n", 0, Add("n", Ap("sum", Add("n", -1))))), Ap("sum", 10))
Let's now consider the semantics of Letrec. Consider the evaluation of Letrec(x, e, body) in an environment env.
What environment should we use to evaluate e and body, respectively? Using env for e will produce a ClosureV(Fun("n", ..."sum"'...), env),
and hence the environment when evaluating body will be envbody = env + (x -> ClosureV(Fun("n", ..."sum"...), env)).
This is bad, because the env in the closure does not contain a binding for "sum" and hence the recursive invocation will fail.
The environment in the closure must contain a mapping for "sum". Hence envbody should look like
envbody = env + (x -> ClosureV(Fun("n", ..."sum"...),
env + ("sum" -> ClosureV(Fun("n", ..."sum"...), env)))
This looks better, but now the second closure contains an environment with no binding of "sum". What we need is an environment
that satisfies the equation:
envbody == env + (x -> ClosureV(Fun("n", ..."sum"..), envbody))
Obviously envbody must be circular. There are different ways to create such a circular environment. We will choose mutation to create
a circle. More specifically, we introduce a mutable pointer to a value class ValuePointer which will be initialized with a null pointer.
In the Letrec case, we put such a ValuePointer in the environment and evaluate the (recursive) expression in that environment.
Then we update the pointer with the result of evaluating that expression.
The only other change we need to make is to dereference a potential value pointer in the Id case. We deal with the necessary case
distinction by a polymorphic value method.
Due to the mutual recursion between ValueHolder and Value the definitions are put into an object.
object Values {
trait ValueHolder {
def value: Value
}
sealed abstract class Value extends ValueHolder { def value = this }
case class ValuePointer(var v: Value) extends ValueHolder { def value = v }
case class NumV(n: Int) extends Value
case class ClosureV(f: Fun, env: Env) extends Value
type Env = Map[String, ValueHolder]
}
import Values._ // such that we do not have to write Values.ValueHolder etc.
The interpreter is unchanged except for the additional Letrec case and the modified Id case.
def eval(e: Exp, env: Env): Value = e match {
case Num(n: Int) => NumV(n)
case Id(x) => env(x).value // dereference potential ValuePointer
case If0(cond, thenExp, elseExp) => eval(cond, env) match {
case NumV(0) => eval(thenExp, env)
case _ => eval(elseExp, env)
}
case Add(l, r) => {
(eval(l, env), eval(r, env)) match {
case (NumV(v1), NumV(v2)) => NumV(v1 + v2)
case _ => sys.error("can only add numbers")
}
}
case f@Fun(param, body) => ClosureV(f, env)
case Ap(f, a) => eval(f, env) match {
case ClosureV(f, closureEnv) => eval(f.body, closureEnv + (f.param -> eval(a, env)))
case _ => sys.error("can only apply functions")
}
case Letrec(x, e, body) => {
val vp = ValuePointer(null) // initialize pointer with null
val newenv = env + (x -> vp) // evaluate e in the environment extended with the placeholder
vp.v = eval(e, newenv) // create the circle in the environment
eval(body, newenv) // evaluate body in circular environment
}
}
The sum of numbers from 1 to 10 should be 55.
assert(eval(sum, Map.empty) == NumV(55))
// These test cases were contributed by rzhxeo (Sebastian Py)
var func = Fun("n", If0("n", 0, Ap("func", Add("n", -1))))
var test1 = Letrec("func", func, Ap("func", 1))
var test2 = Letrec("func", Ap(Fun("notUsed", func), 0), Ap("func", 1))
assert(eval(test1, Map()) == NumV(0))
assert(eval(test2, Map()) == NumV(0))
Mutation
The content of this chapter is available as a Scala file here.
Today we study mutation. More specifically, we want to equip our language with mutable data structures.
Typical mutable data structures in common languages include objects with mutable fields or structures/records in languages like C or Pascal. We will study a particularly simple mutable data structure: Boxes. In OO parlance, boxes can be thought of as an object with a single field that can be mutated. Despite their simplicity, boxes already illustrate all main issues associated with adding mutable state to a language.
A different and less interesting form of mutation is the mutability of variables, such as the possibility to assign something
to a 'local' variable bound via a lambda or with. We will not talk about mutable variables today.
We will add boxes to our base language, FAE.
object Syntax {
enum Exp:
case Num(n: Int)
case Id(name: String)
case Add(lhs: Exp, rhs: Exp)
case Mul(lhs: Exp, rhs: Exp)
case If0(cond: Exp, thenExp: Exp, elseExp: Exp)
case Fun(param: String, body: Exp)
case Ap(funExpr: Exp, argExpr: Exp)
/** To add mutation to FAE, we add four language constructs: */
case NewBox(e: Exp) // create a new box
case SetBox(b: Exp, e: Exp) // assign to a box
case OpenBox(b: Exp) // read value in a box
case Seq(e1: Exp, e2: Exp) // sequencing of expressions
object Exp:
implicit def num2exp(n: Int): Exp = Num(n)
implicit def id2exp(s: String): Exp = Id(s)
def wth(x: String, xdef: Exp, body: Exp): Exp = Ap(Fun(x, body), xdef)
}
import Syntax._
import Exp._
In this new language, the following sample program,
val test1 = wth("b", NewBox(0),
Seq(
SetBox("b", Add(1, OpenBox("b"))),
OpenBox("b")))
should give as result 1 in a proper implementation.
Let's consider how our interpreter could handle sequencing.
Here is an attempt:
case Seq(e1, e2) => {
eval(e1, env)
eval(e2, env)
}
This cannot be correct. As long as our interpreter does not use mutation, evaluation could not make any changes to the environment,
hence there is no way the evaluation of e1 could have any effect on the evaluation of e2.
In order to demostrate the actual nature of mutation, we will not use mutation in our meta-language to implement mutation in our object language. Thus, we will not use a mutable data structure to implement the environment in our interpreter. Instead, one may turn to the so-called environment-passing style, in which the interpreter returns also a possibly updated environment together with the computed value when it evaluates an expression. However, this solution does not always work. Consider the following example:
val test2 = wth("a", NewBox(1),
wth("f", Fun("x", Add("x", OpenBox("a"))),
Seq(SetBox("a", 2),
Ap("f", 5))))
The mutation should affect the box stored in the closure bound to f. But with the implementation strategy described above it would not.
Note that changing the value of a in the example is not a vialation of static scope. Scoping only says where an identifier is bound;
it does not say to what an identifier is bound, in particular, whether whatever bound to the identifier is fixed.
Indeed, the variable a is bound to the same box in both the static environment where the function f is created and the dynamic environment
where the function f is applied.
As before, when applying the function f to the argument 5, we can choose either
-
To use the static environment (where the variable
ais bound to a boxed 1) stored in the closure created forf. -
Or to use the dynamic environment (where the variable
ais bound to a boxed 2) present at the time of applyingf.
The first choice leads the program to evaluate to 6 rather than the expected 7. The second will record the change to the box, but it reintroduces dynamic scoping. So both choices do not work. Insight: We need two repositories of information. One, the environment, guards static scope.
sealed abstract class Value
type Env = Map[String, Value]
case class NumV(n: Int) extends Value
case class ClosureV(f: Fun, env: Env) extends Value
The other, which we call store, is tracking dynamic changes. Determining the value inside a box will become a two-step process: We first evaluate the box expression to an address, and then use the store to lookup the value stored at that address. We choose to represent addresses by integers.
type Address = Int
case class AddressV(a: Address) extends Value
type Store = Map[Address, Value]
We will often need a fresh address in the store. We do so using a counter variable.
var _nextAddress = 0
def nextAddress: Address = {
_nextAddress += 1
_nextAddress
}
Note: We promised to implement the interpreter without using mutation. Here we did use mutation, but this usage of mutation is not essential: we could instead just search for the largest address in the present store and add one to it. Let's now discuss the evaluation of FAE with conditionals and boxes, BCFAE. To this end, consider the following sample program:
val test3 = wth("switch", NewBox(0),
wth("toggle", Fun("dummy", If0(OpenBox("switch"),
Seq(SetBox("switch", 1), 1),
Seq(SetBox("switch", 0), 0))),
Add(Ap("toggle", 42), Ap("toggle", 42))))
This program should return 1. Let's discuss on the blackboard what the environment and store should look like during the evaluation of this program.
| ID | Exp | Value | Env | Store |
|---|---|---|---|---|
| A | wth(.. | "switch" -> . | 1 -> NumV(0) | |
| B | wth(.. | "toggle" -> .. | ||
| C | Add(.. | |||
| D | Ap("toggle") | 1 | 1 -> NumV(1) | |
| E | Ap("toggle") | 0 | 1 -> NumV(0) | |
| F | Add(1, 0) | 1 |
Insight: We must pass the current store in to evaluate every expression and pass the possibly updated store out after the evaluation. This is called store-passing style. Consequently, we have to update the type of our evaluator.
def eval(e: Exp, env: Env, s: Store): (Value, Store) = e match {
/* All expressions whose evaluation does not alter the store just return s. */
case Num(n) => (NumV(n), s)
case Id(x) => (env(x), s)
case f@Fun(_, _) => (ClosureV(f, env), s)
// In recursive cases we have to thread the store through the evaluation. In particular, we define the order of evaluation
// explicitly through data flow dependencies.
case If0(cond, thenExp, elseExp)
=> eval(cond, env, s) match {
case (NumV(0), s1) => eval(thenExp, env, s1)
case (_, s1) => eval(elseExp, env, s1)
/* An alternative that enfoces runtime type-correctness of
* the conditional expression:
case (NumV(_), s1) => eval(elseExp, env, s1)
case _ => sys.error("can only test if a number is 0") */
}
case Add(l, r)
=> eval(l, env, s) match {
case (NumV(v1), s1)
=> eval(r, env, s1) match {
case (NumV(v2), s2) => (NumV(v1 + v2), s2)
case _ => sys.error("can only add numbers")
}
case _
=> sys.error("can only add numbers")
}
case Mul(l, r)
=> eval(l, env, s) match {
case (NumV(v1), s1)
=> eval(r, env, s1) match {
case (NumV(v2), s2) => (NumV(v1 * v2), s2)
case _ => sys.error("can only multiply numbers")
}
case _ => sys.error("can only multiply numbers")
}
case Ap(f, a)
=> eval(f, env, s) match {
case (ClosureV(f, closureEnv), s1)
=> eval(a, env, s1) match {
case (av, s2)
=> eval(f.body, closureEnv + (f.param -> av), s2)
}
case _ => sys.error("can only apply functions")
}
// In a sequence, we ignore the result of evaluating e1 but not its effect on the store.
case Seq(e1, e2) => eval(e2, env, eval(e1, env, s)._2)
// A new box is created by putting it into the store at a new address.
case NewBox(e: Exp)
=> eval(e, env, s) match {
case (v, s1) => {
val a = nextAddress
(AddressV(a), s1 + (a -> v))
}
}
// Setting a box is now a two-step process: First evaluate b to an
// address, then lookup and update the value associated to the
// address in the store. Note that "updated" is a functional method.
case SetBox(b: Exp, e: Exp)
=> eval(b, env, s) match {
case (AddressV(a), s1)
=> eval(e, env, s1) match {
case (ev, s2) => (ev, s2.updated(a, ev))
}
case _ => sys.error("can only set boxes")
}
// OpenBox uses the same two-step process but does not update the
// store.
case OpenBox(b: Exp)
=> eval(b, env, s) match {
case (AddressV(a), s1) => (s1(a), s1)
case _ => sys.error("can only open boxes")
}
}
Freeing Memory
From an implementation point of view, our interpreter has the problem that nothing is ever removed from the store. One possibility would be to add an operation "removeBox" or the like to the language, but this would lead to dangling pointers and all the problems associated with manual memory management.
Our model of stores is sufficient to illustrate how modern languages often deal with memory management: by garbage collection. Garbage collectors automatically reclaim memory that is no longer referenced from within the active part of the computation. We can model a (naive) mark-and-sweep garbage collector as follows:
def gc(env: Env, store: Store): Store = {
def allAddrInVal(v: Value): Set[Address] = v match {
case AddressV(a) => Set(a)
case NumV(_) => Set.empty
case ClosureV(f, env) => allAddrInEnv(env)
}
def allAddrInEnv(env: Env): Set[Address] =
env.values.map(allAddrInVal _).fold(Set.empty)(_ union _)
def mark(seed: Set[Address]): Set[Address] = {
val newAddresses = seed.flatMap(ad => allAddrInVal(store(ad)))
if (newAddresses.subsetOf(seed)) seed
else mark(seed union newAddresses)
}
val marked = mark(allAddrInEnv(env)) // mark ...
store.view.filterKeys(marked(_)).toMap // and sweep!
}
val teststore = Map(
6 -> NumV(42),
7 -> NumV(6),
8 -> AddressV(6),
9 -> AddressV(7),
10 -> ClosureV(Fun("x", "y"), Map("y" -> AddressV(8)))
)
/*
10 -> 8 -> 6
9 -> 7 */
assert(gc(Map("a" -> AddressV(10)), teststore) == teststore - 7 - 9)
Note that garbage collectors only approximate the set of semantically disposable store entities. Even with garbage collectors, applications may very well suffer from memory leaks. The approximation should be safe, in the sense that a datum is never reclaimed when it is used by subsequent computations.
Furthermore, it must reclaim enough garbage to be actually useful. Reachability has turned out to be a rather useful (and sound) approximation of semantic disposability. Garbage collectors must also be efficient. Efficiency of GC is a huge research topic that we are not going to discuss. One efficiency problem with garbage collectors based on reachability that we want to mention is the "stop-the-world" phenomenon.
Garbage Collection
The content of this chapter is available as a Scala file here.
Let us now consider a more accurate modeling of garbage collection (gc). This time, we will use a mutable store instead of a functional store, because our purpose is not to explain mutation but to explain gc.
This is the well-known syntax of our language: FAE with boxes.
enum Exp:
case Num(n: Int)
case Id(name: String)
case Add(lhs: Exp, rhs: Exp)
case Mul(lhs: Exp, rhs: Exp)
case If0(cond: Exp, thenExp: Exp, elseExp: Exp)
case Fun(param: String, body: Exp)
case Ap (funExpr: Exp, argExpr: Exp)
case NewBox(e: Exp)
case SetBox(b: Exp, e: Exp)
case OpenBox(b: Exp)
case Seq(e1: Exp, e2: Exp)
object Exp:
implicit def num2exp(n: Int): Exp = Num(n)
implicit def id2exp(s: String): Exp = Id(s)
def wth(x: String, xdef: Exp, body: Exp): Exp = Ap(Fun(x, body), xdef)
import Exp._
We will equip our values with a mutable flag that is useful for mark-and-sweep garbage collection. In real systems it is implemented as a bit flag, or, if the so-called "tri-color algorithm" is used, with two bit flags.
abstract class Value {
var marked: Boolean = false
}
We will also use a mutable map instead of a map for environments. This is not needed for mark-and-sweep, but for copying garbage collectors such as Cheney's semi-space garbage collection algorithm.
type Env = scala.collection.mutable.Map[String, Value]
case class NumV(n: Int) extends Value
case class ClosureV(f: Fun, env: Env) extends Value
case class AddressV(a: Int) extends Value
To be able to experiment with different store and gc designs, we create an interface for stores.
The stack parameter in malloc is needed during gc to determine the root nodes from which the algorithms can start.
trait Store {
def malloc(stack: List[Env], v: Value): Int
def update(index: Int, v: Value): Unit
def apply(index: Int): Value
}
In our interpreter, the stack of environments is only implicitly available on the stack of the meta-language. To reify the call-stack we need to make it explicit. We do so by constructing the stack explicitly and passing it as parameter. The first element of the stack is the current environment; the rest is only needed for gc.
def eval(e: Exp, stack: List[Env], store: Store): Value = e match {
case Num(n) => NumV(n)
case Id(x) => stack.head(x)
case f@Fun(_, _) => ClosureV(f, stack.head)
/* With a mutable store, we do not have to thread it according to
* the order of evaluation any more.
*/
case If0(cond, thenExp, elseExp)
=> eval(cond, stack, store) match {
case NumV(0) => eval(thenExp, stack, store)
case _ => eval(elseExp, stack, store)
}
/* The mutable store allows us to take advantage of Scala's
* evaluation order and perform two pattern matchings
* simultaneously.
*/
case Add(l, r)
=> (eval(l, stack, store), eval(r, stack, store)) match {
case (NumV(v1), NumV(v2)) => NumV(v1 + v2)
case _ => sys.error("can only add numbers")
}
case Mul(l, r)
=> (eval(l, stack, store), eval(r, stack, store)) match {
case (NumV(v1), NumV(v2)) => NumV(v1 * v2)
case _ => sys.error("can only multiply numbers")
}
/* A new environment should be pushed onto the stack only when
* binding occurs. Where exactly in BCFAE do bindings happen?
*/
case Ap(f, a)
=> eval(f, stack, store) match {
case ClosureV(f, cEnv)
=> eval(
f.body,
(cEnv += (f.param -> eval(a, stack, store))) :: stack,
store
)
case _ => sys.error("can only apply functions")
}
/* The mutable store allows us to implement Seq-expression
* in terms of sequencing in Scala itself.
*/
case Seq(e1, e2)
=> eval(e1, stack, store); eval(e2, stack, store)
case NewBox(e: Exp)
=> {
val a = store.malloc(stack, eval(e, stack, store))
AddressV(a)
}
case SetBox(b: Exp, e: Exp)
=> eval(b, stack, store) match {
case AddressV(a)
=> {
val ev = eval(e, stack, store)
store.update(a, ev)
ev
}
case _ => sys.error("can only set boxes")
}
case OpenBox(b: Exp)
=> eval(b, stack, store) match {
case AddressV(a) => store(a)
case _ => sys.error("can only open boxes")
}
}
Here is one implementation of the Store interface that does not perform gc. It just runs out of memory once the store is full.
class NoGCStore(size: Int) extends Store {
val memory = new Array[Value](size)
var nextFreeAddr: Int = 0
def malloc(stack: List[Env], v: Value): Int = {
val x = nextFreeAddr
if (x >= size) sys.error("out of memory")
nextFreeAddr += 1
update(x, v)
x
}
def update(index: Int, v: Value): Unit = memory.update(index, v)
def apply(index: Int) = memory(index)
}
Here is a mark-and-sweep garbage collector.
class MarkAndSweepStore(size: Int) extends Store {
val memory = new Array[Value](size)
var free: Int = size
var nextFreeAddr: Int = 0
def malloc(stack: List[Env], v: Value): Int = {
if (free <= 0) gc(stack)
if (free <= 0) sys.error("out of memory")
/* Here we find the next available location in memory via a while-
* loop. In order to avoid maintaining a list of available spaces
* (because we are lazy), let us assume that no box created in
* BCFAE can have an address pointing to a null memory cell (which
* also is the case).
*
* If we ensure the invariant that the variable `free` has always
* the number of free memory space, then the following loop will
* always halt. The nontermination situation will generate an out-
* of-memory error and the program will abort. */
while (memory(nextFreeAddr) != null) {
nextFreeAddr += 1
if (nextFreeAddr == size) nextFreeAddr = 0
}
free -= 1
update(nextFreeAddr, v)
nextFreeAddr
}
def update(index: Int, v: Value): Unit = memory.update(index, v)
def apply(index: Int) = memory(index)
def allAddrInVal(v: Value): Set[Int] = v match {
case AddressV(a) => Set(a)
case NumV(_) => Set.empty
case ClosureV(f, env) => allAddrInEnv(env)
}
def allAddrInEnv(env: Env): Set[Int] =
env.values.map(allAddrInVal _).fold(Set.empty)(_ union _)
def mark(seed: Set[Int]): Unit = {
seed.foreach(memory(_).marked = true)
val newAddresses = seed.flatMap(
ad => allAddrInVal(memory(ad))
).filter(!memory(_).marked)
if(newAddresses != Set.empty) {
mark(newAddresses)
}
}
/* What graph algorithm underlies the mark step as implemented here?
* What potential problem could it cause in a "real" interpreter? */
def sweep(): Unit = {
memory.indices.foreach(
index => if (memory(index) == null) {
/* No work needed on an empty memory cell */
}
else if (memory(index).marked) {
/* Reset `marked` flag for the next gc */
memory(index).marked = false
}
else {
free += 1
memory(index) = null
}
)
}
def gc(stack: List[Env]): Unit = {
println("\nSTARTING GC\nSTACK = " + stack + "\nSTORE = " + memory)
mark(stack.map(allAddrInEnv _).fold(Set.empty)(_ union _))
sweep()
println("GC COMPLETE\nSTORE = " + memory +
"\nNUMBER OF FREE SLOTS = " + free)
}
}
val test4 = wth("makedata", Fun("x", NewBox(NewBox(NewBox("x")))),
Seq(Ap("makedata", 1),
Seq(Ap("makedata", 2),
Seq(wth("s", Ap("makedata", 3),
Ap("makedata", "s")),
Ap("makedata", 4)))))
def runTest4 = eval(
test4,
List(scala.collection.mutable.Map.empty),
new MarkAndSweepStore(5)
)
This model of garbage collection does not illustrate the difficulty of memory management. In most languages, the size of the allocated memory regions on the heap vary, and hence one needs an algorithm to find a free and large-enough spot on the heap. There are various algorithms and heuristics (best-fit, worst-fit, first-fit, ...) for that purpose.
There are also various alternative gc designs. Mark-and-sweep is a non-moving algorithm, where reachable heap objects are never moved. In contrast to that, copying gc algorithms move the reachable objects to a different portion of the heap. One of the oldest algorithms is the semi-space garbage collector, in particular with the implementation purpose.
Topic for class discussion: What are the pros and cons of moving vs. non-moving gc?
It can be shown empirically that most unreachable objects become unreachable while they are still young. Generational gc algorithms take this empirical fact into account and divide the objects into generations, whereby the (small) youngest generation of objects is garbage-collected more frequently.
A typical problem of the simple gc algorithms we discussed is the stop-the-world phenomenon: All execution has to be stopped during a gc cycle. This issue is addressed by incremental or concurrent garbage collectors. Incremental garbage collectors typically reduce the total throughput but increase responsiveness and real-time behavior.
A completely different approach to memory management is reference counting. In reference counting, each object on the heap (in our case, each box) maintains a counter which says how many pointers currently point to that object. The counter is adjusted whenever a pointer variable is assigned to this object (incremented), or moved from this object to another object (decremented). When the counter is 0, the object can be reclaimed.
The obvious disadvantage of reference counting is that it cannot detect cycles on the heap. Hence reference counting algorithm must be augmented with some means to detect cycles. Topic for class discussion: What are the pros and cons of reference counting vs. tracing garbage collectors such as mark-and-sweep or semi-space?
Syntactic and Meta Interpretation
The content of this chapter is available as a Scala file here.
For each desired language semantics, there exist many different ways to implement an interpreter in some meta-language to encode this semantics.
One question that is of particular importance is whether a language feature is implemented by using a corresponding language feature of the meta-language, or whether it is implemented using more primitive language constructs. The first case is called meta-interpretation, the second case syntactic interpretation.
Meta-interpretation can be convenient if we are not interested in having control over the exact meaning of the construct, or if the way the meta-language handles this construct is just what we want for our object-language.
Syntactic interpretation is required if we want to understand what the language feature really means in terms of more primitive constructs, or if we want to implement the language feature differently than the meta-language. Of course, if the meta-language has no corresponding feature, then we have no choice but to make a syntactic interpretation.
Our FAE interpreter is a meta-interpreter with respect to many features. For instance, it does not tell us
- the precision of numbers, or the algorithm for addition
- how the call stack is managed, e.g. the maximum depth of recursion supported by the interpreter
- whether/how memory management for closures works (they are objects on the heap!)
That said, it is possible to make the FAE interpreters still more "meta". Here are two examples.
HOAS
The first one is a version of FAE that uses a different representation of the program syntax, namely one using
meta-language functions to represent object-language functions. This technique is called higher-order abstract syntax, or HOAS.
For instance, the function Fun("x", Add("x", 5)) is now represented as Fun(x => Add(x, 5)).
The interpreter becomes rather short, because substitution and lexical scoping are now being dealt with by the
corresponding meta-level construct.
object HOAS {
enum Exp:
case Num(n: Int)
case Id(name: String)
case Add(lhs: Exp, rhs: Exp)
case Fun(f: Exp => Exp)
case Ap(funExpr: Exp, argExpr: Exp)
import Exp._
def eval(e: Exp): Exp = e match {
case Id(v) => sys.error("unbound identifier: " + v)
case Add(l, r) => (eval(l), eval(r)) match {
case (Num(x), Num(y)) => Num(x + y)
case _ => sys.error("can only add numbers")
}
case Ap(f, a) => eval(f) match {
case Fun(f) => eval(f(eval(a)))
case _ => sys.error("can only apply functions")
}
case _ => e // numbers and functions evaluate to themselves
}
}
Meta-Level Closures
A different way to use meta-level functions in the interpreter is to represent object-level closures by meta-level closures. Notice that this interpreter then has no control anymore about scoping; rather, it is completely inherited from the meta-language.
A particularly pleasing and important property of this interpreter below is that it is compositional, meaning that all recursive calls
of eval are only on subparts of the original expression. This means that it becomes particularly easy to reason about program equivalence
in the object-language in terms of program equivalence in the meta-language: Two object-language expressions are equivalent if their
"denotations" as meta-level expressions are equivalent in the meta-level.
Compositionality is the cornerstone of denotational semantics. A denotational semantics can be thought of as a compositional interpreter in which the meta-language is mathematics. Compositionality also has a rather practical side-effect: It means that we can implement the interpreter in the internal visitor style that we learned about at the beginning of the course (recall that the internal visitor style enforces compositionality). Recommended exercise: Re-implement the interpreter as an internal visitor.
enum Exp:
case Num(n: Int)
case Id(name: String)
case Add(lhs: Exp, rhs: Exp)
case Fun(param: String, body: Exp)
case Ap(funExpr: Exp, argExpr: Exp)
import Exp._
object Compositional {
sealed abstract class Value
type Env = Map[String, Value]
case class NumV(n: Int) extends Value
case class FunV(f: Value => Value) extends Value
def eval(e: Exp): Env => Value = e match {
case Num(n: Int) => (env) => NumV(n)
case Id(x) => env => env(x)
case Add(l, r) => { (env) =>
(eval(l)(env), eval(r)(env)) match {
case (NumV(v1), NumV(v2)) => NumV(v1 + v2)
case _ => sys.error("can only add numbers")
}
}
case Fun(param, body) => (env) => FunV((v) => eval(body)(env + (param -> v)))
case Ap(f, a) => (env) => (eval(f)(env), eval(a)(env)) match {
// Use environment stored in (meta-level) closure to realize proper lexical scoping!
case (FunV(g), arg) => g(arg)
case _ => sys.error("can only apply functions")
}
}
}
For comparison, here is our original FAE interpreter.
object FAE {
sealed abstract class Value
type Env = Map[String, Value]
case class NumV(n: Int) extends Value
case class ClosureV(f: Fun, env: Env) extends Value
def eval(e: Exp, env: Env): Value = e match {
case Num(n: Int) => NumV(n)
case Id(x) => env(x)
case Add(l, r) => {
(eval(l, env), eval(r, env)) match {
case (NumV(v1), NumV(v2)) => NumV(v1 + v2)
case _ => sys.error("can only add numbers")
}
}
case f@Fun(param, body) => ClosureV(f, env)
case Ap(f, a) => eval(f, env) match {
// Use environment stored in closure to realize proper lexical scoping!
case ClosureV(f, closureEnv) => eval(f.body, closureEnv + (f.param -> eval(a, env)))
case _ => sys.error("can only apply functions")
}
}
}
We will soon learn about ways to make FAE more syntactic in various ways. For instance, we will no longer rely on call-stack management of the meta-language, or the existence of higher-order functions.
One dimension in which the interpreter could easily be made more syntactic is the treatment of numbers and arithmetic. For instance, we could represent numbers as sequences of digits instead of Scala numbers. Another aspect in which our FAE interpreter relies on the host language is memory management.
This is particularly relevant for environments stored inside closures. These environments cannot be organized on the call stack and hence need memory management. Since we are using Scala references to refer to environments, environments that are no longer needed are collected by the Scala (or rather, Java) virtual machine.
Church Encodings
The content of this chapter is available as a Scala file here.
Today we shrink our language. It does not seem to be big, but today we want to illustrate how powerful our core language,
the lambda calculus, is. Here is a shrinked version of FAE that does not even have numbers anymore. For testing purposes,
we introduce a new expression PrintDot whose semantics is to print a dot on the screen.
enum Exp:
case Id(name: String)
case Fun(param: String, body: Exp)
case Ap(funExpr: Exp, argExpr: Exp)
case PrintDot()
object Exp:
implicit def id2exp(s: String): Exp = Id(s)
import Exp._
abstract class Value
type Env = Map[String, Value]
// the only values are closures
case class ClosureV(f: Fun, env: Env) extends Value
Notice that the only values in this language are closures. This means that there cannot be the situation anymore that we expect, say, a number but get in fact a closure. Hence, this language has the fascinating property that no dynamic type errors can occur.
def eval(e: Exp, env: Env): Value = e match {
// We give the identity function as dummy value for PrintDot
case PrintDot() => print("."); ClosureV(Fun("x", "x"), Map.empty)
case Id(x) => env(x)
case f@Fun(param, body) => ClosureV(f, env)
case Ap(f, a) => eval(f, env) match {
case ClosureV(f, closureEnv) => eval(f.body, closureEnv + (f.param -> eval(a, env)))
}
}
Now we want to illustrate that we can, in principle, bootstrap a full programming language from this small core. To do so, we use the technique of Church encoding. This means that each datum is represented by its own fold function.
Church Encoding of Booleans
Let's start with booleans and boolean arithmetic.
val f = Fun("t", Fun("f", "f")) // false
val t = Fun("t", Fun("f", "t")) // true
val and = Fun("a", Fun("b", Ap(Ap("a", "b"), "a")))
val or = Fun("a", Fun("b", Ap(Ap("a", "a"), "b")))
val not = Fun("a", Fun("t", Fun("f", Ap(Ap("a", "f"), "t"))))
We can now write our own control structures, such as if/then/else
val ifthenelse = Fun("cond", Fun("t", Fun("f", Ap(Ap("cond", "t"), "f"))))
Church Encoding of Numbers
Let's now consider Numbers. We encode them as Peano numbers. These encodings of numbers are often called Church numbers.
val zero = Fun("s", Fun("z", "z"))
val succ = Fun("n", Fun("s", Fun("z", Ap("s", Ap(Ap("n", "s"), "z")))))
val one = Ap(succ, zero)
val two = Ap(succ, one)
val three = Ap(succ, two)
val add = Fun("a", Fun("b", Fun("s", Fun("z", Ap(Ap("a", "s"), Ap(Ap("b", "s"), "z"))))))
val mult = Fun("a", Fun("b", Fun("s", Fun("z", Ap(Ap("a", Ap("b", "s")), "z")))))
val exp = Fun("a", Fun("b", Ap(Ap("b", Ap(mult, "a")), one)))
val iszero = Fun("a", Ap(Ap("a", Fun("x", f)), t))
The predecessor function is more complicated (why?). We do not show it here. For testing, here is a function that prints a unary representation of a number.
val printnum = Fun("a", Ap(Ap("a", Fun("x", PrintDot())), f))
Church encoding of lists
Again straightforward, except "tail", which we do not show here. It needs the same kind of trick (called "pairing trick") as the predecessor function.
val emptylist = Fun("c", Fun("e", "e"))
val cons = Fun("h", Fun("r", Fun("c", Fun("e", Ap(Ap("c", "h"), Ap(Ap("r", "c"), "e"))))))
val head = Fun("l", Ap(Ap("l", Fun("h", Fun("t", "h"))), f))
For instance, we can multiply all numbers in a list
val multlist = Fun("l", Ap(Ap("l", mult), one))
Here is the list 3, 2, 3:
val list323 = Ap(Ap(cons, three), Ap(Ap(cons, two), Ap(Ap(cons, three), emptylist)))
val test = Ap(printnum, Ap(multlist, list323))
Calling exec should yield 18 dots before the dummy result
val exec = eval(test, Map.empty)
// ..................
// exec: Value = ClosureV(
// f = Fun(param = "x", body = Id(name = "x")),
// env = Map()
// )
Topic for class discussion: Can we do these encodings directly in Scala or Haskell?
Object Algebras
The content of this chapter is available as a Scala file here.
Object algebras: A practical way of using Church Encodings
In previous lectures, we have talked about the "expression problem": The problem of encoding a data structure (like expressions) and functions on that data structure (like evaluators, or pretty-printers) in such a way that both the data structure and the functions thereon can be extended without modifying code, while at the same time maintaining static type safety.
Church encodings look like an obscure theoretical idea at first, but we will see that their incarnation as "object algebras" leads to a quite attractive and practical solution to the expression problem.
Let's look at a Scala version of the Church encodings we saw for the lambda calculus. We use objects instead of functions, but otherwise it is the same. Let's start with booleans.
trait Bool {
def ifthenelse[T](t: T, e: T): T
}
case object T extends Bool {
def ifthenelse[T](t: T, e: T) = t
}
case object F extends Bool {
def ifthenelse[T](t: T, e: T) = e
}
def and(a: Bool, b: Bool): Bool = a.ifthenelse(b, a)
In Smalltalk and related languages, booleans are actually implemented like that (at least conceptually).
In the same way, we can encode Church numerals.
trait NumC {
def fold[T](z: T, s: T => T): T
}
case object Zero extends NumC {
def fold[T](z: T, s: T => T) = z
}
case class Succ(n: NumC) extends NumC {
def fold[T](z: T, s: T => T) = s(n.fold(z, s))
}
def plus(a: NumC, b: NumC) = {
new NumC {
def fold[T](z: T, s: T => T): T = {
a.fold(b.fold(z, s), s)
}
}
}
val oneC = Succ(Zero)
val twoC = Succ(oneC)
val threeC = Succ(twoC)
def testplusC = plus(twoC, threeC).fold[Unit]((), _ => print("."))
Object algebras are a different way to do Church encodings in object-oriented languages. This is what the encoding of Church numbers looks like in object-algebra style.
trait NumSig[T] {
def z: T
def s(p: T): T
}
trait Num {
def apply[T](x: NumSig[T]): T
}
In other words, every constructor of the data type is turned into
a function of the NumSig type, with recursive occurences being replaced
by the type constructor T.
Actual numbers have the type Num, i.e., they are basically functions of type
NumSig[T] => T.
In the terminology of universal algebra, NumSig is an algebraic
signature, and NumSig[T] => T is the type of algebras for that signature.
Compared to the Church encoding above, we bundle the arguments of the
fold-function into a trait NumSig and pass them as a single object.
The advantage of this encoding is that we can extend the set of parameters
of the fold by using inheritance.
In this encoding, the plus-function looks like this:
def plus(a: Num, b: Num) = new Num {
def apply[T](x: NumSig[T]): T = a(new NumSig[T] {
def z = b(x)
def s(p: T) = x.s(p)
})
}
Here is the representation of some numbers.
val zero: Num = new Num { def apply[T](x: NumSig[T]) = x.z }
val one: Num = new Num { def apply[T](x: NumSig[T]) = x.s(x.z) }
val two: Num = new Num { def apply[T](x: NumSig[T]) = x.s(one(x)) }
val three: Num = new Num { def apply[T](x: NumSig[T]) = x.s(two(x)) }
This is an interpretation of the Num-"language" as Scala integers:
object NumAlg extends NumSig[Int] {
def z = 0
def s(x: Int) = x + 1
}
val testplus = plus(two, three)(NumAlg)
// testplus: Int = 5
Let's look at a more useful application of object algebras. We encode expression trees as object algebras.
trait Exp[T] {
implicit def id(name: String): T
def fun(param: String, body: T): T
def ap(funExpr: T, argExpr: T): T
implicit def num(n: Int): T
def add(e1: T, e2: T): T
def wth(x: String, xdef: T, body: T): T = ap(fun(x, body), xdef)
}
The structure of expressions forces compositional interpretations. Hence we use the compositional interpretation using meta-level closures to represent closures.
sealed abstract class Value
type Env = Map[String, Value]
case class ClosureV(f: Value => Value) extends Value
case class NumV(n: Int) extends Value
An interpretation of expressions is now an implementation of the Exp interface
trait eval extends Exp[Env => Value] {
def id(name: String) = env => env(name)
def fun(param: String, body: Env => Value) = env => ClosureV(v => body(env + (param -> v)))
def ap(funExpr: Env => Value, argExpr: Env => Value) = env => funExpr(env) match {
case ClosureV(f) => f(argExpr(env))
case _ => sys.error("can only apply functions")
}
def num(n: Int) = env => NumV(n)
def add(e1: Env => Value, e2: Env => Value) = env => (e1(env), e2(env)) match {
case (NumV(n1), NumV(n2)) => NumV(n1 + n2)
case _ => sys.error("can only add numbers")
}
}
object eval extends eval
An example program becomes a function that is parametric in the chosen interpretation:
def test[T](semantics: Exp[T]) = {
import semantics._
ap(ap(fun("x", fun("y", add("x", "y"))), 5), 3)
}
We evaluate the program by folding the eval-visitor over it.
val testres = test(eval)(Map.empty)
// testres: Value = NumV(n = 8)
The object algebra encoding of expressions is quite extensible. For instance, we can add another case to the expression data type by extending the interface.
trait ExpWithMult[T] extends Exp[T] {
def mult(e1: T, e2: T): T
}
trait evalWithMult extends eval with ExpWithMult[Env => Value] {
def mult(e1: Env => Value, e2: Env => Value) = env => (e1(env), e2(env)) match {
case (NumV(n1), NumV(n2)) => NumV(n1 * n2)
case _ => sys.error("can only multiply numbers")
}
}
object evalWithMult extends evalWithMult
def testMult[T](semantics: ExpWithMult[T]) = {
import semantics._
ap(ap(fun("x", fun("y", mult("x", "y"))), 5), 3)
}
val testresMult = testMult(evalWithMult)(Map.empty)
// testresMult: Value = NumV(n = 15)
Note that there is no danger of confusing the language variants. For instance,
an attempt to pass testMult to eval will be a static type error.
At the same time, we can add another function on expressions (such as a pretty-printer)
without changing existing code, too: Just add a
trait prettyPrint extends Exp[String] and, if pretty-printing of ExpWithMult
is required, extend with trait prettyPrintMult extends prettyPrint with ExpWithMult[String].
This is the object algebra way of solving the expression problem.
We can also go one step further and combine object algebras with typed higher-order abstract syntax, using higher-kinded type members. Don't panic if you don't understand what is going on here.
trait ExpT {
type Rep[_]
def fun[S, T](f: Rep[S] => Rep[T]): Rep[S => T]
def ap[S, T](funExpr: Rep[S => T], argExpr: Rep[S]): Rep[T]
implicit def num(n: Int): Rep[Int]
def add(e1: Rep[Int], e2: Rep[Int]): Rep[Int]
}
Instead of having the semantic domain as a type parameter T as above,
we encode it as a higher-kinded abstract type member Rep[_]. This leads
to significantly shorter type signatures and more fine-grained typing
via Scala's support for "path-dependent types".
Note that, in contrast to eval, no dynamic checks (match ...) are needed
in the interpreter. Also, the result type of the evaluator is just X. In
contrast to Value, this is a "tagless" type, that is, it does not maintain
information at runtime about which variant it is. This is because the ExpT
datatype guarantees well-typedness of expressions. This interpreter will, in
general, run much faster and can in fact be formulated in such a way that
interpreting a program is just as fast as writing the program directly in
the meta language.
object evalT extends ExpT {
type Rep[X] = X
def fun[S, T](f: S => T) = f
def ap[S, T](f: S => T, a: S) = f(a)
def num(n: Int) = n
def add(e1: Int, e2: Int) = e1 + e2
}
object prettyprintT extends ExpT {
var counter = 0
type Rep[X] = String
def fun[S, T](f: String => String) = {
val varname = "x" + counter.toString
counter += 1
"(" + varname + " => " + f(varname) + ")"
}
def ap[S, T](f: String, a: String) = f + "(" + a + ")"
def num(n: Int) = n.toString
def add(e1: String, e2: String) = "(" + e1 + "+" + e2 + ")"
}
def test2(semantics: ExpT) = {
import semantics._
ap(ap(fun((x: Rep[Int]) => fun((y: Rep[Int]) => add(x, y))), 5), 3)
}
val testres2 = test2(evalT)
// testres2: Int = 8
val testres3 = test2(prettyprintT)
// testres3: String = "(x0 => (x1 => (x0+x1)))(5)(3)"
An attempt to construct an ill-formed object program will be detected by the Scala type checker. For instance, the following program which adds a number and a function is rejected by the Scala type checker:
def testilltyped(semantics: ExpT) = {
import semantics._
add(5, fun((x: Rep[Int]) => x))
}
// error:
// Found: semantics.Rep[Int => Int]
// Required: semantics.Rep[Int]
// add(5, fun((x: Rep[Int]) => x))
// ^^^^^^^^^^^^^^^^^^^^^^^
The type system encoded in the ExpT type is the so-called "simply-typed lambda calculus".
Encoding more expressive type system in a similar style (including, e.g., type parameters)
is an active area of research.
References: B. Olivira, W.Cook. Extensibility for the Masses: Practical Extensibility with Object Algebras. Proc. ECOOP 2012.
Continuations: Motivation
The content of this chapter is available as a Scala file here.
Consider the following very simple program:
def inputNumber(prompt: String): Int = {
println(prompt)
Integer.parseInt(readLine())
}
def progSimple = {
println(inputNumber("First number:") + inputNumber("Second number"))
}
Now consider a web version of the program:
- the first number is entered on the first page
- then the first number is submitted, a form to enter the second number is shown
- when the second number is submitted, a form with the result is generated and shown.
Even this "addition server" is difficult to implement. Because http is a stateless protocol (for good reasons), every web program is basically forced to terminate after every request. This means that the Web developer must turn this application into three programs:
- The first program displays the first form.
- The second program consumes the form values from the first form, and generates the second form.
- The third program consumes the form values from the second form, computes the output, and generates the result.
Because the value entered in the first form is needed by the third program to compute its output, this value must somehow be transmitted from the first program to the third. This is typically done by using the hidden field mechanism of HTML.
Suppose, instead of using a hidden field, the application developer used a Java Servlet session object, or a database field, to store the first number. (Application developers are often pushed to do this because that is the feature most conveniently supported by the language and API they are employing.) Then, if the developer were to exploratorily open multiple windows the application can compute the wrong answer. Hence, the actual program in a web developer's mind has the structure of the following program. An actual web program is of course more complicated, but this primitive model of web programming is sufficient to explain the problem.
// we use the return type "Nothing" for functions that will never return (normally)
def webdisplay(s: String): Nothing = {
println(s)
sys.error("program terminated")
}
def webread(prompt: String, continue: String): Nothing = {
println(prompt)
println("send input to: " + continue)
sys.error("program terminated")
}
def program1 = webread("enter first number", "s2")
def program2(n1: Int) = webread("enter second number and remind me of previoulsy entered number " + n1, "s3")
def program3(n1: Int, n2: Int) = webdisplay("The sum of " + n1 + " and " + n2 + " is " + (n1 + n2))
We could write a better webread and webdisplay procedure if we could somehow get hold of the
pending computation at the time when the procedure was invoked. Such a pending computation is
called continuation.
Let's consider the continuation at the point of the first interaction in the original program,
def prog = {
println(inputNumber() + inputNumber())
}
The pending computation (or, continuation in the following) is to take the result of the first
inputNumber invocation, add to it the result of the second invocation, and display it.
We can express the continuation as a function:
val cont1 = (n: Int) => println(n + inputNumber("Second number"))
Similarly, the continuation at the second point of interaction is:
val cont2 = (m: Int) => println(n + m)
where n is the result of the first input, which is stored in the closure of cont2.
Assuming an explicit representation of the continuation, it is obvious that we can now
write a version of webread, called webread_k, which takes the continuation as second parameter and invokes
the continuation once the answer to the result is received by the server.
This can be implemented, say, by associating to a continuation a unique ID, store the continuation
in a hashmap on the server using this ID, and storing the ID in the form such that it gets
submitted back to the server once the client presses the submit button.
Here is code illustrating the idea. For simplicity we assume that all web forms return a single integer value.
val continuations = new scala.collection.mutable.HashMap[String, Int => Nothing]()
var nextIndex: Int = 0
def getNextID = {
nextIndex += 1
"c" + nextIndex
}
def webread_k(prompt: String, k: Int => Nothing): Nothing = {
val id = getNextID
continuations += (id -> k)
println(prompt)
println("to continue, invoke continuation: " + id)
sys.error("program terminated")
}
def continue(kid: String, result: Int) = continuations(kid)(result)
Using webread_k, we can now define our addition server as follows.
If you try webprog, ignore the stack traces.
def webprog = webread_k("enter first number", (n) =>
webread_k("enter second number", (m) =>
webdisplay("The sum of " + n + " and " + m + " is " + (n + m))))
For instance, try:
scala> webprog -- yields some continuation id "c1"
scala> continue("c1", 5) -- yields some continuation id "c2"
scala> continue("c2", 7)
This should yield the result 12 as expected. But also try:
scala> webprog -- yields some continuation id "c1"
scala> continue("c1", 5) -- yields some continuation id "c2"
scala> continue("c1", 6) -- yields some continuation id "c3"
scala> continue("c2", 3) -- should yield 8
scala> continue("c3", 3) -- should yield 9
The style of programming in webprog, which is obviously more complicated than the logical
structure of progSimple, shows up in many practical programming scenarios - server-side web programming
is just one of them. For instance, in JavaScript many API functions for asynchronous communication
such as httprequest in AJAX require to pass a callback function, which leads to similar code
as the one in webprog above.
Let's consider this "web transformation" - the transformation from progSimple to webprog - in more detail.
To this end, let's make our application a bit more sophisticated. Instead of entering only two
numbers, the user enters n numbers, e.g., the prices of a list of n items.
Here is the "non-web" version of the application:
def allCosts(itemList: List[String]): Int = itemList match {
case Nil => 0
case x :: rest => inputNumber("Cost of item " + x + ":") + allCosts(rest)
}
val testData: List[String] = List("banana", "apple", "orange")
def test = println("Total sum: " + allCosts(testData))
This version of allCosts is clearly not web-friendly, because it uses inputNumber,
which we do not know how to implement for the web.
The first thing to observe is that on its own, allCosts is not a complete program: it doesn't do anything unless
it is called with actual arguments!
Instead, it is a library procedure that may be used in many different contexts. Because it has a web interaction,
however, there is the danger that at the point of interaction, the rest of the computation -- that is, the
computation that invoked allCosts -- will be lost. To prevent this, allCosts must consume an extra argument,
a continuation, that represents the rest of the pending computation. To signify this change in contract, we will use
the convention of appending _k to the name of the procedure and k to name the continuation parameter.
Here is a first attempt to define allCosts_k.
def allCosts_k(itemList: List[String], k: Int => Nothing): Nothing = itemList match {
case Nil => 0
case x :: rest => webread_k("Cost of item " + x + ":", n => n + allCosts_k(rest, k))
}
This may look reasonable, but it suffers from an immediate problem. When the recursive call occurs, if
the list had two or more elements, then there will immediately be another web interaction. Because this will
terminate the program, the pending addition will be lost! Therefore, the addition of n has to move into the
continuation fed to allCosts_k. In code:
def allCosts_k(itemList: List[String], k: Int => Nothing): Nothing = itemList match {
case Nil => 0
case x :: rest => webread_k("Cost of item " + x + ":", n => allCosts_k(rest, m => k(m + n)))
}
That is, the receiver of the web interaction is invoked with the cost of the first item. When allCosts_k is invoked
recursively, it is applied to the rest of the list. Its receiver must therefore receive the tally of costs of the
remaining items. That explains the pattern in the receiver.
The only problem is, where does a continuation ever get a value? We create larger-and-larger continuations on each recursive invocation, but what ever invokes them?
Here is the same problem from a different angle (that also answers the question above). Notice that each
recursive invocation of allCosts_k takes place in the aftermath of a web interaction. We have already seen how
the act of web interaction terminates the pending computation. Therefore, when the list empties, where
is the value 0 going? Presumably to the pending computation, but there is none. Any computation that
would have been pending has now been recorded in k, which is expecting a value. Therefore, the correct
transformation of this procedure is:
def allCosts_k(itemList: List[String], k: Int => Nothing): Nothing = itemList match {
case Nil => k(0)
case x :: rest => webread_k("Cost of item " + x + ":", n => allCosts_k(rest, m => k(m + n)))
}
def testweb = allCosts_k(testData, m => webdisplay("Total sum: " + m))
Let's now consider the case that we have used a library function for the iteration in allCosts, namely
the map function, which we replicate here.
def map[S, T](c: List[S], f: S => T): List[T] = c match {
case Nil => Nil
case x :: rest => f(x) :: map(rest, f)
}
Using map, we can rephrase allCosts as follows.
def allCosts2(itemList: List[String]): Int =
map(itemList, (x: String) => inputNumber("Cost of item " + x + ":")).sum
What if we we want to use map in allCosts_k?
Just using webread_k in place of inputNumber will not work, since webread_k expects an additional parameter.
Obviously we must somehow modify the definition of map. But what can we pass as second parameter in the call
to f?
Insight: We must perform the "web transformation" to map as well. We call the result map_k. Here is the code:
def map_k[S, T](c: List[S], f: (S, T => Nothing) => Nothing, k: List[T] => Nothing): Nothing = c match {
case Nil => k(Nil)
case x :: rest => f(x, t => map_k(rest, f, (tr: List[T]) => k(t :: tr)))
}
def allCosts2_k(itemList: List[String], k: Int => Nothing): Nothing =
map_k(itemList,
(x: String, k2: Int => Nothing) =>
webread_k("Cost of item " + x + ":", k2),
(l: List[Int]) => k(l.sum))
Implications of the "web transformation":
-
We had to make decisions about the order of evaluation. That is, we had to choose whether to evaluate the left or the right argument of addition first. This was an issue we had specified only implicitly earlier; if our evaluator had chosen to evaluate arguments right-to-left, the web program at the beginning of this document would have asked for the second argument before the first! We have made this left-to-right order of evaluation explicit in our transformation.
-
The transformation we use is global, namely it (potentially) affects all the procedures in the program by forcing them all to consume an extra continuation as an argument. We usually don't have a choice as to whether or not to transform a procedure. Suppose
finvokesgandginvokesh, and we transformftof_kbut don't transformgorh. Now whenf_kinvokesgandginvokesh, supposehconsumes input from the web. At this point the program terminates, but the last continuation procedure (necessary to resume the computation when the user supplies an input) is the one given tof_k, with all record ofgandhlost. -
This transformation sequentializes the program. Given a nested expression, it forces the programmer to choose which sub-expression to evaluate first (a consequence of the first point above); further, every subsequent operation lies in the continuation, which in turn picks the first expression to evaluate, pushing all other operations into its continuation; and so forth. The net result is a program that looks an awful lot like a traditional procedural program. This suggests that this series of transformations can be used to compile a program in a language like Scheme into one in a language like C!
Continuations: Definition
The content of this chapter is available as a Scala file here.
Today's goal is to make the "web" (or rather, CPS) transformation which we applied informally in the previous lecture formal.
In the previous lecture we have seen that we had to translate the following program:
println("The sum is: " + (inputNumber("First number:") + inputNumber("Second number")))
into this program:
webread_k("First number", (n) =>
webread_k("Second number:", (m) =>
webdisplay("The sum is: " + (n + m))))
This hand-translation is sufficient if this expression is the entire program. If we wish to use it as a sub-expression in a larger program, this does not suffice, because there may be a pending computation outside its own evaluation. For that reason, the program has to send its result to a continuation instead of returning it:
k => webread_k("First number", (n) =>
webread_k("Second number:", (m) =>
webdisplay("The sum is: " + k(n + m))))
This version can be employed in the transformation of a larger program. In the special case where this is the entire program we can apply the transformed term to the identity function to get the same result as the previous manual transformation.
In general, every term, when converted to CPS, will be have the following properties (see O. Danvy, Three Steps for the CPS Transformation, 1991):
-
The values of all intermediate applications are given a name.
-
The evaluation of these applications is sequentialized based on a traversal of their abstract syntax tree.
-
The results of the transformation are procedures that expect a continuation parameter - a lambda abstraction whose application to intermediate values yields the final result of the whole evaluation.
Function application
Let us now look at the transformation of a function application. For instance, let us consider the term
f(a)(g(b))
The transformation of the function argument, f(a), should be
f_k(a, fval => ...)
Similarly, the transformation of the argument position would be:
g_k(b, arg => ...)
Given these two values, fval and arg, we can now perform the application, like so:
k(fval(arg))
However, this will not work, because if fval is in CPS itself, it will not return.
Instead, k must be given as an argument to the function, like so:
k => f_k(a, fval => g_k(b, arg => fval(arg, k)))
Reading this sequentially, it says to evaluate the function expression, store its value in fval,
then evaluate the argument, store its value in arg, and finally invoke the function value on the argument.
This function's continuation is the outer continuation of the function application itself.
Variables and constants
What about variables and constants? Since every term in CPS must be a function that consumes a continuation,
the constant is simply sent to the continuation.
For instance, the CPS transformation of the number 3 is k => k(3).
Function definitions
What about function definitions, such as x => x? Since every lambda expression is also a constant,
we might be tempted to use the same rule as above, i.e.,
k => k(x => x)
However, the transformation is more subtle. A function application invokes the function on two arguments, whereas
the original function x => x consumes only one. What is the second argument?
Answer: It is the dynamic continuation, i.e., the continuation at the time of the function application (as opposed to its definition). We cannot ignore this continuation: It is the stack active at the point of function invocation, so we want to preserve it. This is in contrast to what we did with environments, and more in line with our treatment of the store.
The transformed version hence reads:
k => k((x, dynk) => (k => k(x))(dynk))
which is equivalent (when the inner application finally happens) to:
k => k((x, dynk) => dynk(x))
This is a function that accepts a value and a dynamic continuation and sends the value to that continuation.
Formal Definition of the CPS Transformation
We are now ready to write this transformation formally, as a source-to-source transformation. This transformation
could have the type cps(e: Exp): Exp, but we choose a different type for two reasons:
-
In CPS we need function definitions and applications with two arguments instead of one. This could be addressed by adding new syntax.
-
More importantly, we want the invariants of the CPS format to be clearly visible in the syntax definition of the result, most importantly the fact that all function applications are tail calls.
enum Exp:
case Num(n: Int)
case Id(name: String)
case Add(lhs: Exp, rhs: Exp)
case Fun(param: String, body: Exp)
case Ap(funExpr: Exp, argExpr: Exp)
object Exp:
implicit def num2exp(n: Int): Exp = Num(n)
implicit def id2exp(s: String): Exp = Id(s)
For CPS transformed terms, we define two different syntactic categories: Values (CPSVal) and Expressions (CPSExp).
By "values", we mean terms that "return", that is, terms that are different from applications of functions
or continuations (neither of which returns). Additions (CPSAdd) are also values in this regard: We assume addition
to be built-in and not requiring CPS-transformations.
The syntax makes clear that all arguments of a function application are values - hence no nesting of applications
can occur. Furthermore, the syntax differentiates between defining an ordinary function (CPSFun) which, when translated,
gets an additional continuation parameter, and Continuation Functions (CPSCont), which are the result of the CPS
transformation. Correspondingly, we have two different forms of applications, CPSContAp and CPSFunAp.
Here is the formal definition:
sealed abstract class CPSExp
abstract class CPSVal extends CPSExp
case class CPSNum(n: Int) extends CPSVal
case class CPSAdd(l: CPSVar, r: CPSVar) extends CPSVal
case class CPSCont(v: String, body: CPSExp) extends CPSVal
case class CPSFun(x: String, k: String, body: CPSExp) extends CPSVal
case class CPSVar(x: String) extends CPSVal { override def toString = x.toString }
implicit def id2cpsexp(x: String): CPSVar = CPSVar(x)
case class CPSContAp(k: CPSVal, a: CPSVal) extends CPSExp
// the arguments are even CPSVar and not only CPSVal!
case class CPSFunAp(f: CPSVar, a: CPSVar, k: CPSVar) extends CPSExp
With these definitions, we are now ready to formalize the transformation described above.
There is one technical issue: We need to introduce new names for binders into our program, such as "k".
We need to make sure that we do not accidentially capture existing names in the program.
For this reason we need our freshName machinery we introduced for
FAE.
def freeVars(e: Exp): Set[String] = e match {
case Id(x) => Set(x)
case Add(l, r) => freeVars(l) ++ freeVars(r)
case Fun(x, body) => freeVars(body) - x
case Ap(f, a) => freeVars(f) ++ freeVars(a)
case Num(n) => Set.empty
}
def freshName(names: Set[String], default: String): String = {
var last: Int = 0
var freshName = default
while (names contains freshName) { freshName = default + last; last += 1; }
freshName
}
def cps(e: Exp): CPSCont = e match {
case Add(e1, e2) => {
val k = freshName(freeVars(e), "k")
val lv = freshName(freeVars(e2), "lv")
CPSCont(k, CPSContAp(cps(e1), CPSCont(lv,
CPSContAp(cps(e2), CPSCont("rv",
CPSContAp(k, CPSAdd("rv", lv)))))))
}
case Fun(a, body) => {
val k = freshName(freeVars(e), "k")
val dynk = freshName(freeVars(e), "dynk")
CPSCont(k, CPSContAp(k, CPSFun(a, dynk, CPSContAp(cps(body), dynk))))
}
case Ap(f, a) => {
val k = freshName(freeVars(e), "k")
val fval = freshName(freeVars(a), "fval")
CPSCont(k, CPSContAp(cps(f), CPSCont(fval,
CPSContAp(cps(a), CPSCont("aval",
CPSFunAp(fval, "aval", k))))))
}
case Id(x) => {
val k = freshName(freeVars(e), "k")
CPSCont(k, CPSContAp(k, CPSVar(x)))
}
case Num(n) => {
val k = freshName(freeVars(e), "k")
CPSCont(k, CPSContAp("k", CPSNum(n)))
}
}
This transformation is the so-called Fischer CPS transformation. There are many other CPS transformation algorithms. The Fischer CPS transformation is nice because it is so simple and because it is defined as one simple structural recursion over the AST. Its main disadvantage is the existence of so-called "administrative redexes".
An administrative redex is a function application whose operator is a "continuation lambda" - a lambda produced during CPS transformation that was not in the original program. Such function applications can be computed immediately because the function which is called is known.
For instance, cps(Add(2, 3)) yields
CPSCont("k",
CPSContAp(
CPSCont("k",
CPSContAp("k", 2)),
CPSCont("lv",
CPSContAp(
CPSCont("k",
CPSContAp("k", 3)),
CPSCont("rv",
CPSContAp("k", CPSAdd("rv", "lv")))))))
instead of
CPSCont("k", CPSContAp("k", CPSAdd(2, 3)))
Many more advanced CPS transformation algorithms try to avoid as many administrative redexes as possible.
First-Class Continuations
The content of this chapter is available as a Scala file here.
Today's goal is to formalize first-class continuations as illustrated by Scheme's let/cc construct. In the previous lecture we have
learned why first class continuations are a powerful language construct. Today we learn the semantics of first-class continuations by
extending our interpreter to support let/cc. Here is the abstract syntax of the language extended with Letcc:
enum Exp:
case Num(n: Int)
case Id(name: String)
case Add(lhs: Exp, rhs: Exp)
case Fun(param: String, body: Exp)
case Ap(funExpr: Exp, argExpr: Exp)
/** The abstract syntax of Letcc is as follows */
case Letcc(param: String, body: Exp)
object Exp:
implicit def num2exp(n: Int): Exp = Num(n)
implicit def id2exp(s: String): Exp = Id(s)
But how do we implement Letcc? How do we get hold of the rest of the computation of the object (=interpreted) program?
One idea would be to CPS-transform the object program. Then we would have the current continuation available and could
store it in environments etc.
However, we want to give a direct semantics to first-class continuations, without first transforming the object program.
Insight: If we CPS-transform the interpreter, the continuation of the interpreter also represents, in some way, the continuation of the object program. The difference is that it represents what's left to do in the interpreter and not in the object program. However, what is left in the interpreter is what is left in the object program.
Hence, we are faced with two tasks:
- CPS-transform the interpreter
- add a branch for
Letccto the interpreter.
Let's start with the standard infrastructure of values and environments.
sealed abstract class Value
type Env = Map[String, Value]
case class NumV(n: Int) extends Value
case class ClosureV(f: Fun, env: Env) extends Value
How do we represent values that represent continuations? Since we want to represent an object-language continuation by a meta-language continuation, we need to be able to wrap a meta-language continuation as an object-language value. This continuation will always accept some other object-language value:
case class ContV(f: Value => Nothing) extends Value
We also need a syntactic construct to apply continuations. One way to provide such a construct would be to add a new syntactic category of continuation application. We will instead do what Scheme and other languages also do: We overload the normal function-applicaton construct and also use it for application of continuations.
This means that we will need a case distinction in our interpreter whether the function argument is a closure or a continuation.
Let's now study the interpreter for our new language. The branches for Num, Id, Add, and Fun are straightforward applications of the
CPS transformation technique we already know.
def eval(e: Exp, env: Env, k: Value => Nothing): Nothing = e match {
case Num(n: Int) => k(NumV(n))
case Id(x) => k(env(x))
case Add(l, r) => {
eval(l, env, lv =>
eval(r, env, rv =>
(lv, rv) match {
case (NumV(v1), NumV(v2)) => k(NumV(v1 + v2))
case _ => sys.error("can only add numbers")
}))
}
case f@Fun(param, body) => k(ClosureV(f, env))
/* In the application case we now need to distinguish whether the first argument
* is a closure or a continuation. If it is a continuation, we ignore the
* current continuation k and "jump" to the stored continuation by applying the
* evaluated continuation argument to it. */
case Ap(f, a) => eval(f, env, cl => cl match {
case ClosureV(f, closureEnv) => eval(a, env, av => eval(f.body, closureEnv + (f.param -> av), k))
case ContV(f) => eval(a, env, av => f(av))
case _ => sys.error("can only apply functions")
})
/* Letcc is now surprisingly simple: We continue the evaluation in the body in an
* extended environment in which param is bound to the current continuation k,
* wrapped as a value using ContV. */
case Letcc(param, body) => eval(body, env + (param -> ContV(k)), k)
}
To make it easier to experiment with the interpreter this code provides the right initialization to eval. We have to give eval a
continuation which represents the rest of the computation after eval is done. A small technical problem arises due to our usage of
the return type Nothing for continuations, to emphasize that they do not return: The only way to implement a value that has this
type is a function that does indeed not return. We do so by letting this function throw an exception. To keep track of the returned
value we store it temporarily in a variable, catch the exception, and return the stored value.
def starteval(e: Exp): Value = {
var res: Value = null
val s: Value => Nothing = (v) => { res = v; sys.error("program terminated") }
try { eval(e, Map.empty, s) } catch { case e: Throwable => () }
res
}
Finally a small test of Letcc.
val testprog = Add(1, Letcc("k", Add(2, Ap("k", 3))))
assert(starteval(testprog) == NumV(4))
Here's a little quiz about Letcc:
Add(Letcc("k", Add(3, Ap("k", 1))), 4)
NumV(8)
NumV(5)
NumV(1)
NumV(4)
LetCC
The content of this chapter is available as a Racket file here.
#lang racket
Racket is a language with so-called first-class continuations. It can reify the current continuation automatically and on the fly. As you may imagine, creating a continuation involves copying the stack, but there are less and more efficient ways of obtaining the same effect.
Adding continuations to a language makes it easy to create a better web programming protocol, as we have seen. But first-class continuations are much more general and give programmers immense power in numerous contexts.
In Racket (and the related programming language Scheme), a continuation is created with
let/cc. It can be used to give the current continuation a name: (let/cc k ... k ...)
Let's write some programs using continuations (try this in the Racket read-eval-print loop).
(let/cc k (k 3)) What is the continuation k here?
(+ 1 (let/cc k (k 3))) What is the continuation k here?
Using let/cc for exception handling: let/cc acts as the "try", invoking k as the "throw".
(define (f n) (+ 10 (* 5 (let/cc k (/ 1 (if (zero? n) (k 1) n))))))
Next we simulate a very simple kind of exception handling mechanism with first-class continuations.
(define exceptionhandler (lambda (msg) (display "unhandled exception")))
(define (f n)
(+ 5
(if (zero? n) (exceptionhandler "division by zero")
(/ 8 n))))
(define (g n)
(+ (f n) (f n)))
(define (h)
(let/cc k
(begin
(set! exceptionhandler (lambda (msg) (begin
(displayln msg)
(k))))
(displayln (g 1))
(displayln (g 0))
(displayln (g 2)))))
Try evaluating (h) in the read-eval-print-loop.
Now we encode a simple debugger with support for breakpoints.
The breakpoint variable stores the continuation at the current breakpoint
(define breakpoint false) ; initalized with a dummy value
The repl variable stores the continuation that jumps to the read-eval-print loop
(define repl false) ; initialized with a dummy value
The break function captures the current continuation, stores it, and jumps to the REPL:
(define (break) (let/cc k
(begin
(set! breakpoint k)
(repl))))
To continue, we jump to the previously stored continuation:
(define (continue)
(breakpoint))
Here is a simple test program of our "debugger":
(define (main)
(display "1")
(break)
(display "2")
(break)
(display "3"))
; nothing to do after this, hence k is the REPL continuation
(let/cc k
(set! repl k))
Let's now consider a more sophisticated usage of let/cc, namely to program a simple form
of cooperative multi-threading, often called co-routines. A co-routine designates points
in the routine where a switch to another routine should occur - a so-called yield point.
With let/cc we can program co-routines within the language, without having any dedicated
built-in support for it:
(define queue empty)
(define (empty-queue?)
(empty? queue))
(define (enqueue x)
(set! queue (append queue (list x))))
(define (dequeue)
(let ((x (first queue)))
(set! queue (rest queue))
x))
(define (fork)
(let/cc k
(begin
(enqueue (lambda () (k 1))) ; enqueue thunk
0)))
(define (join)
(if (not (empty-queue?))
((dequeue))
'alljoined))
(define (yield)
(let/cc k
(enqueue k)
((dequeue)))) ; invoke thunk
(define (fact n) (if (zero? n) 1 (* n (fact (- n 1)))))
(define (fib n) (if (< n 2) 1 (+ (fib (- n 1)) (fib (- n 2)))))
(define (printfibs n)
(if (zero? n)
(begin (print "Fertig mit fibs") (newline))
(begin
(print (format "Fib(~A)=~A" n (fib n)))
(newline)
(yield)
(printfibs (- n 1)))))
(define (printfacts n)
(if (zero? n)
(begin (print "Fertig mit facts") (newline))
(begin
(print (format "Fact(~A)=~A" n (fact n)))
(newline)
(yield)
(printfacts (- n 1)))))
(define (test-forkjoin)
(if (= (fork) 0)
(printfibs 8)
(printfacts 12))
(join)
(if (= (fork) 0)
(printfibs 10)
(printfacts 8))
(join))
Delimited Continuations
The content of this chapter is available as a Scala file here.
The continuations we have seen so far represent the whole call-stack. Invoking a continuation was not like a function call because continuations never return a result. Invoking a continuation is more similar to a disciplined version of GOTO.
However, the fact that continuations never return and represent the full call-stack often makes their use cumbersome. In particular, such continuations cannot be composed. The non-composability of continuations is visible in the fact that applications using first-class continuations often need to make use of mutable state.
This is different with delimited continuations. Delimited continuations only represent a segement of the call-stack. Delimited continuations behave like functions, that is, they return a value and are hence composable.
Delimited continuations have many quite powerful applications, ranging from advanced exception handling to backtracking algorithms and probabilistic programming as well as so-called algebraic effects. Delimited continuations are available in Racket and many variants of Scheme, OCaML, Haskell and, thanks to work in our research group, in Java.
There are many different variants of delimited continuations, many of them dating back to the late 1980s and
early 1990s. One of the most common forms of delimited continuations is in the form of reset and shift,
proposed by Olivier Danvy and Andrzej Filinski in 1990. The first of these primitives, reset e, marks the
current stack frame and continues with e. An invocation of the second primitive, shift k e, reifies the
stack segment between the current stack frame and the closest stack frame marked by a reset as a function,
binds this function to k, and evaluates e (which can then call k zero or more times).
Their meaning can be understood via a code transformation.
reset (...A... shift k e ...B...)
; -->
with k = lambda x. reset (...A... x ...B...) :
reset e
reset e ; no invocation of shift inside e
; -->
e
In class, we will look at a couple of examples of using shift and reset. shift and reset are available
in some variants of Scheme, including Racket, as an extension of Scala, as a library in OcaML, as well
as various usually partial, incomplete or buggy simulations in other languages.
A definitional interpreter for delimited continuations is pretty simple.
enum Exp:
case Num(n: Int)
case Id(name: String)
case Add(lhs: Exp, rhs: Exp)
case Fun(param: String, body: Exp)
case Ap(funExpr: Exp, argExpr: Exp)
case Shift(param: String, body: Exp)
case Reset(body: Exp)
object Exp:
implicit def num2exp(n: Int): Exp = Num(n)
implicit def id2exp(s: String): Exp = Id(s)
sealed abstract class Value
type Env = Map[String, Value]
case class NumV(n: Int) extends Value
case class ClosureV(f: Fun, env: Env) extends Value
case class ContV(f: Value => Value) extends Value
def eval(e: Exp, env: Env, k: Value => Value): Value = e match {
case Num(n: Int) => k(NumV(n))
case Id(x) => k(env(x))
case Add(l, r) => {
eval(l, env, lv =>
eval(r, env, rv =>
(lv, rv) match {
case (NumV(v1), NumV(v2)) => k(NumV(v1 + v2))
case _ => sys.error("can only add numbers")
}))
}
case f@Fun(param, body) => k(ClosureV(f, env))
case Ap(f, a) => eval(f, env, cl => cl match {
case ClosureV(f, closureEnv) => eval(a, env, av => eval(f.body, closureEnv + (f.param -> av), k))
// compose continuations k2 and k
case ContV(k2) => eval(a, env, av => k(k2(av)))
case _ => sys.error("can only apply functions")
})
// reset the continuation to the identity function
case Reset(e) => k(eval(e, env, x => x))
// wrap current continuation and reset continuation
case Shift(param, body) => eval(body, env + (param -> ContV(k)), x => x)
}
Shift
in the following expression?
Add(3,
Reset(Add(1,
Shift("k", Add(4, Ap("k", 2))))))
Add(1, -)
Add(3, -)
Reset is captured.
Add(3, Add(1, -)
Reset is captured.
Add(4, -)
Shift is captured.
Add(
Reset(Add(2,
Shift("k", Add(Ap("k", 1), Ap("k", 3))))),
5)
Num(8)
Reset is not discarded.
Num(13)
Num(18)
Reset is not captured.
sys.error("can only add numbers")
References:
- Olivier Danvy and Andre Filinski, “Abstracting control”, LISP and Functional Programming, 1990.
- O. Kiselyov, An argument against call/cc.
- O. Kiselyov, Introduction to programming with shift and reset.
Introduction to Monads
The content of this chapter is available as a Scala file here.
We have seen various patterns of function composition:
- The environment-passing style, in which an environment is passed down in recursive calls.
- The store-passing style, in which a store is threaded in and out of every computation.
- The continuation-passing style, in which every function call is a tail call.
Monads are way to abstract over such patterns of function composition.
Motivation
Using monads, we can write code which can be parameterized to be in one of the styles above (or many others). Here is another common pattern of function composition. Suppose we have the following API of (nonsensical) functions:
def f(n: Int): String = "x"
def g(x: String): Boolean = x == "x"
def h(b: Boolean): Int = if (b) 27 else sys.error("error")
def clientCode = h(!g(f(27) + "z"))
Now suppose that these functions can possibly fail (say, because they involve remote communication). A common way to deal with such
failures is to use the Option datatype:
def fOp(n: Int): Option[String] = if (n < 100) Some("x") else None
def gOp(x: String): Option[Boolean] = Some(x == "x")
def hOp(b: Boolean): Option[Int] = if (b) Some(27) else None
However, now the clientCode must be changed rather dramatically:
def clientCodeOp =
fOp(27) match {
case Some(x) => gOp(x + "z") match {
case Some(y) => hOp(!y)
case None => None
}
case None => None
}
We see a kind of pattern in this code. We have a value of type Option[A], but the next function we need to call requires an A and
produces an Option[B]. If the Option[A] value is None, then the whole computation produces None. If it is Some(x)
instead, we pass x to the function.
We can capture this pattern in the form of a function:
def bindOption[A, B](a: Option[A], f: A => Option[B]): Option[B] = a match {
case Some(x) => f(x)
case None => None
}
Using bindOption, we can rewrite the code above as follows:
def clientCodeOpBind =
bindOption(fOp(27), (x: String) =>
bindOption(gOp(x + "z"), (y: Boolean) =>
hOp(!y)))
Now suppose that our original client code was not h(!g(f(27) + "z"))
but instead !g(f(27) + "z"). How can we express this with bindOption? This
thing does not type check:
def clientCode =
bindOption(f(27), (x: String) =>
bindOption(g(x + "z"), (y: Boolean) =>
!y))
One way to fix the situation is to insert a call to Some, like so:
def clientCode2Op =
bindOption(fOp(27), (x: String) =>
bindOption(gOp(x + "z"), (y: Boolean) =>
Some(!y)))
While this works, it is incompatible with our original goal of abstracting over the function composition pattern, because the
Some constructor exposes what kind of pattern we are currently dealing with. Hence let's abstract over it by adding a second
function unit to our function composition interface:
def unit[A](x: A): Option[A] = Some(x)
def clientCode2OpUnit =
bindOption(fOp(27), (x: String) =>
bindOption(gOp(x + "z"), (y: Boolean) =>
unit(!y)))
This looks better, but the types of unit and bindOption (and also the name, but we can of course change that) still
reveal that we are dealing with the Option function-composition pattern. Let's abstract over the Option type constructor
by turning the type constructor into a parameter. The resulting triple (type constructor, unit function, bind function) is
called a monad. Certain conditions (the "monad laws") on unit and bind also need to hold to make it a true monad,
but we'll defer a discussion of these conditions until later.
The Monad Interface
So here it is: The Monad interface.
trait Monad[M[_]] {
def unit[A](a: A): M[A]
def bind[A, B](m: M[A], f: A => M[B]): M[B]
// The "monad laws":
// 1) "unit" acts as a kind of neutral element of "bind", that is:
// 1a) bind(unit(x), f) == f(x) and
// 1b) bind(x, y => unit(y)) == x
// 2) Bind enjoys an associative property
// bind(bind(x, f), g) == bind(x, y => bind(f(y), g))
}
Using this interface, we can now make clientCode depend only on this interface, but no longer on the Option type:
def clientCode2Op(m: Monad[Option]) =
m.bind(fOp(27), (x: String) =>
m.bind(gOp(x + "z"), (y: Boolean) =>
m.unit(!y)))
If the API is parametric in the monad, we can make the client code fully parametric, too. We model the monad object as an implicit parameter to save the work of passing on the monad in every call.
def fM[M[_]](n: Int)(using m: Monad[M]): M[String] = sys.error("not implemented")
def gM[M[_]](x: String)(using m: Monad[M]): M[Boolean] = sys.error("not implemented")
def hM[M[_]](b: Boolean)(using m: Monad[M]): M[Int] = sys.error("not implemented")
def clientCode2[M[_]](using m: Monad[M]) =
m.bind(fM(27), (x: String) =>
m.bind(gM(x + "z"), (y: Boolean) =>
m.unit(!y)))
For-Comprehension Syntax
All these nested calls to bind can make the code hard to read. Luckily, there is a notation called "monad-comprehension" to make
monadic code look simpler. Monad-comprehensions are directly supported in Haskell and some other languages. In Scala, we can
piggy-back on the "for-comprehension" syntax instead.
A "for-comprehension" is usually used for lists and other collections. For instance:
val l = List(List(1, 2), List(3, 4))
assert((for { x <- l; y <- x } yield y + 1) == List(2, 3, 4, 5))
The Scala compiler desugars the for-comprehension above into calls of the standard map and flatMap functions. That is, the above
for-comprehension is equivalent to:
assert(l.flatMap(x => x.map(y => y + 1)) == List(2, 3, 4, 5))
We will make use of for-comprehension syntax by supporting both flatMap (which is like bind) and map (which is like fmap).
We support these functions by an implicit conversion to an object that supports these functions as follows:
extension [A, M[_]](m: M[A])(using mm: Monad[M])
def map[B](f: A => B): M[B] = mm.bind(m, (x: A) => mm.unit(f(x)))
def flatMap[B](f: A => M[B]): M[B] = mm.bind(m, f)
Using the new support for for-comprehension syntax, we can rewrite our client code as follows: Given the API from above,
def fOp(n: Int): Option[String] = if (n < 100) Some("x") else None
def gOp(x: String): Option[Boolean] = Some(x == "x")
def hOp(b: Boolean): Option[Int] = if (b) Some(27) else None
We can now rewrite this
def clientCode2Op(m: Monad[Option]) =
m.bind(fOp(27), (x: String) =>
m.bind(gOp(x + "z"), (y: Boolean) =>
m.unit(!y)))
to this:
def clientCode2OpFor(using m: Monad[Option]) =
for {
x <- fOp(27)
y <- gOp(x + "z")
} yield !y
The Option Monad
Let's look at some concrete monads now. We have of course already seen one particular monad: The Option monad. This monad is also
sometimes called the Maybe monad.
object OptionMonad extends Monad[Option] {
override def bind[A, B](a: Option[A], f: A => Option[B]): Option[B] =
a match {
case Some(x) => f(x)
case None => None
}
override def unit[A](a: A) = Some(a)
}
We can now parameterize clientCode with OptionMonad.
def v: Option[Boolean] = clientCode2Op(OptionMonad)
Generic Functions for Monads
There are many other sensible monads. Before we discuss those, let us discuss whether there are useful functions that are generic enough to be useful for many different monads. Here are some of these functions:
fmap turns every function between A and B into a function between M[A] and M[B]:
def fmap[M[_], A, B](f: A => B)(using m: Monad[M]): M[A] => M[B] =
a => m.bind(a, (x: A) => m.unit(f(x)))
In fancy category theory terms, we can say that every monad is a functor.
sequence composes a list of monadic values into a single monadic value which is a list.
def sequence[M[_], A](l: List[M[A]])(using m: Monad[M]): M[List[A]] = l match {
case x :: xs => m.bind(x, (y: A) =>
m.bind(sequence(xs), (ys: List[A]) =>
m.unit(y :: ys)))
case Nil => m.unit(List.empty)
}
mapM composes sequence and the standard map function:
def mapM[M[_], A, B](f: A => M[B], l: List[A])(using m: Monad[M]): M[List[B]] =
sequence(l.map(f))
join is another useful function to unwrap a layer of monads.
In category theory, monads are defined via unit (denoted by the greek letter η)
and join (denoted μ) instead of unit and bind. There are additional "naturality" and
"coherence conditions" that make the category theory definition equivalent to ours.
def join[M[_], A](x: M[M[A]])(using m: Monad[M]): M[A] = m.bind(x, (y: M[A]) => y)
Here are some other common monads:
The Identity Monad
The identity monad is the simplest monad which corresponds to ordinary function application. If we parameterize monadic code with the identity monad, we get the behavior of the original non-monadic code.
type Id[X] = X
object IdentityMonad extends Monad[Id] {
def bind[A, B](x: A, f: A => B): B = f(x)
def unit[A](a: A): A = a
}
The Reader Monad
This is the reader monad, a.k.a. environment monad. It captures the essence of "environment-passing style".
The type parameter [A] =>> R => A may look a bit complicated, but
it is merely "currying" the function arrow type constructor.
The type constructor which is created here is M[A] = R => A
trait ReaderMonad[R] extends Monad[[A] =>> R => A] {
// pass the "environment" r into both computations
override def bind[A, B](x: R => A, f: A => R => B): R => B = r => f(x(r))(r)
override def unit[A](a: A): R => A = (_) => a
}
Example: Suppose that all functions in our API above depend on some kind of environment, say, the current configuration.
For simplicitly, let's assume that the current configuration is just an Int, hence all functions have a return type of
the form Int => A:
def fRead(n: Int): Int => String = sys.error("not implemented")
def gRead(x: String): Int => Boolean = sys.error("not implemented")
def hRead(b: Boolean): Int => Int = sys.error("not implemented")
Our original code,
def clientCode = h(!g(f(27) + "z"))
becomes:
def clientCodeRead(env: Int) = hRead(!gRead(fRead(27)(env) + "z")(env))(env)
In monadic form, the explicit handling of the environment disappears again:
def clientCode2Read(using m: ReaderMonad[Int]) =
m.bind(fRead(27), (x: String) =>
m.bind(gRead(x + "z"), (y: Boolean) =>
m.unit(!y)))
/** this code does not work in older versions of Scala */
def clientCode2ReadFor(using m: ReaderMonad[Int]) =
for {
x <- fRead(27)
y <- gRead(x + "z")
} yield !y
The State Monad
The state monad, in which computations depend on a state S
which is threaded through the computations, is defind as follows:
trait StateMonad[S] extends Monad[[A] =>> S => (A, S)] {
override def bind[A, B](x: S => (A, S), f: A => S => (B, S)): S => (B, S) =
// thread the state through the computations
s => x(s) match { case (y, s2) => f(y)(s2) }
override def unit[A](a: A): S => (A, S) = s => (a, s)
}
Example: Assume that our API maintains a state which (for simplicity) we assume to be a single integer. That is, it would look like this:
def fState(n: Int): Int => (String, Int) = sys.error("not implemented")
def gState(x: String): Int => (Boolean, Int) = sys.error("not implemented")
def hState(b: Boolean): Int => (Int, Int) = sys.error("not implemented")
The original code,
def clientCode = h(!g(f(27) + "z"))
becomes:
def clientCodeState(s: Int) =
fState(27)(s) match {
case (x, s2) => gState(x + "z")(s2) match {
case (y, s3) => hState(!y)(s3) }}
In monadic style, however, the state handling disappears once more:
def clientCode2State(using m: StateMonad[Int]) =
m.bind(fState(27), (x: String) =>
m.bind(gState(x + "z"), (y: Boolean) =>
m.unit(!y)))
The List Monad
In the list monad, computations produce lists of results. The bind operator combines all those results in a single list.
object ListMonad extends Monad[List] {
// apply f to each element, concatenate the resulting lists
override def bind[A, B](x: List[A], f: A => List[B]): List[B] = x.flatMap(f)
override def unit[A](a: A) = List(a)
}
Example: Assume that our API functions return lists of results, and our client code must exercise the combination of all possible answers.
def fList(n: Int): List[String] = sys.error("not implemented")
def gList(x: String): List[Boolean] = sys.error("not implemented")
def hList(b: Boolean): List[Int] = sys.error("not implemented")
The original code,
def clientCode = h(!g(f(27) + "z"))
becomes:
def clientCodeList =
fList(27).map(x => gList(x + "z")).flatten.map(y => hList(!y)).flatten
The monadic version of the client code stays the same, as expected:
def clientCode2List = {
given Monad[List] = ListMonad
for {
x <- fList(27)
y <- gList(x + "z")
} yield !y
}
The Continuation Monad
The last monad we are going to present is the continuation monad, which stands for computations that are continuations.
trait ContinuationMonad[R] extends Monad[[A] =>> (A => R) => R] {
type Cont[X] = (X => R) => R
override def bind[A, B](x: Cont[A], f: A => Cont[B]): Cont[B] =
// construct continuation for x that calls f with the result of x
k => x(a => f(a)(k))
override def unit[A](a: A): Cont[A] = k => k(a)
// callcc is like letcc; the difference is that letcc binds a name,
// whereas callcc expects a function as argument.
// That means that letcc(k, ...) is expressed as callcc(k => ...).
def callcc[A, B](f: (A => Cont[B]) => Cont[A]): Cont[A] =
k => f((a: A) => (_: B => R) => k(a))(k)
}
Example: Suppose our API was CPS-transformed:
def fCPS[R](n: Int): (String => R) => R = sys.error("not implemented")
def gCPS[R](x: String): (Boolean => R) => R = sys.error("not implemented")
def hCPS[R](b: Boolean): (Int => R) => R = sys.error("not implemented")
The original code,
def clientCode = h(!g(f(27) + "z"))
becomes:
def clientCodeCPS[R]: (Int => R) => R =
k => fCPS(27)((x: String) => gCPS(x + "z")((y: Boolean) => hCPS(!y)(k)))
The monadic version hides the CPS transformation in the operations of the monad.
def clientCode2CPS[R](using m: ContinuationMonad[R]) =
m.bind(fCPS(27), (x: String) =>
m.bind(gCPS(x + "z"), (y: Boolean) =>
m.unit(!y)))
Let's implement 1 + (2 + 3) in monadic style and implicitly CPS-transform using the continuation monad:
// unfortunately we can, again, not use for-comprehension syntax
def ex123[R](using m: ContinuationMonad[R]) = {
m.bind(
m.bind(m.unit(2), (two: Int) =>
m.bind(m.unit(3), (three: Int) => m.unit(two + three))),
(five: Int) => m.unit(1 + five))
}
def runEx123 = ex123(using new ContinuationMonad[Int]{})(x => x)
Let's implement the (+ 1 (let/cc k (+ 2 (k 3)))) example using callcc
def excallcc[R](using m: ContinuationMonad[R]) = {
m.bind(
m.bind(m.unit(2), (two: Int) =>
m.callcc[Int, Int](k => m.bind(k(3), (three: Int) => m.unit(two + three)))),
(five: Int) => m.unit(1 + five))
}
def runExcallcc = excallcc(using new ContinuationMonad[Int]{})(x => x)
Remember how we had to CPS-transform the map function in the "allCosts" example when we talked about continuations?
Now we can define a monadic version of map that works for any monad, including the continuation monad:
def mapM[M[_], A, B](x: List[A], f: A => M[B])(using m: Monad[M]): M[List[B]] =
sequence(x.map(f))
Monad Transformers
The purpose of monad transformers is to compose monads. For instance, what if we want to have both the list monad and the option monad at the same time? Such situations arise very often in practical code.
One solution is to have a monad transformer version of each monad, which is parameterized with another monad. We show this for the Option monad case.
type OptionT[M[_]] = [A] =>> M[Option[A]]
class OptionTMonad[M[_]](val m: Monad[M]) extends Monad[OptionT[M]] {
override def bind[A, B](x: M[Option[A]], f: A => M[Option[B]]): M[Option[B]] =
m.bind(x, (z: Option[A]) => z match { case Some(y) => f(y)
case None => m.unit(None) })
override def unit[A](a: A) = m.unit(Some(a))
def lift[A](x: M[A]): M[Option[A]] = m.bind(x, (a: A) => m.unit(Some(a)))
}
val ListOptionM = new OptionTMonad(ListMonad)
// in this case, for-comprehension syntax doesn't work because it clashes with the
// built-in support for for-comprehensions for lists :-(
def example = {
val m = ListOptionM
m.bind(List(Some(3), Some(4)), (x: Int) => m.unit(x + 1))
}
def example2 = {
val m = ListOptionM
m.bind(List(Some(3), Some(4)), (x: Int) => m.lift(List(1, 2, 3, x)))
}
def example3 = {
val m = ListOptionM
m.bind(List(Some(3), None, Some(4)), (x: Int) => m.unit(x + 1))
}
def example4 = {
val m = ListOptionM
m.bind(List(Some(3), Some(4)), (x: Int) => if (x > 3) m.m.unit(None) else m.unit(x * 2))
}
Monad transformers are a standard way to compose monads, e.g., in Haskell and in Scala. They have a number of well-known disadvantages. For instance, one needs additional transformer versions of monads and the required lifting sometimes destroys modularity. There are a number of alternative proposals to monad transformers, such as "extensible effects".
IO Monad
The content of this chapter is available as a Scala file here.
trait IOMonad {
type IO[_]
def unit[A](a: A): IO[A]
def bind[A, B](m: IO[A], f: A => IO[B]): IO[B]
def printString(s: String): IO[Unit]
def inputString: IO[String]
def performIO[A](action: IO[A]): A
}
val iomonad: IOMonad = new IOMonad {
type World = String
type IO[A] = World => (A, World)
def unit[A](a: A): IO[A] = w => (a, w)
def bind[A, B](m: IO[A], f: A => IO[B]): IO[B] =
w => m(w) match { case (a, w2) => f(a)(w2) }
def printString(s: String): IO[Unit] =
w => { println(s); ((), w + s + " was printed and then ...\n") }
def inputString: IO[String] =
w => {
val input = scala.io.StdIn.readLine();
(input, w + input + " was entered and then ...\n")
}
def performIO[A](action: IO[A]): A =
action("The world in which nothing has happened yet, but then ...\n") match {
case (a, w) =>
println("Peformed all actions. The world in which all this happened is: \n" + w); a
}
}
def someIOActions(implicit m: IOMonad): m.IO[Unit] =
m.bind(m.printString("Enter your first name:"), (_: Unit) =>
m.bind(m.inputString, (firstName: String) =>
m.bind(m.printString("Enter your last name:"), (_: Unit) =>
m.bind(m.inputString, (lastName: String) =>
m.printString("Hello, " + firstName + " " + lastName + "!")))))
def test = iomonad.performIO(someIOActions(iomonad))
Modular Interpreters
The content of this chapter is available as a Scala file here.
A Monad Library
We define a Monad library in Scala. Monad libraries like in scalaz and cats (for Scala) or the Haskell standard library look similar.
trait Monad {
type M[_] // this time we treat M as a type member and not as type parameter
// because it leads to shorter type signatures
def unit[A](a: A): M[A]
def bind[A, B](m: M[A], f: A => M[B]): M[B]
extension [A](m: M[A])
def map[B](f: A => B): M[B] = bind(m, (x: A) => unit(f(x)))
def flatMap[B](f: A => M[B]): M[B] = bind(m, f)
}
We formulate concrete monads in the form of abstract interfaces first.
The idea of those interfaces is that it should be possible to use
the monad only in terms of that interface, without knowing anything
about M. The advantage of this approach is that it enables us to
compose monads. M changes in every composition of monads. For instance,
when composing the list monad and the option monad, then
M[X] = Option[List[X]] or M[X] = List[Option[X]].
By keeping M abstract and using it only via the interfaces, "client code"
does not need to depend on the particular composition of monads.
Reader Monad
The Reader (or Environment) monad captures computations that depend
on an environment of type R.
The ask function yields the current environment, the local function
is used to transform the environment in a subcomputation a by an
environment transformer f.
trait ReaderMonad extends Monad {
type R
def ask: M[R]
def local[A](f: R => R, a: M[A]): M[A]
}
The standard implementation of the Reader monad:
trait ReaderMonadImp extends ReaderMonad {
type M[X] = R => X
def unit[A](a: A): M[A] = r => a
def bind[A, B](m: M[A], f: A => M[B]): M[B] = r => f(m(r))(r)
def ask: M[R] = identity
def local[A](f: R => R, a: M[A]): M[A] = r => a(f(r))
}
An example of using the Reader monad to propagate an environment
of type Int through a computation.
object ReaderExample extends ReaderMonadImp {
type R = Int
def example: M[Int] = for { x <- ask } yield (x + 1)
def example2: M[Int] = local(r => 99, example)
}
A more useful example where we use the Reader monad
to propagate a mapping from identifiers to boolean values
in an interpreter for boolean formulas. Note that the signature of
eval is identical to def eval(e: Exp): Map[String, Boolean] => Boolean,
that is, we curry eval to make it applicable to the Reader monad.
object ReaderExample2 extends ReaderMonadImp {
enum Exp:
case Id(x: String)
case And(l: Exp, r: Exp)
case Or(l: Exp, r: Exp)
import Exp._
type R = Map[String, Boolean]
def eval(e: Exp): M[Boolean] = e match {
case Id(x) => for {env <- ask } yield env(x)
case And(l, r) => for {
x <- eval(l)
y <- eval(r)
} yield (x && y)
case Or(l, r) => for {
x <- eval(l)
y <- eval(r)
} yield (x || y)
}
}
The implementation of the And case is semantically equivalent to this code:
case And(l, r) => env => {
val x = eval(l)(env)
val y = eval(r)(env)
x && y
}
However, the monadic code is more abstract (and hence
more reusable) because it is not coupled to the concrete M.
State Monad
This is the interface and standard implementation for the State monad:
trait StateMonad extends Monad {
type S
def getState: M[S]
def putState(s: S): M[Unit]
}
trait StateMonadImp extends StateMonad {
type M[A] = S => (A, S)
def unit[A](a: A): M[A] = (s: S) => (a, s)
def bind[A, B](m: M[A], f: A => M[B]): M[B] = (s: S) => {
val (a, s2) = m(s)
f(a)(s2)
}
def getState: M[S] = s => (s, s)
def putState(s: S): M[Unit] = _ => ((), s)
}
Continuation Monad
And here is the interface for the Continuation monad. The Continuation monad provides
a method callcc, which reifies the current Continuation k: A => M[B].
trait ContinuationMonad extends Monad {
def callcc[A, B](f: (A => M[B]) => M[A]): M[A]
}
Implementaions
Now we provide implementations of the monad interfaces.
The identity monad, which is the end of each transformer chain reads:
trait IdentityMonad extends Monad {
type M[A] = A
def unit[A](a: A): M[A] = a
def bind[A, B](m: M[A], f: A => M[B]) = f(m)
}
object IdentityMonad extends IdentityMonad
We organize most other monads as monad transformers. A monad transformer is parameterized with another monad. The monads are organized in a chain. Operations of "inner" monads must be lifted to top-level operations.
trait MonadTransformer extends Monad {
val m: Monad
}
Reader Monad Transformer
The Reader monad transformer. We provide some convenient
functions lift, lift2 etc. to lift functions from the inner monad.
Note that M[X] = R => m.M[X] instead of M[X] = R => X (as for
the non-transformer version of the Reader monad).
The correct implementation of the interface methods follows from
this type equation.
trait ReaderT extends MonadTransformer with ReaderMonad {
type R
override type M[X] = R => m.M[X]
override def unit[A](a: A): M[A] = r => m.unit(a)
override def bind[A, B](x: M[A], f: A => M[B]): M[B] =
r => m.bind(x(r), (n: A) => f(n)(r))
override def ask: M[R] = r => m.unit(r)
override def local[A](f: R => R, a: M[A]): M[A] = r => a(f(r))
protected implicit def lift[A](x: m.M[A]): M[A] = r => x
protected implicit def lift2[A, B](x: A => m.M[B]): A => M[B] = a => lift(x(a))
protected implicit def lift3[A, B, C](x: (A => m.M[B]) => m.M[C]): (A => M[B]) => M[C] =
f => r => x((a: A) => f(a)(r))
protected implicit def lift4[A, B, C, D](x: ((A => m.M[B]) => m.M[C]) => m.M[D]): ((A => M[B]) => M[C]) => M[D] =
f => r => x((a: A => m.M[B]) => f(lift2(a))(r))
}
// The original Reader monad can be reconstructed by composing ReaderT with the identity monad.
trait ReaderMonadImpl extends ReaderT {
val m: IdentityMonad = IdentityMonad
}
We do not need this because we have just synthesized it:
trait ReaderMonadImpl extends ReaderMonad {
type M[X] = R => X
def unit[A](a: A): M[A] = r => a
def bind[A, B](m: M[A], f: A => M[B]): M[B] = r => f(m(r))(r)
def ask: M[R] = identity
def local[A](f: R => R, a: M[A]): M[A] = (r) => a(f(r))
}
State Monad Transformer
The design of StateT is similar to that of ReaderT:
trait StateT extends MonadTransformer with StateMonad {
type M[A] = S => m.M[(A, S)]
override def unit[A](a: A): M[A] = (s: S) => m.unit(a, s)
override def bind[A, B](x: M[A], f: A => M[B]): M[B] = (s: S) => {
m.bind[(A, S), (B, S)](x(s), { case (a, s2) => f(a)(s2)})
}
override def getState: M[S] = s => m.unit((s, s))
override def putState(s: S): M[Unit] = _ => m.unit(((), s))
}
// and again we can reconstruct the ordinary State monad.
trait StateMonadImpl extends StateT {
val m: IdentityMonad = IdentityMonad
}
We do not need this because we have just synthesized it:
trait StateMonadImpl extends StateMonad {
type M[A] = S => (A, S)
def unit[A](a: A): M[A] = (s: S) => (a, s)
def bind[A, B](m: M[A], f: A => M[B]): M[B] = (s: S) => {
val (a, s2) = m(s)
f(a)(s2)
}
def getState: M[S] = s => (s, s)
def putState(s: S): M[Unit] = _ => ((), s)
}
Continuation Monad
We could also synthesize ContinuationMonadImpl from a ContT
just as we did for ReaderMonadImpl and StateMonadImpl,
but for simplicity we only present the ordinary Continuation monad here.
trait ContinuationMonadImpl extends ContinuationMonad {
type T
type M[A] = (A => T) => T
override def unit[A](a: A): M[A] = k => k(a)
override def bind[A, B](m: M[A], f: A => M[B]): M[B] = k => m(a => f(a)(k))
override def callcc[A, B](f: (A => M[B]) => M[A]): M[A] = k => f(a => _ => k(a))(k)
}
Compositions
Let's compose some monads.
The composition of the Reader monad and some Continuation monad.
trait ReaderContinuationMonadForwarder extends ReaderT with ContinuationMonad {
val m: ContinuationMonad
// call to lift4 inserted automatically
override def callcc[A, B](f: (A => M[B]) => M[A]): M[A] = (m.callcc[A, B] _)(f)
}
Fro the implementation, we use the Continuation-monad implementation.
trait ReaderContinuationMonadImpl extends ReaderContinuationMonadForwarder {
type T
val m: ContinuationMonadImpl { type T = ReaderContinuationMonadImpl.this.T } =
new ContinuationMonadImpl { type T = ReaderContinuationMonadImpl.this.T }
}
Composition of the Reader monad with some State monad.
trait ReaderStateMonadForwarder extends ReaderT with StateMonad {
val m: StateMonad { type S = ReaderStateMonadForwarder.this.S }
override def getState: M[S] = m.getState
override def putState(s: S): M[Unit] = m.putState(s)
}
And the implementation with StateMonadImpl.
trait ReaderStateMonadImpl extends ReaderStateMonadForwarder {
val m: StateMonadImpl { type S = ReaderStateMonadImpl.this.S } =
new StateMonadImpl { type S = ReaderStateMonadImpl.this.S }
}
A Modular Interpreter
Now we use the monad library to modularize the interpreters of the various language variants we have seen so far.
trait Expressions extends Monad {
abstract class Value
abstract class Exp {
def eval: M[Value]
}
}
trait Numbers extends Expressions {
case class NumV(n: Int) extends Value
}
trait Arithmetic extends Numbers {
case class Num(n: Int) extends Exp {
def eval = unit(NumV(n))
}
implicit def num2exp(n: Int): Exp = Num(n)
case class Add(lhs: Exp, rhs: Exp) extends Exp {
def eval = for {
l <- lhs.eval
r <- rhs.eval
} yield (l, r) match {
case (NumV(v1), NumV(v2)) => NumV(v1 + v2)
case _ => sys.error("can only add numbers")
}
}
}
trait If0 extends Numbers {
case class If0(cond: Exp, thenExp: Exp, elseExp: Exp) extends Exp {
def eval = for {
c <- cond.eval
res <- c match {
case NumV(0) => thenExp.eval
case _ => elseExp.eval
}
} yield res
}
}
trait Functions extends Expressions with ReaderMonad {
type Env = Map[String, Value]
override type R = Env
case class ClosureV(f: Fun, env: Env) extends Value
case class Fun(param: String, body: Exp) extends Exp {
def eval = for { env <- ask } yield ClosureV(this, env)
}
case class Ap(f: Exp, a: Exp) extends Exp {
def eval = for {
fv <- f.eval
av <- a.eval
res <- fv match {
case ClosureV(fun, cenv) =>
local(env => cenv + (fun.param -> av), fun.body.eval)
}
} yield res
}
case class Id(x: String) extends Exp {
def eval = for {
env <- ask
} yield env(x)
}
implicit def id2exp(x: String): Exp = Id(x)
def wth(x: String, xdef: Exp, body: Exp): Exp = Ap(Fun(x, body), xdef)
}
trait Boxes extends Expressions with StateMonad {
type Store = Map[Address, Value]
override type S = Store
type Address = Int
var _nextAddress = 0
def nextAddress: Address = {
_nextAddress += 1
_nextAddress
}
case class AddressV(a: Address) extends Value
case class NewBox(e: Exp) extends Exp {
def eval = {
val a = nextAddress
for {
v <- e.eval
s <- getState
_ <- putState(s + (a -> v))
} yield AddressV(a)
}
}
case class SetBox(b: Exp, e: Exp) extends Exp {
def eval =
for {
box <- b.eval
ev <- e.eval
s <- getState
_ <- putState(box match { case AddressV(a) => s.updated(a, ev) })
} yield ev
}
case class OpenBox(b: Exp) extends Exp {
def eval = for {
bv <- b.eval
s <- getState
} yield (bv match { case AddressV(a) => s(a) })
}
case class Seq(e1: Exp, e2: Exp) extends Exp {
def eval = bind(e1.eval, (_: Value) => e2.eval)
}
}
trait Letcc extends Expressions with ContinuationMonad with ReaderMonad {
override type R = Map[String, Value]
// We introduce a new application form CAp instead of using Ap because we cannot extend Ap
case class CAp(f: Exp, a: Exp) extends Exp {
override def eval: M[Value] =
for {
fv <- f.eval
av <- a.eval
res <- fv match { case ContV(f) => f(av) }
} yield res
}
case class Letcc(param: String, body: Exp) extends Exp {
override def eval: M[Value] =
callcc[Value, Value](k => local(env => env + (param -> ContV(k)), body.eval))
}
case class ContV(f: Value => M[Value]) extends Value
}
Let's compose together some languages!
object AE extends Arithmetic with IdentityMonad {
val aetest = Add(1, Add(2, 3))
}
assert(AE.aetest.eval == AE.NumV(6))
object FAELang extends Functions with Arithmetic with ReaderMonadImpl {
val faetest = Ap(Fun("x", Add("x", 1)), Add(2, 3))
assert(faetest.eval(Map.empty) == NumV(6))
}
object BCFAE extends Boxes with Arithmetic with Functions with If0 with ReaderStateMonadImpl {
val test = wth("switch", NewBox(0),
wth("toggle", Fun("dummy", If0(OpenBox("switch"),
Seq(SetBox("switch", 1), 1),
Seq(SetBox("switch", 0), 0))),
Add(Ap("toggle", 42), Ap("toggle", 42))))
}
assert(BCFAE.test.eval(Map.empty)(Map.empty)._1 == BCFAE.NumV(1))
object FAEwLetcc extends Arithmetic with Functions with If0 with Letcc with ReaderContinuationMonadImpl {
override type T = Value
val testprog = Add(1, Letcc("k", Add(2, CAp("k", 3))))
}
assert(FAEwLetcc.testprog.eval(Map.empty)(identity) == FAEwLetcc.NumV(4))
Monadic Reflection
The content of this chapter is available as a Racket file here.
#lang racket
(require racket/control)
Monadic style can encode continuation-passing style:
Just use the continuation monad.
But the converse is also true in a certain sense that was discovered by A. Filinski, who invented the notion of "monadic reflection". Here, we exemplify monadic reflection in terms of the list monad, but it is straightforward to abstract over the concrete monad and make this work for every monad.
The list monad operations
(define (return x) (list x))
(define (bind m f)
(apply append (map f m)))
Monadic reflection (Filinski)
; List[A] -> A (quasi-type)
(define (reflect m)
(shift k (bind m k)))
; A -> List[A] (quasi-type)
; this is a macro that transforms (reify e) into (reify-thunk (thunk e))
; its sole purpose is to prevent the evaluation of e and wrap it into a thunk
(define-syntaxes (reify)
(syntax-rules ()
[(_ e)
(reify-thunk (thunk e))]))
(define (reify-thunk t)
(reset (return (t))))
Now we can write direct-style programs (in this case: a direct-style + function), yet use monadic features.
(reify (+ (reflect (list 1 2)) (reflect (list 3 4))))
More information in "Representing Monads" by A. Filinski.
Example: Backtracking using monadic reflection: The n-queens problem.
If partial results are desired, lists should be replaced by streams.
(define (fail) (reflect empty))
; Nat List[Nat] Nat -> Bool
(define (safe x l n)
(or (empty? l)
(let ((c (first l)))
(and (not (= x c))
(not (= x (+ c n)))
(not (= x (- c n)))
(safe x (rest l) (+ n 1))))))
(define (queens n)
(foldl (lambda (_ y)
(let ((next (reflect (inclusive-range 1 n))))
(if (safe next y 1)
(cons next y)
(fail))))
empty
(inclusive-range 1 n)))
(reify (queens 8))
Defunctionalization, Refunctionalization
The content of this chapter is available as a Scala file here.
In the discussion of syntactic interpretation vs. meta interpretation we have learned that we only learn something about (and control) a language feature if we choose syntactic interpretation.
Today we want to discuss techniques with which we can make our interpreter so syntactic that it corresponds to an abstract machine: A machine with a (possibly infinite) set of states and a simple transition relation between the states. We already know the technique with which we can take control over the call stack management: CPS transformation. After CPS-transforming the interpreter, we do not rely on the order of evaluation and call stack management of the meta-language anymore. We replicate its definition here:
enum Exp:
case Num(n: Int)
case Id(name: String)
case Add(lhs: Exp, rhs: Exp)
case Fun(param: String, body: Exp)
case Ap(funExpr: Exp, argExpr: Exp)
object Exp:
implicit def num2exp(n: Int): Exp = Num(n)
implicit def id2exp(s: String): Exp = Id(s)
import Exp._
sealed abstract class Value
type Env = Map[String, Value]
case class NumV(n: Int) extends Value
case class ClosureV(f: Fun, env: Env) extends Value
object CPSTransformed {
def eval[T](e: Exp, env: Env, k: Value => T): T = e match {
case Num(n: Int) => k(NumV(n))
case Id(x) => k(env(x))
case Add(l, r) =>
eval(l, env,
lv => eval(r, env,
rv => (lv, rv) match {
case (NumV(v1), NumV(v2)) => k(NumV(v1 + v2))
case _ => sys.error("can only add numbers")
}))
case f@Fun(param, body) => k(ClosureV(f, env))
case Ap(f, a) =>
eval(f, env,
cl => cl match {
case ClosureV(f, closureEnv) =>
eval(a, env,
av => eval(f.body, closureEnv + (f.param -> av), k))
case _ => sys.error("can only apply functions")
})
}
}
However, the CPS-transformed interpreter still uses high-level features of the meta-language, most notably first-class functions. We will now introduce one transformation that can be used to transform a program using higher-order functions into one using only first-order functions. It is a general program transformation technique, not restricted only to interpreters.
Lambda Lifting
The first of these techniques is lambda lifting. The goal of lambda lifting is to turn local functions into top-level functions. That is, all "lambdas" only occur at the top-level. Variables in the local environment that are normally stored in the function's closure are instead passed as parameters to the top-level function. Lambda lifting is accomplished by the following steps:
- Invent a new and unique name for each function that is not a top-level function.
- Create a function with this name. Its body is the body of the former local function. Such a function will contain free variables.
- Add a parameter to the so-obtained top-level function for each free variable in its body. Hence, it becomes a higher-order function that returns a function when passed these arguments.
- Replace the local function by a call to the new top-level function and pass the corresponding local context via the arguments created in step 3.
Example: Let's lambda-lift the functions y => y + n and y => y * n in
def map(f: Int => Int, xs: List[Int]): List[Int] = xs match {
case Nil => Nil
case (x :: xs) => f(x) :: map(f, xs)
}
def addAndMultNToList(n: Int, xs: List[Int]) = map(y => y * n, map(y => y + n, xs))
We create two new top-level functions, let's call them f and g. Their bodies are respectively y => y + n and y => y * n.
We add a parameter for each free variable. In the example, the free variable is n in both cases:
def fLam(n: Int) = (y: Int) => y + n
def gLam(n: Int) = (y: Int) => y * n
or shorter:
def f(n: Int)(y: Int) = y + n
def g(n: Int)(y: Int) = y * n
The local function can now be replaced by a call to the new global function.
def addAndMultNToListLifted(n: Int, xs: List[Int]) = map(g(n)(_), map(f(n)(_), xs))
Let's now perform the same technique to the CPS-transformed interpreter given above. It contains local functions in four places:
two in the Add branch and two in the Ap branch. We call the corresponding top-level functions, from left to right,
addC1, addC2, apC1 and apC2.
An interesting novelty in the interpreter is that some local functions (corresponding to addC1 and apC1) create local
functions themselves. This means that addC1 must call addC2 and apC1 must call apC2. The rest of the transformation
is a straightforward application of the transformation steps described above:
object LambdaLifted {
def addC1[T](r: Exp, env: Env, k: Value => T)(lv: Value) =
eval(r, env, addC2(lv, k))
def addC2[T](lv: Value, k: Value => T)(rv: Value) = (lv, rv) match {
case (NumV(v1), NumV(v2)) => k(NumV(v1 + v2))
case _ => sys.error("can only add numbers")
}
def apC1[T](a: Exp, env: Env, k: Value => T)(cl: Value) = cl match {
case ClosureV(f, closureEnv) => eval(a, env, apC2(f, closureEnv, k))
case _ => sys.error("can only apply functions")
}
def apC2[T](f: Fun, closureEnv: Env, k: Value => T)(av: Value) =
eval(f.body, closureEnv + (f.param -> av), k)
def eval[T](e: Exp, env: Env, k: Value => T): T = e match {
case Num(n: Int) => k(NumV(n))
case Id(x) => k(env(x))
case Add(l, r) => eval(l, env, addC1(r, env, k))
case f@Fun(param, body) => k(ClosureV(f, env))
case Ap(f, a) => eval(f, env, apC1(a, env, k))
}
}
The lambda-lifted interpreter contains no local functions anymore, but it still contains higher-order functions, since addC1 etc.
return functions that are passed as parameters to other functions.
Defunctionalization
Defunctionalization is a program transformation technique that turns higher-order programs that have already been lambda-lifted
into first-order programs that contain no higher-order functions anymore. Any program contains only finitely many function definitions.
The idea of defunctionalization is to assign a unique identifier to each of these function definitions. The function-"dispatch" then
happens in a function apply, which receives the identifier corresponding to a function definition and dispatches the identifier
to the right function body. Every function application within the program is then replaced by a call to the apply function with
the function identifier as the first argument.
In addition to the unique identifier, the apply function also needs bindings for the free variables in the function body.
Hence we need to store the values for these free variables along with the unique identifier. Finally, the apply function needs
to know about the arguments to the function. These become additional parameters of the apply function.
Let's illustrate defunctionalization in the addAndMultNToList example from above.
enum FunctionValue:
case F(n: Int)
case G(n: Int)
import FunctionValue._
def apply(f: FunctionValue, y: Int): Int = f match {
case F(n) => y + n
case G(n) => y * n
}
def map(f: FunctionValue, xs: List[Int]): List[Int] = xs match {
case Nil => Nil
case (x :: xs) => apply(f, x) :: map(f, xs)
}
def addAndMultNToListDefun(n: Int, xs: List[Int]) = map(G(n), map(F(n), xs))
Let's now apply defunctionalization to our CPS-transformed interpreter:
object Defunctionalized {
enum FunctionValue[T]:
case AddC1(r: Exp, env: Env, k: FunctionValue[T]) extends FunctionValue[T]
case AddC2(lv: Value, k: FunctionValue[T]) extends FunctionValue[T]
case ApC1(a: Exp, env: Env, k: FunctionValue[T]) extends FunctionValue[T]
case ApC2(f: Fun, closureEnv: Env, k: FunctionValue[T]) extends FunctionValue[T]
import FunctionValue._
def apply[T](fv: FunctionValue[T], v: Value): T = fv match {
case AddC1(r, env, k) => eval(r, env, AddC2(v, k))
case AddC2(lv, k) => (lv, v) match {
case (NumV(v1), NumV(v2)) => apply(k, NumV(v1 + v2))
case _ => sys.error("can only add numbers")
}
case ApC1(a, env, k) => v match {
case ClosureV(f, closureEnv) => eval(a, env, ApC2(f, closureEnv, k))
case _ => sys.error("can only apply functions")
}
case ApC2(f, closureEnv, k) => eval(f.body, closureEnv + (f.param -> v), k)
}
def eval[T](e: Exp, env: Env, k: FunctionValue[T]): T = e match {
case Num(n: Int) => apply(k, NumV(n))
case Id(x) => apply(k, env(x))
case Add(l, r) => eval(l, env, AddC1(r, env, k))
case f@Fun(param, body) => apply(k, ClosureV(f, env))
case Ap(f, a) => eval(f, env, ApC1(a, env, k))
}
}
This interpreter can be seen as an abstract machine. The state space of the abstract machine is
(Exp \( \times \) Env \( \times \) FunctionValue) \( \cup \) (FunctionValue \( \times \) Value),
where \( \times \) stands for cross product and \( \cup \) stands for set union.
Every case in the pattern matches in apply and eval can be read as a transition in this state space.
From Interpreter to Abstract Machine
To see that we can read the above functions as transitions of an abstract machine, let's actually
construct that machine.
Its domain of States is the type MachineState[T].
The final state of the machine is Done(v), for some value v.
Its transition function is the function named transition.
We can see every intermediate state of the abstract machine.
Its state is fully described by the (first-order) state type. We are no
longer dependent on call-stack management or higher-order functions of
the meta-language (Scala).
object AbstractMachine {
enum FunctionValue[T]:
case AddC1(r: Exp, env: Env, k: FunctionValue[T]) extends FunctionValue[T]
case AddC2(lv: Value, k: FunctionValue[T]) extends FunctionValue[T]
case ApC1(a: Exp, env: Env, k: FunctionValue[T]) extends FunctionValue[T]
case ApC2(f: Fun, closureEnv: Env, k: FunctionValue[T]) extends FunctionValue[T]
case IdentityFV() extends FunctionValue[Value]
import FunctionValue._
enum MachineState[T]:
case EvalState(e: Exp, env: Env, fv: FunctionValue[T]) extends MachineState[T]
case ApplyState(fv: FunctionValue[T], v: Value) extends MachineState[T]
case Done(v: Value) extends MachineState[Value]
import MachineState._
def transition[T](s: MachineState[T]): MachineState[T] =
s match {
case EvalState(e, env, k) => transitionEval(e, env, k)
case ApplyState(fv, v) => transitionApply(fv, v)
case Done(v) => sys.error("already done")
}
def transitionEval[T](e: Exp, env: Env, k: FunctionValue[T]): MachineState[T] = e match {
case Num(n: Int) => ApplyState(k, NumV(n))
case Id(x) => ApplyState(k, env(x))
case Add(l, r) =>
EvalState(l, env, AddC1(r, env, k))
case f@Fun(param, body) => ApplyState(k, ClosureV(f, env))
case Ap(f, a) => EvalState(f, env, ApC1(a, env, k))
}
def transitionApply[T](fv: FunctionValue[T], v: Value): MachineState[T] = fv match {
case IdentityFV() => Done(v)
case AddC1(r, env, k) => EvalState(r, env, AddC2(v, k))
case AddC2(lv, k) => (lv, v) match {
case (NumV(v1), NumV(v2)) => ApplyState(k, NumV(v1 + v2))
case _ => sys.error("can only add numbers")
}
case ApC1(a, env, k) => v match {
case ClosureV(f, closureEnv) => EvalState(a, env, ApC2(f, closureEnv, k))
case _ => sys.error("can only apply functions")
}
case ApC2(f, closureEnv, k) => EvalState(f.body, closureEnv + (f.param -> v), k)
}
}
import AbstractMachine._
import FunctionValue._
import MachineState._
Now let's try this out with a concrete example and look at the tract of transitions
val test = Ap(Fun("x", Add("x", 1)), 5)
// test: Exp = Ap(
// funExpr = Fun(param = "x", body = Add(lhs = Id(name = "x"), rhs = Num(n = 1))),
// argExpr = Num(n = 5)
// )
val initMS: MachineState[Value] = EvalState(test,
Map.empty,
AbstractMachine.FunctionValue.IdentityFV())
// initMS: MachineState[Value] = EvalState(
// e = Ap(
// funExpr = Fun(
// param = "x",
// body = Add(lhs = Id(name = "x"), rhs = Num(n = 1))
// ),
// argExpr = Num(n = 5)
// ),
// env = Map(),
// fv = IdentityFV()
// )
val s1 = transition(initMS)
// s1: MachineState[Value] = EvalState(
// e = Fun(param = "x", body = Add(lhs = Id(name = "x"), rhs = Num(n = 1))),
// env = Map(),
// fv = ApC1(a = Num(n = 5), env = Map(), k = IdentityFV())
// )
val s2 = transition(s1)
// s2: MachineState[Value] = ApplyState(
// fv = ApC1(a = Num(n = 5), env = Map(), k = IdentityFV()),
// v = ClosureV(
// f = Fun(param = "x", body = Add(lhs = Id(name = "x"), rhs = Num(n = 1))),
// env = Map()
// )
// )
val s3 = transition(s2)
// s3: MachineState[Value] = EvalState(
// e = Num(n = 5),
// env = Map(),
// fv = ApC2(
// f = Fun(param = "x", body = Add(lhs = Id(name = "x"), rhs = Num(n = 1))),
// closureEnv = Map(),
// k = IdentityFV()
// )
// )
val s4 = transition(s3)
// s4: MachineState[Value] = ApplyState(
// fv = ApC2(
// f = Fun(param = "x", body = Add(lhs = Id(name = "x"), rhs = Num(n = 1))),
// closureEnv = Map(),
// k = IdentityFV()
// ),
// v = NumV(n = 5)
// )
val s5 = transition(s4)
// s5: MachineState[Value] = EvalState(
// e = Add(lhs = Id(name = "x"), rhs = Num(n = 1)),
// env = Map("x" -> NumV(n = 5)),
// fv = IdentityFV()
// )
val s6 = transition(s5)
// s6: MachineState[Value] = EvalState(
// e = Id(name = "x"),
// env = Map("x" -> NumV(n = 5)),
// fv = AddC1(r = Num(n = 1), env = Map("x" -> NumV(n = 5)), k = IdentityFV())
// )
val s7 = transition(s6)
// s7: MachineState[Value] = ApplyState(
// fv = AddC1(r = Num(n = 1), env = Map("x" -> NumV(n = 5)), k = IdentityFV()),
// v = NumV(n = 5)
// )
val s8 = transition(s7)
// s8: MachineState[Value] = EvalState(
// e = Num(n = 1),
// env = Map("x" -> NumV(n = 5)),
// fv = AddC2(lv = NumV(n = 5), k = IdentityFV())
// )
val s9 = transition(s8)
// s9: MachineState[Value] = ApplyState(
// fv = AddC2(lv = NumV(n = 5), k = IdentityFV()),
// v = NumV(n = 1)
// )
val s10 = transition(s9)
// s10: MachineState[Value] = ApplyState(fv = IdentityFV(), v = NumV(n = 6))
val s11 = transition(s10)
// s11: MachineState[Value] = Done(v = NumV(n = 6))
We can also automate this into a function that collects the list of all states.
def evalMachine(e: Exp): List[MachineState[Value]] = {
val initMS: MachineState[Value] = EvalState(e,
Map.empty,
AbstractMachine.FunctionValue.IdentityFV())
List.unfold(initMS)({ case Done(v) => None
case s => { val s2 = transition(s); Some((s, s2))}})
}
val q = evalMachine(test)
// q: List[MachineState[Value]] = List(
// EvalState(
// e = Ap(
// funExpr = Fun(
// param = "x",
// body = Add(lhs = Id(name = "x"), rhs = Num(n = 1))
// ),
// argExpr = Num(n = 5)
// ),
// env = Map(),
// fv = IdentityFV()
// ),
// EvalState(
// e = Fun(param = "x", body = Add(lhs = Id(name = "x"), rhs = Num(n = 1))),
// env = Map(),
// fv = ApC1(a = Num(n = 5), env = Map(), k = IdentityFV())
// ),
// ApplyState(
// fv = ApC1(a = Num(n = 5), env = Map(), k = IdentityFV()),
// v = ClosureV(
// f = Fun(param = "x", body = Add(lhs = Id(name = "x"), rhs = Num(n = 1))),
// env = Map()
// )
// ),
// EvalState(
// e = Num(n = 5),
// env = Map(),
// fv = ApC2(
// f = Fun(param = "x", body = Add(lhs = Id(name = "x"), rhs = Num(n = 1))),
// closureEnv = Map(),
// k = IdentityFV()
// )
// ),
// ApplyState(
// fv = ApC2(
// f = Fun(param = "x", body = Add(lhs = Id(name = "x"), rhs = Num(n = 1))),
// closureEnv = Map(),
// k = IdentityFV()
// ),
// v = NumV(n = 5)
// ),
// EvalState(
// e = Add(lhs = Id(name = "x"), rhs = Num(n = 1)),
// env = Map("x" -> NumV(n = 5)),
// fv = IdentityFV()
// ),
// EvalState(
// e = Id(name = "x"),
// env = Map("x" -> NumV(n = 5)),
// ...
Refunctionalization
Can we also invert defunctionalization? That is, can we represent a program such that a data type is replaced by a function type?
Let's look at an example.
enum MyList[T]:
case MyEmptyList() extends MyList[T]
case MyCons(x: T, xs: MyList[T]) extends MyList[T]
import MyList._
def nth[T](l: MyList[T], i: Int): T = l match {
case MyEmptyList() => sys.error("index out of range")
case MyCons(x, xs) => if (i == 0) then x else nth(xs, i - 1)
}
Refunctionalization works smoothly when there is just one pattern match on
a data type. In this case, we represent a list by "its" nth function:
type MyListR[T] = Int => T
def myEmptyList[T]: MyListR[T] = _ => sys.error("index out of range")
def myCons[T](x: T, xs: MyListR[T]): MyListR[T] =
i => if (i == 0) then x else xs(i - 1)
The defunctionalized and the refunctionalized lists differ in their modular structure.
In the defunctionalized version, it is "easy" (only addition of code but no modification
of existing code necessary) to add new functions that pattern-match on lists, such
as a lengthfunction.
def length[T](l: MyList[T]): Int = l match {
case MyEmptyList() => 0
case MyCons(x, xs) => 1 + length(xs)
}
In the refunctionalized version, on the other hand, it is "easy" to add new ways to create lists. For instance, here is a constructor for the infinite list of numbers
def allNats: MyListR[Int] = i => i
The two versions hence corresponds to the two dimensions of the aforementioned "expression problem". These program transformations are hence generally applicable program transformations in a programmer's modularity toolbox.
But what about refunctionalization in the case that there is more than one pattern-match on the
data type? It turns out that we can refunctionalize if we generalize functions to objects, that is,
if we view functions as special kinds of objects with a single apply method.
For instance, in the case of lists with two pattern-matching functions, nth and length,
we can represent lists as objects with two methods, one for each pattern match.
trait MyListRO[T] {
def nth(i: Int): T
def length: Int
}
def myEmptyListO[T]: MyListRO[T] = new MyListRO[T] {
def nth(i: Int): T = sys.error("index out of range")
def length: Int = 0
}
def myConsO[T](x: T, xs: MyListRO[T]): MyListRO[T] = new MyListRO[T] {
def nth(i: Int): T = if (i == 0) then x else xs.nth(i - 1)
def length: Int = 1 + xs.length
}
With this generalization, we can defunctionalize any object type (the transformation could then maybe be called "deobjectionalization") and we can refunctionalize any algebraic data type, and thereby completely invert the extensibility of the program.
Recall that both transformations are global and not compositional, that is, the full program must be transformed at once.
We have glossed over some technical details that would need to be addressed to automate these transformations and make them inverse to each other. For instance, we have not addressed how to reverse the lambda lifting part.
Historical notes: Defunctionalization was proposed by John Reynolds in 1972 in his landmark paper "Definitional Interpreters for Higher-Order Programming Languages". Similar to these lecture notes, Reynolds applied defunctionalization to a CPS-transformed interpreter. The generalization of refunctionalization to use objects instead of functions was presented in a 2015 paper by Rendel, Trieflinger, and Ostermann entitled "Automatic Refunctionalization to a Language with Copattern Matching: With Applications to the Expression Problem". A fully formal account of the transformations that also addresses invertible lambda lifting and proves that the transformations are inverses of each other can be found in the 2020 paper "Decomposition Diversity with Symmetric Data and Codata" by Binder, Jabs, Skupin and Ostermann.
Type Systems
The content of this chapter is available as a Scala file here.
Type Systems
The aim of type systems is to prevent certain classes of errors to occur at runtime. Examples of such errors include the addition of a number to a function, or the usage of a free variable. There can be many different type systems for the same programming language. A sound type systems guarantees that the errors that the type system aims to prevent will not occur in any run of the program. This is different from testing, in which only a single program run on some particular input data is considered.
Since - by Rice's theorem - all interesting properties of the runtime behavior of a program (in a Turing complete language) are undecidable, type systems are necessarily imperfect. But they are usually designed in such a way that the errors are directed:
Each type system unfairly rejects some programs that could be executed without runtime errors. But programs that are accepted by the type system will never produce one of the precluded runtime errors. The latter property is usually called soundness, the former property completeness. Hence we can say that most type systems are sound but not complete. One also often says that type systems are conservative. A conservative approximation of the behavior of a program is one that considers all possible program runs but also some impossible program runs - an overapproximation.
Well-typedness is usually a context-sensitive property, hence it cannot be expressed in the (context-free) grammar of the language but is defined as an additional filter which rules out some syntactically correct programs. Let's look at a small toy language to illustrate type systems:
enum Exp:
case Num(n: Int)
case Add(lhs: Exp, rhs: Exp)
case Bool(x: Boolean)
case If(cond: Exp, thn: Exp, els: Exp)
object Exp:
implicit def num2exp(n: Int): Exp = Num(n)
implicit def bool2exp(x: Boolean): Exp = Bool(x)
import Exp._
def eval(e: Exp): Exp = e match {
case Add(l, r) => (eval(l), eval(r)) match {
case (Num(x), Num(y)) => Num(x + y)
case _ => sys.error("can only add numbers")
}
case If(cond, thn, els) => eval(cond) match {
case Bool(true) => eval(thn)
case Bool(false) => eval(els)
case _ => sys.error("Condition must be boolean")
}
case _ => e
}
In this language, we can see that two different types of runtime errors can occur:
An addition where one of the operands is not a number, or an if-expression where the condition
does not evaluate to a boolean.
Here are a few syntactically correct programs. Only the first three execute correctly. The other ones yield runtime errors.
val ex1 = Add(3, 5)
val ex2 = If(true, 7, 5)
val ex2b = If(true, 7, true)
val ex3 = If(Add(3, 4), 7, true)
val ex4 = Add(true, 3)
Let's now design a type system for this language. Most type systems entail a classification of the values into different types.
In this type system, we choose to define two types, one called BoolType and one called IntType.
enum Type:
case BoolType()
case IntType()
import Type._
A type checker is a compositional assignment of types (or type errors) to expressions. Compositionality means that the type of a composite expression is computed from the type of its subexpressions. Compositionality is quite important for reasoning about types. In this case, the type checker is a rather straightforward structural recursion (= compositionality) over expressions.
def typeCheck(e: Exp): Type = e match {
case Num(n) => IntType()
case Bool(x) => BoolType()
case Add(a, b) => (typeCheck(a), typeCheck(b)) match {
case (IntType(), IntType()) => IntType()
case _ => sys.error("Type Error in addition")
}
case If(c, t, e) => (typeCheck(c), typeCheck(t), typeCheck(e)) match {
case (BoolType(), t1, t2) => if (t1 == t2) t1 else sys.error("Type error in if")
case _ => sys.error("Type error in If")
}
}
Type Soundness
If we typecheck the examples from above with the algorithm, we can see that it rejects all programs that lead to runtime errors, and it also (unfairly) rejects one program that can be executed without error. Hence the type system is conservative, as expected. We can now say more precisely what we mean by soundness of the type checker, namely that it correctly predicts the kind of value that the interpreter will produce:
If
eis an expression andtypeCheck(e)yields a typet, theneval(e)yields a valuevsuch thattypeCheck(v) == t.
This statement of type soundness has to be changed a bit when we have a programming language with non-terminating programs. Then it will have the following form:
If
eis an expression andtypeCheck(e)yields a typet, theneval(e)either diverges, or it yields a valuevsuch thattypeCheck(v) == t, but it does not terminate with a runtime error.
In the most general case, we also have runtime errors that are not captured by the type system. In this case we have to restrict the last part of the sentence to those runtime errors that are captured by the type system.
Simply Typed Lambda Calculus
The content of this chapter is available as a Scala file here.
The Simply Typed Lambda Calculus
We will now consider the so-called Simply Typed Lambda Calculus (STLC). We start with the untyped substitution-based lambda calculus augmented by the possibility to add type annotations to function definitions. The type annotation is ignored by the interpreter. Why are we using the substitution-based interpreter? Because it is simpler to state the type soundness theorem. If we had values that are separate from expressions, we would need to define a type system for these values. This is particularly tricky for closures with their embedded environments.
We also show a couple of standard extensions to the simply typed lambda calculus:
- A unit type
JunitType()with associated termJUnit() Let-bindings (which don't need type annotations)- Type Ascription (corresponding to
:in Scala, like5 + 3: Int) - Products (or Pairs, more specifically)
- Sums (binary sums, more specifically)
To avoid the problem of "guessing" the "from" type in a function definition, we annotate function definitions with the expected argument type.
sealed abstract class Type
enum Exp:
case Num(n: Int)
case Id(name: String)
case Add(lhs: Exp, rhs: Exp)
case Fun(param: String, t: Type, body: Exp)
case Ap(funExpr: Exp, argExpr: Exp)
case Junit()
case Let(x: String, xdef: Exp, body: Exp)
case TypeAscription(e: Exp, t: Type)
case Product(e1: Exp, e2: Exp)
case Fst(e: Exp)
case Snd(e: Exp)
case SumLeft(left: Exp, right: Type)
case SumRight(left: Type, right: Exp)
case EliminateSum(e: Exp, fl: Exp, fr: Exp)
object Exp:
implicit def num2exp(n: Int): Exp = Num(n)
implicit def id2exp(s: String): Exp = Id(s)
import Exp._
def freshName(names: Set[String], default: String): String = {
var last: Int = 0
var freshName = default
while (names contains freshName) { freshName = default + last.toString; last += 1; }
freshName
}
def freeVars(e: Exp): Set[String] = e match {
case Id(x) => Set(x)
case Add(l, r) => freeVars(l) ++ freeVars(r)
case Fun(x, _, body) => freeVars(body) - x
case Ap(f, a) => freeVars(f) ++ freeVars(a)
case Num(n) => Set.empty
case Junit() => Set.empty
case TypeAscription(e, t) => freeVars(e)
case Let(x, xdef, body) => freeVars(xdef) ++ (freeVars(body) - x)
case Product(e1, e2) => freeVars(e1) ++ freeVars(e2)
case Fst(e) => freeVars(e)
case Snd(e) => freeVars(e)
case SumLeft(e, _) => freeVars(e)
case SumRight(_, e) => freeVars(e)
case EliminateSum(e, fl, fr) => freeVars(e) ++ freeVars(fl) ++ freeVars(fr)
}
def subst(e1: Exp, x: String, e2: Exp): Exp = e1 match {
case Num(n) => e1
case Junit() => e1
case Add(l, r) => Add(subst(l, x, e2), subst(r, x, e2))
case Id(y) => if (x == y) e2 else Id(y)
case Ap(f, a) => Ap(subst(f, x, e2), subst(a, x, e2))
case TypeAscription(e, t) => TypeAscription(subst(e, x, e2), t)
case Fun(param, t, body) =>
if (param == x) e1 else {
val fvs = freeVars(body) ++ freeVars(e2)
val newvar = freshName(fvs, param)
Fun(newvar, t, subst(subst(body, param, Id(newvar)), x, e2))
}
case Let(y, ydef, body) =>
if (x == y) Let(y, subst(ydef, x, e2), body) else {
val fvs = freeVars(body) ++ freeVars(e2)
val newvar = freshName(fvs, y)
Let(newvar, subst(ydef, x, e2), subst(subst(body, y, Id(newvar)), x, e2))
}
case Product(a, b) => Product(subst(a, x, e2), subst(b, x, e2))
case Fst(e) => Fst(subst(e, x, e2))
case Snd(e) => Snd(subst(e, x, e2))
case SumLeft(e, t) => SumLeft(subst(e, x, e2), t)
case SumRight(t, e) => SumRight(t, subst(e, x, e2))
case EliminateSum(e, fl, fr) =>
EliminateSum(subst(e, x, e2), subst(fl, x, e2), subst(fr, x, e2))
}
def eval(e: Exp): Exp = e match {
case Id(v) => sys.error("unbound identifier: " + v)
case Add(l, r) => (eval(l), eval(r)) match {
case (Num(x), Num(y)) => Num(x + y)
case _ => sys.error("can only add numbers")
}
case Ap(f, a) => eval(f) match {
case Fun(x, _, body) => eval(subst(body, x, eval(a))) // call-by-value
case _ => sys.error("can only apply functions")
}
case TypeAscription(e, _) => eval(e)
case Let(x, xdef, body) => eval(subst(body, x, eval(xdef)))
case Product(a, b) => Product(eval(a), eval(b))
case Fst(e) => eval(e) match {
case Product(a, b) => a
case _ => sys.error("can only apply Fst to products")
}
case Snd(e) => eval(e) match {
case Product(a, b) => b
case _ => sys.error("can only apply Snd to products")
}
case SumLeft(e, t) => SumLeft(eval(e), t)
case SumRight(t, e) => SumRight(t, eval(e))
case EliminateSum(e, fl, fr) => eval(e) match {
case SumLeft(e2, _) => eval(Ap(fl, e2))
case SumRight(_, e2) => eval(Ap(fr, e2))
case _ => sys.error("can only eliminate sums")
}
case _ => e // numbers and functions evaluate to themselves
}
We classify values into three types: Booleans, integers, and function types. For function types, we need some abstraction for its input
and output; otherwise the type checker cannot be compositional. Luckily we do already have such an abstraction, namely types.
Hence FunType becomes a recursive data type.
case class NumType() extends Type
case class FunType(from: Type, to: Type) extends Type
case class JunitType() extends Type
case class ProductType(fst: Type, snd: Type) extends Type
case class SumType(left: Type, right: Type) extends Type
Let's look at the type checker for the simply typed lambda calculus. To deal with identifiers,
we need an abstraction of environments. A type environment has the form Map[String, Type].
The type checker for the STLC is as follows:
def typeCheck(e: Exp, gamma: Map[String, Type]): Type = e match {
case Num(n) => NumType()
case Junit() => JunitType()
case Id(x) => gamma.get(x) match {
case Some(t) => t
case _ => sys.error("free variable: " ++ x.toString)
}
case Add(l, r) => (typeCheck(l, gamma), typeCheck(r, gamma)) match {
case (NumType(), NumType()) => NumType()
case _ => sys.error("Type error in Add")
}
case Fun(x, t, body) => FunType(t, typeCheck(body, gamma + (x -> t)))
case Ap(f, a) => {
typeCheck(f, gamma) match {
case FunType(from, to) =>
if (from == typeCheck(a, gamma))
to
else
sys.error("type error: arg does not match expected type")
case _ => sys.error("first operand of Ap must be a function")
}
}
case Let(x, xdef, body) => typeCheck(body, gamma + (x -> typeCheck(xdef, gamma)))
case TypeAscription(e, t) =>
if (typeCheck(e, gamma) == t) t else sys.error("type error in ascription")
case Product(e1, e2) => ProductType(typeCheck(e1, gamma), typeCheck(e2, gamma))
case Fst(e) => typeCheck(e, gamma) match {
case ProductType(t1, t2) => t1
case _ => sys.error("can only project Products")
}
case Snd(e) => typeCheck(e, gamma) match {
case ProductType(t1, t2) => t2
case _ => sys.error("can only project Products")
}
case SumLeft(e, t) => SumType(typeCheck(e, gamma), t)
case SumRight(t, e) => SumType(t, typeCheck(e, gamma))
case EliminateSum(e, fl, fr) => typeCheck(e, gamma) match {
case SumType(left, right) => (typeCheck(fl, gamma), typeCheck(fr, gamma)) match {
case (FunType(lf, t1), FunType(rf, t2)) if ((left == lf) && (right == rf)) =>
if (t1 == t2)
t1
else
sys.error("type error: functions must have same return type")
case _ =>
sys.error("type error in EliminateSum: second and third argument must be functions")
}
case _ => sys.error("type error: can only eliminate sums")
}
}
Soundness of Simply Typed Lambda Calculus (STLC):
If
e: ExpandtypeCheck(e, Map.empty) == t, thentypeCheck(eval(e), Map.empty) == t.
Fun("x", NumType(), Product(5, Add(3, "x")))
FunType(NumType(), NumType())
ProductType(NumType(), NumType())
FunType(NumType(),
ProductType(NumType(), NumType()))
NumType()
EliminateSum(SumLeft(3, JunitType()),
Fun("x", NumType(), "x"),
Fun("x", JunitType(), 0))
JunitType()
NumType()
SumType(NumType(), JunitType())
FunType(NumType(), NumType())
Type Inference
The content of this chapter is available as a Scala file here.
Type inference (sometimes called type reconstruction) is the idea to avoid type annotations
in the program and instead infer all typing-related information from the program.
For instance, if + is an operator on numbers, then we can infer that x must have
the number type in an expression x + 1.
The best-known type inference algorithm is Hindley-Milner type inference with so-called "let-polymorphism".
The basic idea of this algorithm is that the type checker synthesizes fresh type variables
whenever a type that is not yet known is needed as an input to a recursive call of the type
checking algorithm. For instance, in a function definition, a fresh type variable is created for the type of
the function argument. In addition to producing a type as output, the type checker will also produce
a set of equality constraints between types (containing type variables). Type checking succeeds only if these
equality constraints have a solution. "Having a solution" means that there is a substitution
(a mapping from type variables to types) that makes all equations trivial. For instance, the substitution that
substitutes X by Num and Y by Bool is a solution for the constraints FunType(X, Bool) == FunType(Num, Y).
In the code below we choose a slightly different representation of substitution, namely as a function that performs the substitution (with regard to our discussion of refunctionalization we could say that we refunctionalize the substitution type).
enum Type:
case FunType(from: Type, to: Type)
case NumType()
case TypeVar(x: String)
import Type._
def freeTypeVars(t: Type): Set[String] = t match {
case FunType(f, t) => freeTypeVars(f) ++ freeTypeVars(t)
case NumType() => Set.empty
case TypeVar(x) => Set(x)
}
def substitution(x: String, s: Type) = new Function[Type, Type] {
def apply(t: Type) = t match {
case FunType(from, to) => FunType(this(from), this(to))
case NumType() => NumType()
case TypeVar(y) => if (x == y) s else TypeVar(y)
}
}
Note that in the FunType-case this is the substitution itself which is simply applied to the input and output type.
A substitution can be found (if it exists) by an algorithm called the "Robinson unification algorithm":
def unify(eq: List[(Type, Type)]): Type => Type = eq match {
case Nil => identity _
case (NumType(), NumType()) :: rest => unify(rest)
case (FunType(f1, t1), FunType(f2, t2)) :: rest => unify((f1, f2) :: (t1, t2) :: rest)
case (TypeVar(x), TypeVar(y)) :: rest if x == y => unify(rest)
case (TypeVar(x), t) :: rest => {
if (freeTypeVars(t)(x)) sys.error(s"Occurs check: $x occurs in $t")
val s = substitution(x, t)
// andThen is just function composition with the first function (here s) applied first
s.andThen(unify(rest.map(p => (s(p._1), s(p._2)))))
}
case (t, TypeVar(x)) :: rest => unify((TypeVar(x), t) :: rest)
case (t1, t2) :: rest => sys.error(s"Cannot unify $t1 and $t2")
}
It is not easy to see that this algorithm terminates in all cases, but it does (ask yourself: why?). It is both sound and complete. It returns the so-called "most general unifier".
Let us now apply this to a concrete language. Here is its definition:
enum Exp:
case Num(n: Int)
case Id(name: String)
case Add(lhs: Exp, rhs: Exp)
case Fun(param: String, body: Exp) // No type annotation!
case Ap(funExpr: Exp, argExpr: Exp)
case Let(x: String, xdef: Exp, body: Exp)
object Exp:
implicit def num2exp(n: Int): Exp = Num(n)
implicit def id2exp(s: String): Exp = Id(s)
import Exp._
def freshName(names: Set[String], default: String): String = {
var last: Int = 0
var freshName = default
while (names contains freshName) { freshName = default + last.toString; last += 1; }
freshName
}
def freeVars(e: Exp): Set[String] = e match {
case Id(x) => Set(x)
case Add(l, r) => freeVars(l) ++ freeVars(r)
case Fun(x, body) => freeVars(body) - x
case Ap(f, a) => freeVars(f) ++ freeVars(a)
case Num(n) => Set.empty
case Let(x, xdef, body) => freeVars(xdef) ++ (freeVars(body) - x)
}
def subst(e1: Exp, x: String, e2: Exp): Exp = e1 match {
case Num(n) => e1
case Add(l, r) => Add(subst(l, x, e2), subst(r, x, e2))
case Id(y) => if (x == y) e2 else Id(y)
case Ap(f, a) => Ap(subst(f, x, e2), subst(a, x, e2))
case Fun(param, body) =>
if (param == x) e1 else {
val fvs = freeVars(body) ++ freeVars(e2)
val newvar = freshName(fvs, param)
Fun(newvar, subst(subst(body, param, Id(newvar)), x, e2))
}
case Let(y, ydef, body) =>
if (x == y) Let(y, subst(ydef, x, e2), body) else {
val fvs = freeVars(body) ++ freeVars(e2)
val newvar = freshName(fvs, y)
Let(newvar, subst(ydef, x, e2), subst(subst(body, y, Id(newvar)), x, e2))
}
}
def eval(e: Exp): Exp = e match {
case Id(v) => sys.error("unbound identifier: " + v)
case Add(l, r) => (eval(l), eval(r)) match {
case (Num(x), Num(y)) => Num(x + y)
case _ => sys.error("can only add numbers")
}
case Ap(f, a) => eval(f) match {
case Fun(x, body) => eval(subst(body, x, eval(a))) // call-by-value
case _ => sys.error("can only apply functions")
}
case Let(x, xdef, body) => eval(subst(body, x, eval(xdef)))
case _ => e // numbers and functions evaluate to themselves
}
The type checker returns both a type (possibly containing type variables) and a list of equality constraints. Note that the only way type checking can actually fail is when encountering a free variable.
var tyvCount: Int = 0
def freshTypeVar: TypeVar = {
tyvCount += 1
TypeVar("X" + tyvCount.toString)
}
def typeCheck(e: Exp, gamma: Map[String, Type]): (List[(Type, Type)], Type) = e match {
case Num(n) => (List.empty, NumType())
case Id(x) => gamma.get(x) match {
case Some(t) => (List.empty, t)
case _ => sys.error("free variable: " ++ x.toString)
}
case Add(l, r) => (typeCheck(l, gamma), typeCheck(r, gamma)) match {
case ((eq1, t1), (eq2, t2)) =>
((t1, NumType()) :: (t2, NumType()) :: (eq1 ++ eq2), NumType())
}
case Fun(x, body) => {
val xtype = freshTypeVar
val resbody = typeCheck(body, gamma + (x -> xtype))
(resbody._1, FunType(xtype, resbody._2))
}
case Ap(f, a) => {
val toType = freshTypeVar
(typeCheck(f, gamma), typeCheck(a, gamma)) match {
case ((eqs1, ft), (eqs2, at)) =>
((ft, FunType(at, toType)) :: (eqs1 ++ eqs2), toType)
}
}
case Let(x, xdef, body) => {
// important if x is not used in body
val (constraints1, _) = typeCheck(xdef, gamma)
// Let-Polymorphism! type check after substitution
val (constraints2, typ) = typeCheck(subst(body, x, xdef), gamma)
(constraints1 ++ constraints2, typ)
}
}
The Let-case of the type checker implements a special extension of the type checking algorithm, which
allows one to use the same definition type-polymorphically at multiple types. This is achieved by first
substituting the binding into the body and only then type check the latter. This way, any occurrence of
the binding in the body can have a different type. Note further, that we still type check the definition
of the binding explicitly, in order to gather the generated constraints also in the case that the binding
is not used in the body.
Full type checking is completed only when the constraints have a solution. The resulting substitution is then applied to the returned type to give the overall inferred type. This is captured by the following definition.
def doTypeCheck(e: Exp, gamma: Map[String, Type]) = {
val (constraints, resType) = typeCheck(e, gamma)
unify(constraints)(resType)
}
assert(doTypeCheck(42, Map.empty) == NumType())
assert(doTypeCheck(Fun("x", Add("x", 1)), Map.empty) == FunType(NumType(), NumType()))
Properties of type inference
As an instance of let-polymorphism, consider the following example where the identity function is once applied to a function and once to a number:
val exId =
doTypeCheck(
Let("id", Fun("x", "x"), Ap(Ap("id", Fun("x", Add("x", 1))), Ap("id", 42))),
Map.empty)
// exId: Type = NumType()
This function could not be type checked in STLC.
This example, on the other hand, should trigger an occurs check error:
val exOmega = doTypeCheck(Fun("x", Ap("x", "x")), Map.empty)
// java.lang.RuntimeException: Occurs check: X9 occurs in FunType(TypeVar(X9),TypeVar(X10))
// at scala.sys.package$.error(package.scala:27)
// at repl.MdocSession$MdocApp.unify(type-inference.md:45)
// at repl.MdocSession$MdocApp.doTypeCheck(type-inference.md:176)
// at repl.MdocSession$MdocApp.$init$$$anonfun$1(type-inference.md:202)
// at repl.MdocSession$MdocApp.$init$$$anonfun$adapted$1(type-inference.md:203)
Hence omega cannot be type checked in STLC (and not even with let-polymorphism).
STLC has the remarkable property that all well-typed programs terminate.
Type inference satisfies the following completeness property:
If there exist type annotations that make a program type check in the STLC type checker, then the type inference will also be able to type check the non-annotated version of the program.
Further, due to let-polymorphism, with type inference we can also type check some programs that would be ill-formed in STLC.
Moreover, the type system is still sound:
If
doTypeCheck(e, Map.empty) == t, theneval(e) == vanddoTypeCheck(v) == t(modulo \( \alpha \)-renaming of type variables).
FunType(NumType(), NumType())
and
FunType(TypeVar("X"), TypeVar("X"))
FunType(TypeVar("X"), TypeVar("Y"))
and
NumType()
NumType().
FunType(NumType(), TypeVar("X"))
and
FunType(NumType(), TypeVar("Y"))
FunType(NumType(), TypeVar("Y"))
and
TypeVar("X")