We describe what this course is about, including how the course is structured, a rough outline of the topics, and high-level remarks about the study of programming languages. We also introduce OCaml, including how to work with utop, how to compile simple programs, and how to write basic expressions.
Reading:
We look at the basic constructs we need to start writing more interesting OCaml programs, and work through some examples. We start to see how the typing rules and semantics of OCaml work. We also introduce dune (which we'll be using for assignments).
Reading:
We explore further the notion of expressions in OCaml (everything is an expression in OCaml). In particular, we look at let expressions as a way of using local variables. We continue to emphasize that as we introduce more programming abstractions, we have to formally present their syntax, typing, and semantics.
We look at various ways of organizing data in OCaml including simple variants, data-carrying variants, tuples, records. We also introduced the notion of a pattern (which is is not the same thing as an expression, though it behaves similarly with respect to typing).
Reading:
We introduce the familiar notion of lists in OCaml, emphasizing that lists are immutable in OCaml. We also talk about tail recursion, how to write tail recursive functions, and why we might want to.
Reading:
We introduce algebraic data types as a way of defining recursive and parameterized data types. We look at many examples. (Note. ADTs are fundamental to functional programming, this is where we really start to see OCaml shine)
Reading:
Many of the programs that we've written so far used specific types like int, string, and bool. We take a moment to discuss polymorphism more formally, and how to use polymorphism to write more general programs.
We introduce the notion of higher-order functions, i.e., functions which take other functions as arguments. There are three common higher-order functions used in programming, we cover the first two: map and filter for lists.
Reading:
We cover the last (and most complex) of the common higher-order functions: fold_left and fold_right for lists. We also look at how higher-order functions can be useful for things other than lists.
Reading:
We introduce modules as a way of organizing OCaml code. We see at how modules can also be used to organize interfaces for data structures.
We also introduce monads as a way to more elegantly deal with options in functional code. We show how to use let* syntax in OCaml to make code easier to follow.
Reading:
We take our last lecture before the midterm to discuss the notions of progress and preservation. These theorems express that well-typed programs are well-behaved, and hold for any good programming languages. Professor Das also takes a moment to lament about programming languages.
We introduce the second half of the course, including the full interpretation pipeline. We then start at the beginning of the pipeline (i.e., parsing) looking at (E)BNF grammars, ambiguity, and precedence.
Reading:
We look more carefully at the difference between lexing and parsing. We then see how to use ocamllex and menhir to generate lexers and parsers for a grammar (in particular, how to deal with ambiguity and precedence). (Note. We will use these tools for every interpreter we build, so it is important to become comfortable with them)
Reading:
We introduce operational semantics (both small-step and big-step) as a way of formally specifying the behavior of executing a programming language. We give some examples of derivations for various semantics.
Reading:
We look the lambda calculus, its syntax and semantics. We also discuss capture-avoiding substitution as a way of dealing with some of the more subtle details of evaluating expressions in the lambda calculus.
Reading:
We discuss (dynamic and lexical) scoping, with an emphasis on how variable scoping is dealt with in OCaml. We consider how this connects to call-by-value semantics and closures.
Reading:
We further discuss closures as a way to better implement lexical scoping in functional programming languages. We introduce the environment model as a more efficient alternative to the substitution model from the previous week.
Reading:
We look even more carefully at the notion of a typing derivation.
We look at the practical considerations of type checking.
Reading:
We discuss type inference and let-polymorphism (potentially non-polymorphic lets).
We discuss more generally the notion of unification, which underlies the type inference algorithm we will be implementing.
We look at practical considerations in the implementation of a type inference algorithm.
Reading:
We discuss stack-oriented languages in general and introduce the syntax and semantics of a basic stack-oriented language with procedures.
We give a high-level introduction of compilation and its relation to interpretation and work through some simple examples. We then go through an example of building a simple byte-code interpreter.
In our last lecture, we cover an advanced topic based on the 300-400 level PL courses being offered in the spring.