Lecture 2: Terms and Types

Title slide

Slides : Recording

Today’s lecture introduced the first topic for the course, on types in programming languages: some of the ways they are used, and their relation to the mathematical models of lambda-calculus and type theory. Students identified a range of languages that use types, with some variation across what they are used for and how they are implemented. The lecture introduced the simply-typed lambda-calculus: its terms and types with α-conversion and β-reduction. The next lecture will start with some examples of programming language support for first-class functions.

Link: Slides for Lecture  2; Recording of Lecture 2

Homework

1. Watch This

MIT Technology Review: 35 Innovators under 35

Jean Yang
Assistant Professor of Computer Science
Carnegie Mellon University

Links: Video (2’18”)Prof. Yang at CMU

Jean Yang

2. Do This

  • Find out what the Blub Paradox is.

  • Read the article that named it

3. Read This

Read this paper and do some of the exercises.

You may find it helpful to also read pages 1–7 of Pierce’s Foundational Calculi for Programming Languages which introduces the untyped lambda-calculus.

Other Reading

The first of these is secretly about lambda-calculus terms and their execution. The second is much less colourful but is useful background reading.

Alligator Eggs!
A Puzzle Game
Bret Victor

Links: Alligator Eggs; Animation

Colourful alligators with colourful eggs
First-Class Function
Wikipedia
I think this a fair overview, leading in to issues of anonymous functions, closures, and higher-order functions in programming languages.
Links: Wikipedia page now; Wikipedia page as at 2018-09-20
Screenshot of Wikipedia page
References

A Set of Postulates for the Foundation of Logic
Alonzo Church
Annals of Mathematics Series 2, 33:346–366. Princeton, 1932.

The original lambda-calculus.
Links: Paper at JSTOR (may require payment); Prepaid access through Edinburgh University Library (EASE login)

Picture of first page of Church's paper introducing the lambda calculus

Types and Programming Languages
Benjamin C. Pierce
MIT Press, 2002

A comprehensive introduction to type systems in computer science and programming languages.

Links: Author’s page; Publisher’s page; Edinburgh University Library copies

Book cover

Advanced Topics in Types and Programming Languages
Benjamin C. Pierce, Editor
MIT Press, 2005

Builds on the previous book with chapters presenting several concrete applications of types to programming, each written by experts in the field.

Links: Author’s page; Publisher’s page; Edinburgh University Library copies

Book cover

Leave a Reply

%d bloggers like this: