CPSC521 Foundations of Functional Programming

CPSC521: FOUNDATIONS OF FUNCTIONAL PROGRAMMING

(Winter 2024, SA123, TuTh 3:30pm-4:45pm)

Lecturer: Robin Cockett

The purpose of the course is to explore various aspects of functional programming using Haskell. In particular, the course provides an introduction to the lambda calculus, abstract machines, types in programming, type inference, and the role of these in the implementation of functional programming.

Why functional programming matters ....

It promotes the view of programming as a mathematical activity.
It promotes programming abstractions (generic code).
It is typed .... Hindley-Milner type inference.
It allows fast accurate prototyping for complex programs.
It has datatypes, classes, monads, and many other goodies.
It helps you, the programmer, develop a clear view of programming!

COURSE OUTLINE:

There will be a midterm exam and a final exam. The course will cover the following topics in roughly this order:

Revision of/Introduction to data, maps, and folds in Haskell (3 lectures + assignment)
Monads, classes, and other topics (3 lectures + assignment)
Introduction to the lambda calculus (5 lectures)
Introduction to abstract machines and/or rewriting (2 lectures + assignment)
Type checking and type inference (5 lectures + assignment)
Strong normalization in the typed lambda calculus (2 lectures)

READING (recommended):

Benjamin Pierce "Types and Programming Languages" MIT Press.
Graham Hutton "Programming in Haskell" Cambridge University Press
Miran Lipovaca "Learn you a Haskell for the greater good" here.
Roger Hindley and Jonathan Seldin "Lambda-Calculus and combinators an introduction".

LECTURE NOTES (as they become available):

Introduction: functional programming, Haskell, and HUGS (includes the use of the state monad for substitution).
Introduction to proofs in general.
On the history of computability here.
A programming approach to the lambda calculus:

Paulson's notes, and some notes of mine - still in development - here
Notes on reduction strategies here.
A lambda calculus reducer by Sean Nichols here

Notes on rewriting.
The typed lambda calculus with fixed points. Unification in Haskell here.
Course handout (a bunch of useful papers).

ASSIGNMENTS:

[Due January 26] Getting going with Haskell (8%) assignment 1 (template file is here with types)
[Due March 1] Lambda lifting (14%) assignment 2 (hint: here is some example code for \alpha renaming lambda expressions).
[Due March 22] Abstract machines: lambda calculus reduction (8%) assignment 3.
[Due April 9] Type inference for the lambda calculus here (15%).

EXAMS:

Midterm exam (20%) -- on the 12th March: previous exams -- please note a different order of topics may have been covered -- 2020, 2016, 2014,2010, 2009, 2007, 2006 and exercise sheet, 2005 and answers, 2002.
Final exam (35%), (previous finals 2002, 2006, 2007, and 2008 oral, 2014, 2016).

GRADESCOPE AND ZOOM:

The course will use gradescope for grading assignments and exams. Students need to sign up at gradescope.ca (press the "sign up" button). To find the course entry code, go to the course in D2L and pull down the "content" tab. The zoom links for the on-line portions of the course will be here.

LAB. NOTES:

Please find the lab. notes here (Melika Norouzbegi).

HASKELL LINKS:

The Haskell home page has many useful subsidiary links (in particular to the various HUGS systems which you can download) .... well worth a visit.
The definitive text on the lambda calculus (the theory underlying functional programming) is written by Henk Barendregt: there is now a revised edition of the book.
Here is the main Journal on Functional programming.
Here is a guide to functional programming on the Web compiled by Philip Wadler who is a cool guy and has many interesting links on his home page. Check out functional programming in the real world. An example of an expository paper is "History of logic and programming languages", this is of special interest (to me!) as it points to the close link between proof theory and programming languages.
The main conference in the area is "The International Conference on Functional Programming (ICFP)" . Of particular interest is the functional programming contest (here for example is the 2001 contest ) which is held each year.
Paul Hudak's homepage.

MONAD LINKS

Functors, applicatives, and monads in pictures here.
Stefan Klinger's "Don't Panic" guide to IO Monads
On the monad laws.
Dr. Seuss on Parser Monads: well some good fun for those who have kids (and who are still kids)!
Monadic parsing: Graham Hutton and Erik Meijer

LAMBDA CALCULUS AND FUNCTIONAL PROGRAMMING LINKS:

Peter Selinger's notes on the lambda calculus.
Larry Paulson's notes on a programming approach to the lambda calculus.
Here are Barendregt's notes on functional programming and the lambda calculus.
Here are my notes on the lambda calculus.

COMPUTABILITY LINKS:

For a proof that the halting problem is undecidable see here.