1 For Prospective Students
In this course, we will will work through the online textbook Programming Language Foundations in Agda (PLFA) by Philip Wadler, Wen Kokke and Jeremy Siek, available in full online. The goal of this book, and our goal, is to study topics in functional programming, logic, semantics, and type theory using the Agda programming language. This was also the goal of my three offerings of CS 798 (Software Foundations), which I last taught in Fall 2018, using the Coq programming language. The reasons I switched to Agda are largely articulated in the preface to PLFA and my own notes on it.
Nonetheless, the preface of the CS 798 textbook, Software Foundations (SF), gives an excellent overview of the topics covered and the reasons to study them; if you are reading this sentence, you should click through and read that preface as well. In addition to what is written in the two book prefaces, I can add that working in Agda (or Coq) is an interesting change from conventional (even functional) programming, and will appeal to those who like solving puzzles or playing games.
I taught this material in person once as CS 842 before submitting a proposal to make it permanent as CS 747. CS 747 was designed as our first general online graduate course, before COVID-19 put all of them online. But unlike other graduate courses, it will remain online when the crisis passes. The point is to permit more flexibility in offerings. CS 747 was first offered in Summer 2021, and the current offering only two terms later helps alleviate a shortage of graduate courses in Winter 2022.
Lectures: In designing a video-based online graduate course, I discovered that there is a great deal of overhead involved in creating or modifying materials, so that the kind of small, incremental changes needed to keep a course fine-tuned tend not to happen. My previous live in-person offerings of this material involved a fair amount of livecoding during lecture, with some student interaction (suggestions as to how to proceed). The bandwidth taken up by a video of a typical screen-capture session (without, of course, any interaction) seems excessive, considering the informational content of the end result. The solution I found was to use "asciicasts", which record terminal emulator commands (character insertion/deletion, cursor movements). The resulting files are quite small and can be played back in the browser.
I have embedded asciicasts of my own livecoding in the notes (linked above and on the Handouts page). The notes run in parallel with the text in PLFA (which is static, with fully developed code). There are no synchronous remote elements to this course, and no asynchronous videos, except for the embedded asciicasts. Synchronous livecoding is still possible via screensharing in office hours, which is the only place you’ll see my face and hear my voice. You can drop in and lurk in public office hours, even if you don’t have an immediate question. Private office hours are when I’m guaranteed to be available for quick one-on-one videochat or audio sessions; these can also be scheduled at mutually convenient times.
The code: The HTML version of PLFA is generated from a set of source files that are written in literate Agda, which intersperses code and commentary. Those source files are available online as well (there is a link at the top of each PLFA chapter). PLFA is hosted on GitHub, so you can download or fork it. There are both stable and development versions.
I have prepared starter files by stripping out the commentary and most of the completed code, leaving just type definitions and holes to be filled. I find these reduced versions easier to work with, and I hope you will also. I have also made several code changes of my own (which I explain in the notes) resulting in what might be considered a "local remix". Those starter files will be available on the Handouts page. The asciicasts (which are relatively short) consist of my working through interactive development from the starter file.
I have also made available "completed" versions with all my interactions completed. These still have unfinished parts, which are the exercises that you will do for credit. It’s straightforward to load a completed file, comment out part of the development, and recreate it interactively, in case you want to try alternatives or experiment before attempting the exercises.
Scope of the course: PLFA was originally divided into two parts, Logical Foundations and Programming Language Foundations, mirroring the two original volumes of SF. Since I taught CS 842, a third part has been added, written mostly by the also-added third author (Jeremy Siek). There are now several more volumes of SF, as well, but the first two parts/volumes of each work remain the core.
Typically in CS 798, I was able to complete the first volume of SF, but had to rush through a third to a half of the second volume. With Agda, there is less first-volume overhead, and in CS 842, we were able to complete the chapters of the second part of PLFA that I wished to cover. The schedule of CS 747 assignment due dates is based on timings from that offering.
Other interactions: We will use Piazza for out-of-class questions and general discussions, and MS Teams for office hours. If you’re enrolled in the class on the first day, you will receive a Piazza invitation; otherwise please contact me and I will add you. Private email to me for questions is also fine, but please send from your UW account if possible, so that I have your userid and can look at any submitted code, in case that helps.
Please avoid screenshots of code. I typically find I need to quote snippets in my reply, or load the code into Agda to work with it. Screenshots of error messages are fine. On Piazza, please try to use code blocks that preserve indentation. With email, it is best to attach your complete Agda file. If you have a question about a version you have submitted to Marmoset, I can see and download the code from there.
Workload: To do the work associated with a particular chapter of PLFA, you should read the chapter in parallel with my notes on it, and watch the embedded asciicasts. You might also load the starter file into Emacs and try out some of the interactions yourself. I will leave it up to you as to whether you do exercises as you encounter them in the readings, or whether you finish the readings before starting any of the exercises.
The assignment questions are all embedded in the starter and completed files. You should use the completed files as the basis for your solutions. Some exercises are marked "PLFA exercise"; these appear in PLFA but will not be assigned in this course. You can choose whether or not to work on them. Others are marked "747/PLFA exercise" or just "747 exercise", and these are the ones that you will be assigned. Most of these exercises appear in PLFA. Some are new and some have been changed.
The exercises involve writing Agda code interactively. The code is for the most part short, especially compared to most other programming, but it may take you some time to get it right. The advantage of using Agda is that you will know immediately whether the code is correct or not (with a few exceptions, in cases where the type signature does not capture all the requirements of a solution). I have personally completed all exercises I will ask you to do, without the benefit of solutions (none will be posted), and I will have some additional comments and hints to offer. These assignments will be the only basis for your final grade. There are no exams, presentations, or projects.
Relative to other graduate courses at this level, I would characterize the workload as moderate.
Because there are no synchronous components, the schedule is largely a suggestion to keep you moving through the material. Your work should be self-directed and self-paced. You can work ahead (I will answer questions on any part of the course at any point). We are living through difficult times, and if you need extra time to complete assignments, please let me know so that I can make adjustments to my marking schedule.
Necessary background: I will expect only some familiarity with some form of programming (such as might be obtained from a first course), exposure to university-level mathematics (including the brief look at discrete mathematics and logic that is found in the typical undergraduate CS curriculum), and the ability to install and work with new software (on which the Logistics page has more details). Exposure to functional programming will help, but if you have none, just be prepared to think about programs differently.