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 this for assignments).
Reading:
We explore further the notion of expressions in OCaml (everything is an expression in OCaml). In particuluar, 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:
We take a moment to discuss more formally the notion of polymorphism.
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 will need to know how modules work for the mini-projects in the second-half of the course. We see at how modules can also be used to organize interfaces for data structures. We also look a bit at the relationship between dune and toplevel.
Reading:
We 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.
We take our last lecture before the midterm to discuss the notions of progress and preservation.
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.
We look more carefully at the difference between lexing and parsing. We then see how to use menhir to generate lexers and parsers for a grammar (in particular, how to deal with ambiguity and precedence). (Note. We will use menhir for every interpreter we build, so it is important to become comfortable with this tool)
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 work again through the untyped lambda calculus, this time with the formal machinery from last lecture. We look at capture-avoiding substitution and (if we have time) DeBruijn indices as ways of dealing with some of the more subtle details of evaluating expressions in the lambda calculus.
Reading:
We discuss (dynamic and lexical) scoping, but with an emphasis on how variable scoping is dealt with in OCaml. We also consider the general problem of passing parameters to functions when they they are called, and look specifically at the call-by-name and call-by-value evaluation strategies in the functional setting.
Reading:
We introduce closures as a way to correctly 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.