diff --git a/README.md b/README.md index 5c449464..47089b1a 100644 --- a/README.md +++ b/README.md @@ -22,14 +22,22 @@ Please send us comments! Contact details below. In directory `sf/` run the following: - $ make clobber - $ make - $ make serve & + `$ make macos-setup` (might need sudo, but try it without first) + `$ make build` (builds lagda->markdown and website) + `$ make build-incremental` (builds lagda->markdown and website using incremental) + `$ make server-start` (starts server in detached mode) + `$ make server-stop` (stops the server, uses pkill) The visible page appears at localhost:4000/sf/ + + ## Unicode abbreviations diff --git a/index.md b/index.md index 7d46da7e..321eddc7 100644 --- a/index.md +++ b/index.md @@ -3,23 +3,21 @@ title : Table of Contents layout : page --- -This is a rewrite of the text [Software Foundations]( -https://softwarefoundations.cis.upenn.edu/current/index.html -) +This is a rewrite of the text [Software Foundations][sf] from Coq to Agda. The authors are -[Wen Kokke]( -https://github.com/wenkokke +[Wen Kokke][wen] + ) and -[Philip Wadler]( -http://homepages.inf.ed.ac.uk/wadler/ +[Philip Wadler][phil] + +( + ). -## Part 1: Logical Foundations + - [Preface](Preface) - +## Part 1: Logical Foundations - [Naturals: Natural numbers](Naturals) - [Properties: Proof by induction](Properties) @@ -41,3 +39,13 @@ http://homepages.inf.ed.ac.uk/wadler/ - [Stlc: The Simply Typed Lambda-Calculus](Stlc) - [StlcProp: Properties of STLC](StlcProp) - [Scoped: Scoped and Typed DeBruijn representation](Scoped) + +[sf]: https://softwarefoundations.cis.upenn.edu/ +[wen]: https://github.com/wenkokke +[phil]: http://homepages.inf.ed.ac.uk/wadler/ + + + + diff --git a/src/Preface.lagda b/src/Preface.lagda new file mode 100644 index 00000000..32ac02f5 --- /dev/null +++ b/src/Preface.lagda @@ -0,0 +1,69 @@ +--- +title : "Preface" +layout : page +permalink : /Preface +--- + +This book is an introduction to programming language theory, written +in Agda. + +Since 2013, I teach a course on Types and Semantics for Programming +Languages to fourth-year undergraduates and masters students at the +University of Edinburgh. That course had been based on the textbook +[Software Foundations][sf], by Pierce and others, written in Coq. I +am convinced of Pierce's claim that basing a course around a proof +assistant aids learning, as summarised in his ICFP Keynote, [Lambda, +The Ultimate TA][ta]. + +However, after five years of experience, I have come to the conclusion +that Coq may not be the best vehicle. Too much of the course needs to +focus on learning tactics for proof derivation, to the cost of +learning the fundamentals of programming language theory. Every +concept has to be learned twice: both the product data type, and the +corresponding tactics for introduction (`split`) and elimination +(`destruct`) of products. The rules Coq applies to generate induction +hypotheses can sometimes seem mysterious. While the `notation` +construct permits pleasingly flexible syntax, it can be confusing that +the same concept must always be given two names, e.g., both `subst N x +M` and `N [x := M]`. Names of tactics are sometimes short and +sometimes long; naming conventions in the standard library can be +wildly inconsistent. *Propositions as types* as a foundation of proof +is present but hidden. + +I found myself keen to recast the course in Agda. In Agda, there is +no longer any need to learn about tactics: there is just +dependently-typed programming, plain and simple. Introduction is +always by a constructor, elimination is always by pattern +matching. Induction is no longer a mysterious separate concept, but +corresponds to familiar recursion. Multifix syntax is flexible while +using just one name for each concept, e.g., substitution is +`_[_:=_]`. The standard library is not perfect, but there is a fair +attempt at consistency. *Propositions as types* as a foundation of +proof is on proud display. + +Alas, there is no standard text for programming language theory in +Agda. Stump's [Verified Functional Programming in Agda][stump] covers +related ground, but focusses more on programming with dependent +types than on teaching the theory of programming languages. + +The original goal was to simply adapt *Software Foundations*, +maintaining the same text but transposing the code from Coq to Agda. +But it quickly became clear to me that after five years in the +classroom I had my own ideas about how to present the material. They +say you should never write a book unless you cannot not write the +book, and I soon found that this was a book I could not not write. + +I am fortunate that my student, [Wen Kokke][wen], was keen to help. +They guided me as a newbie to Agda and provided an infrastructure that +is easy to use and produces pages that are a pleasure to view. Most +of the text was written during a sabbatical in the first half of 2018. + +Please send suggestions to improve the text to [me][phil]. + +-- Philip Wadler, Rio de Janeiro, January--June 2018 + +[sf]: https://softwarefoundations.cis.upenn.edu/ +[ta]: http://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf +[stump]: http://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?cPath=24&products_id=908 +[wen]: https://github.com/wenkokke +[phil]: http://homepages.inf.ed.ac.uk/wadler/