Programming Language Design 2

Overview

At this point, you’ve built a foundation with multiple programming languages and have learned about the theory behind them. In this part, we’ll dive deeper into the theory of programming languages and programming language design. We’ll primarily use Rust as the programming language for examples and exercises.

We begin by writing parsers using a Rust library called nom. Then, we look into simply typed lambda calculus (STLC) in more detail, and build a programming language called STLC++ based on it. Here are some List functions implemented in STLC++:

sum : List Integer -> Integer
sum = fun xs : List Integer,
        lcase xs of
        | nil => 0
        | cons x xs => x + sum xs

append : List Integer -> List Integer -> List Integer
append = fun xs : List Integer,
        fun ys : List Integer,
            lcase xs of
            | nil => ys
            | cons x xs => cons x (append xs ys)

reverse : List Integer -> List Integer
reverse = fun xs : List Integer,
        lcase xs of
        | nil => nil Integer
        | cons x xs => append (reverse xs) (cons x nil Integer)

The language supports integers, booleans, functions, lists, sum and product types, general recursion¹, and Haskell-style declarations and imports.

This part is organized as follows:

Parsing with Nom. This part starts with learning a useful parsing framework for Rust.
Variables and Substitution Here we start diving deeper into the theory of lambda calculus and define what is substitution.
Reduction and evaluation. With substitution, we are able to define -reduction easily. This chapter discusses how -reduction can be used for evaluation.
Simply Typed Lambda Calculus. Here we introduce lambda calculus as the architecture for creating programming languages. We study the evaluation semantics of lambda calculus, namely -reduction, and then discuss the type checking of terms which have variables in them.
STLC with Integers and Booleans. We extend the calculus with integers and booleans and study their dynamics and statics.
STLC Extensions. We add pairs, lists and sum types to STLC.
STLC Fixed Points and Recursion. We add a fixed point combinator to make the language capable of computing complex algorithms with recursion.
STLC++ Declarations, Modules and Imports. Finally we polish the syntax with declarations and add a simple module system along with imports.
A Taste of Formalization. An optional chapter with formal proofs of type safety of the simply typed lambda calculus using the Lean proof assistant.

General recursion only on term level. Implementing recursive types is a topic outside the scope of this course. ↩

Parsing with Nom →

Overview

Footnotes