Conclusion

That’s the end! In this course, we learned about

Functions, as embodied in the λ-calculus. This single concept is powerful enough to express any computation a Turing machine can, so learning how to define the operational semantics of functions is a fast-track to learning how to define the operational semantics of a full programming language.

Types: We learned how to define type systems, which enable us to prove some static guarantees about a program’s behavior (type safety or “well-typed programs don’t get stuck”). But our first attempt was also unduly restrictive; we looked at several ways of increasing expressivity, in both the mathematical sense (is it Turing complete?) and practical sense (would you want to program in this?).

Effects: Whether untyped or typed, we actually can’t express everything we want to, if we use the stricter notion of macro-expressibility: we can’t express effects like state and control. We can define these by translation into continuation-passing style, or macro-express them in terms of a “universal” effect like shift/reset.

What’s next? If you are interested in reading more about…

• λ-calculus: Lambda Calculus and Combinators: An Introduction, 2nd ed., Hindley and Seldin

• Denotational semantics: Formal Semantics of Programming Languages, Winskel

• Types: The rest of TAPL

• Effects: I’m not aware of a textbook or tutorial introduction; a nice recent paper is “On the expressive power of user-defined effects”, Forster et al.

• Compilers: Compiling with Continuations, Appel