Announcements
Migration to Agda 2.7.0
We upgraded to Agda 2.7.0 and version 2.1 of the standard library. If you want to continue working with the book, you’ll have to update your versions locally. Please follow the instructions in Getting Started to reinstall Agda and the standard library.
In the past, we maintained compatibility with versions of Agda all the way back to Agda 2.6.1.3 and version 1.6 of the standard library. However, version 2.0 of the standard library broke backwards compatibility with earlier versions of the standard library. Consequently, starting with today’s version of PLFA, the oldest supported versions of Agda and its standard library are Agda 2.6.4.3 and version 2.0 of the standard library.
Migration to Agda 2.6.3
We upgraded to Agda 2.6.3 and version 1.7.2 of the standard library. If you want to continue working with the book, you’ll have to update your versions locally. Please follow the instructions in Getting Started to reinstall Agda and the standard library.
Release Notes v22.08
We are pleased to announce the release of v22.08 of Programming Language Foundations in Agda.
The release will be permanently available at:
Changes:
- We have migrated to Agda v2.6.2.2 with standard library v1.7.1.
- Our contributors have contributed numerous fixes to the text.
- Support for dark mode was added by Wen Kokke. To activate click the moon in the header or add
?dark=trueto the URL.
We are grateful to the many individuals who have made contributions, which have improved the book significantly.
PLFA as PDF and EPUB
We’re pleased to announce that PLFA is now available as both a PDF and an EPUB! Thanks to hard work by Yuanting Mao, who did an internship with Phil at the University of Edinburgh, and a little elbow grease on our part, we’re finally compiling to PDF!
In a double whammy, we’ve recently fixed compilation to EPUB as well! Compilation to EPUB never quite survived the move to Hakyll, and the EPUB available on the website was broken for quite a while. Fortunately, we’ve fixed the EPUB compilation, based on Yuanting Mao work on PDF compilation and Michael Reed’s original work on EPUB compilation.
There’s still several kinks to even out in the process:
- (#577) EPUB generation breaks internal links;
- (#578) EPUB fragment identifier is not defined;
- (#579) EPUB font cannot be found;
- (#580) EPUB attribute “name” not allowed;
- (#581) PDF code overflows margins;
And probably tons of other little bugs I’ve missed!
As always, bug reports and pull requests are very, very welcome!
Migration to Agda 2.6.1
We upgraded to Agda 2.6.1 and version 1.3 of the standard library. If you want to continue working with the latest version of the book, you’ll have to update your versions locally. Please follow the instructions in Getting Started to reinstall Agda and the standard library.
Changes to the termination checker
Agda 2.6.1 made several changes to the termination checker. As a result of these changes, Agda is no longer able to see that our evaluation functions, e.g., in Properties, are terminating. In response, we changed the definition of Gas to be a record type, rather than a data type:
- data Gas : Set where
- gas : ℕ → Gas
+ record Gas : Set where
+ constructor gas
+ field
+ amount : ℕThe reason this works is that η-equality holds by definition for records. Agda uses this to see that unwrapping and rewrapping numbers as Gas is the identity, and hence the amount of gas is decreasing if that number is decreasing.
Changes to equational reasoning
The function ≡⟨⟩_, part of the equational reasoning syntax, was renamed to step-≡, for various reasons. The new function has the same semantics, but flips the order of the arguments. This does not mean you have to change your equational reasoning proofs, as the module also defines a syntax macro, which recovers the original argument order:
infixr -2 step-≡
step-≡ : ∀ x {y z : A} → y ≡ z → x ≡ y → x ≡ z
step-≡ y≡z x≡y = trans x≡y y≡z
syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡zSyntax macros aren’t quite definitions in Agda, so you cannot import them by “name”. Instead, they’re imported together with the function for which they’re defined, i.e., as step-≡:
- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)If you’d like more details, there’s a lot of discussion of why this change was made in the CHANGELOG. For PLFA, we make a note of the incongruence in the chapter on Equality, but leave our definitions of equational reasoning unchanged.
Deprecation of Data.List.{All,Any}
The modules Data.List.{All,Any} were deprecated in v1.0, and were moved to Data.List.Relation.Unary.{All,Any}:
- import Data.List.All using (All; []; _∷_)
- import Data.List.Any using (Any; here; there)
+ import Data.List.Relation.Unary.All using (All; []; _∷_)
+ import Data.List.Relation.Unary.Any using (Any; here; there)Versions and Releases
We’re adding stable releases to PLFA, which you can find on GitHub!
For the past two years, we’ve tried to do major revisions of the book during winter break and early summer, to ensure that the text remains consistent throughout the teaching period… Inevitably, we fixed bugs, and make small changes here and there, perhaps resulting in a less-than-consistent experience.
Starting today, you can be sure that PLFA will remain consistent, since we’re adding stable releases! You can find the releases on GitHub, and as tags in the Git repository. The releases are numbered using calendar versioning using the v0Y.0M format, e.g., v20.07 was released in July 2020. Each release will be available indefinitely. For instance, if you’d like to browse PLFA version v20.07, just go to: https://plfa.github.io/20.07/
Release Notes v20.07
We are pleased to announce the release of v20.07 of Programming Language Foundations in Agda.
The release will be permanently available at:
Introducing Part 3: Denotational Semantics
We’re pleased to announce an entirely new part of the book, contributed by Jeremy G. Siek! You may have noticed his name appearing on the list of authors some months ago, or the chapters that make up Part 3 slowly making their appearance. Well, that’s all Jeremy’s work!
Part 3 introduces denotational semantics, presenting the denotational semantics of the untyped lambda calculus. Our development is unusual in that emphasizes the use of intersection type systems as denotational models instead of the more traditional domain theory, but this choice allows us to build upon the simple type systems studied in Part 2. Part 3 also proves the basic properties of the denotational semantics using techniques and variations of the techniques introduced in Part 2. We prove the soundness of reduction with respect to the denotational semantics by showing that reduction preserves and reflects denotations. We prove adequacy of the denotational semantics using a logical-relations style proof with respect to a big-step semantics of the untyped calculus. Finally, with these results in hand, we prove a standardisation theorem, that reduction to weak-head normal form implies the termination of call-by-name evaluation.
To better prepare the reader for Part 3, we made some changes and updates to Part 2. We’ve changed the reduction semantics for the untyped lambda calculus to be the standard one, with unconstrained beta reduction. We also added two new chapters to Part 2. The first proves confluence—a.k.a. the Church-Rosser property—for the untyped lambda calculus. The second presents big-step semantics for call-by-name evaluation, and proves that call-by-name termination implies the reduction to weak-head normal form.
Finally, we also include an Appendix with a single chapter, which proves the substitution lemma for the untyped lambda calculus. We opted to place this chapter an Appendix, and not in Part 2, because we already discuss substitution for the simply-typed lambda calculus, and we feel it would not be particularly enlightening for students to work through the proofs, especially since the ratio of insight to lines of code is rather low.
Talking about PLFA…
We published a paper about PLFA at the Brazilian Symposium on Formal Methods and in the Science of Computer Programming (extended version). In them, we describe our experiences writing the book, and compare it to Software Foundations.
PLFA as EPUB
It has been just over a year and a half since this feature was first requested in #112… Thanks to hard work by Michael Reed, and a little elbow grease on our part, it is finally here! An EPUB version of PLFA!
Praise for PLFA
Types and Semantics for Programming Languages, the course we teach in Edinburgh, was shortlisted as an Outstanding Course by the Edinburgh University Student Association (Runner Up)!
“Types and Semantics for Programming Languages was the single best course I took throughout my time at the University of Edinburgh. Philip Wadler clearly poured his heart into teaching it, including writing a whole textbook including exercises specifically for the course.”
“One of the most inspiring courses. Philip designed a course that is both very theoretical and very practical.”
PLFA as a Notebook
NextJournal has created a notebook version of PLFA, which lets you edit and run the code samples from the book online! The notebook is based on PLFA version 19.08, with some minor changes to adapt the contents to NextJournal.
Release Notes v19.08
We are pleased to announce the release of v19.08 of Programming Language Foundations in Agda.
The release will be permanently available at:
Migration to Agda 2.6.0.1
We upgraded to Agda 2.6.0.1 and version 1.1 of the standard library. If you want to continue working with the book, you’ll have to update your versions locally. Please follow the instructions in Getting Started to reinstall Agda and the standard library.
For this upgrade, we made several major changes to the PLFA infrastructure.
We deprecated agda2html. In version 2.6, Agda has added support for the –html-highlight flag. Using this command, Agda will highlight only the code in a file, and leave the rest untouched:
agda --html --html-highlight=code FILE.lagda.mdOf course, agda2html offered support for more than just inline highlighting of code in Markdown files. We have written a bash script, highlight.sh (deprecated) which supports much of the same functionality. In particular, it uses sed to redirect links to the standard library to the online version. For the time being, we dropped support for module references, e.g., linking to the chapter on Naturals by writing [Naturals][plfa.Naturals], and removed all module references from the text.
Lastly, to use Agda 2.6 with Markdown, we updated all literal Agda files. We replaced LaTeX code fences, i.e., \begin{code} and \end{code}, with Markdown backtick fences ```, and changed the file extensions .lagda to .lagda.md. As a consequence, when you open up a literate Agda file in Emacs, it will open the file in Markdown mode – if you have it installed – or in fundamental mode. To switch to Agda mode, you will have to invoke M-x agda2-mode.