michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

merge

Browse source
This commit is contained in:
wadler 2020-05-29 10:17:10 -03:00
commit 07934be2b5
5 changed files with 766 additions and 144 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

298
README.md
View file

@ -4,45 +4,129 @@ title: Getting Started
permalink: /GettingStarted/
---
[![Build Status](https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev)](https://travis-ci.org/plfa/plfa.github.io)
[![Agda](https://img.shields.io/badge/agda-2.6.0.1-blue.svg)](https://github.com/agda/agda/releases/tag/v2.6.0.1)
[![agda-stdlib](https://img.shields.io/badge/agda--stdlib-1.1-blue.svg)](https://github.com/agda/agda-stdlib/releases/tag/v1.1)
<!-- Links -->
[plfa]: http://plfa.inf.ed.ac.uk
[plfa-dev]: https://github.com/plfa/plfa.github.io/archive/dev.zip
[plfa-status]: https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev
[plfa-travis]: https://travis-ci.org/plfa/plfa.github.io
[plfa-master]: https://github.com/plfa/plfa.github.io/archive/master.zip
[agda]: https://github.com/agda/agda/releases/tag/v2.6.0.1
[agda-version]: https://img.shields.io/badge/agda-v2.6.0.1-blue.svg
[agda-docs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html
[agda-docs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html#notation-for-key-combinations
[agda-docs-package-system]: https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#example-using-the-standard-library
[agda-stdlib-version]: https://img.shields.io/badge/agda--stdlib-v1.1-blue.svg
[agda-stdlib]: https://github.com/agda/agda-stdlib/releases/tag/v1.1
[haskell-stack]: https://docs.haskellstack.org/en/stable/README/
[haskell-ghc]: https://www.haskell.org/ghc/
[mononoki]: https://madmalik.github.io/mononoki/
[ruby]: https://www.ruby-lang.org/en/documentation/installation/
[ruby-bundler]: https://bundler.io/#getting-started
[ruby-jekyll]: https://jekyllrb.com/
[ruby-html-proofer]: https://github.com/gjtorikian/html-proofer
[kramdown]: https://kramdown.gettalong.org/syntax.html
<!-- Status & Version Badges -->
[![Build Status][plfa-status]][plfa-travis]
[![Agda][agda-version]][agda]
[![agda-stdlib][agda-stdlib-version]][agda-stdlib]
# Getting Started with PLFA
There are several tools you need to work with PLFA:
## Dependencies for users
- [Agda](https://agda.readthedocs.io/en/v2.6.0.1/getting-started/installation.html)
- [Agda standard library](https://github.com/agda/agda-stdlib/releases/tag/v1.1)
You can read PLFA [online][plfa] without installing anything.
However, if you wish to interact with the code or complete the exercises, you need several things:
For most of the tools, you can simply follow their respective build instructions.
We list the versions of our dependencies on the badges above. We have
tested with the versions listed; either earlier or later versions may
cause problems.
- [Agda][agda]
- [Agda standard library][agda-stdlib]
- [PLFA][plfa-dev]
You can get the appropriate version of Programming Language Foundations in Agda from GitHub,
either by cloning the repository,
or by downloading [the zip archive](https://github.com/plfa/plfa.github.io/archive/dev.zip):
PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems.
git clone https://github.com/plfa/plfa.github.io
### Installing Agda using Stack
Finally, we need to let Agda know where to find the standard library.
For this, you can follow the instructions
[here](https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#example-using-the-standard-library).
The easiest way to install any specific version of Agda is using [Stack][haskell-stack]. You can get the required version of Agda from GitHub, either by cloning the repository and switching to the correct branch, or by downloading [the zip archive][agda]:
```bash
git clone https://github.com/agda/agda.git
cd agda
git checkout v2.6.0.1
```
To install Agda, run Stack from the Agda source directory:
```bash
stack install --stack-yaml stack-8.6.5.yaml
```
If you want Stack to use you system installation of GHC, you can pass the `--system-ghc` flag and select the appropriate `stack-*.yaml` file. For instance, if you have GHC 8.2.2 installed, run:
```bash
stack install --system-ghc --stack-yaml stack-8.2.2.yaml
```
It is possible to set up PLFA as an Agda library as well. If you want
to complete the exercises found in the `courses` folder, or to import
modules from the book, you need to do this. To do so, add the path to
`plfa.agda-lib` to `~/.agda/libraries` and add `plfa` to
`~/.agda/defaults`, both on lines of their own.
### Installing the Standard Library and PLFA
## Auto-loading `agda-mode` in Emacs
You can get the required version of the Agda standard library from GitHub, either by cloning the repository and switching to the correct branch, or by downloading [the zip archive][agda-stdlib]:
```bash
git clone https://github.com/agda/agda-stdlib.git
cd agda-stdlib
git checkout v1.1
```
You can get the latest version of Programming Language Foundations in Agda from GitHub, either by cloning the repository, or by downloading [the zip archive][plfa-dev]:
```bash
git clone https://github.com/plfa/plfa.github.io
```
Finally, we need to let Agda know where to find the standard library. For this, you can follow the instructions [here][agda-docs-package-system].
In order to have `agda-mode` automatically loaded whenever you open a file ending
with `.agda` or `.lagda.md`, put the following on your Emacs configuration file:
It is possible to set up PLFA as an Agda library as well. If you want to complete the exercises found in the `courses` folder, or to import modules from the book, you need to do this. To do so, add the path to `plfa.agda-lib` to `~/.agda/libraries` and add `plfa` to `~/.agda/defaults`, both on lines of their own.
``` elisp
## Setting up and using Emacs
The recommended editor for Agda is Emacs with `agda-mode`. Agda ships with `agda-mode`, so if you’ve installed Agda, all you have to do to configure `agda-mode` is run:
```bash
agda-mode setup
```
To load and type-check the file, use [`C-c C-l`][agda-docs-emacs-notation].
Agda is edited “interactively, which means that one can type check code which is not yet complete: if a question mark (?) is used as a placeholder for an expression, and the buffer is then checked, Agda will replace the question mark with a “hole” which can be filled in later. One can also do various other things in the context of a hole: listing the context, inferring the type of an expression, and even evaluating an open term which mentions variables bound in the surrounding context.”
Agda is edited interactively, using “holes”, which are bits of the program that are not yet filled in. If you use a question mark as an expression, and load the buffer using `C-c C-l`, Agda replaces the question mark with a hole. There are several things you can to while the cursor is in a hole:
C-c C-c x split on variable x
C-c C-space fill in hole
C-c C-r refine with constructor
C-c C-a automatically fill in hole
C-c C-, goal type and context
C-c C-. goal type, context, and inferred type
See [the emacs-mode docs][agda-docs-emacs-mode] for more details.
If you want to see messages beside rather than below your Agda code, you can do the following:
- Open your Agda file, and load it using `C-c C-l`;
- type `C-x 1` to get only your Agda file showing;
- type `C-x 3` to split the window horizontally;
- move your cursor to the right-hand half of your frame;
- type `C-x b` and switch to the buffer called “Agda information”.
Now, error messages from Agda will appear next to your file, rather than squished beneath it.
### Auto-loading `agda-mode` in Emacs
Since version 2.6.0, Agda has support for literate editing with Markdown, using the `.lagda.md` extension. One side-effect of this extension is that most editors default to Markdown editing mode, whereas
In order to have `agda-mode` automatically loaded whenever you open a file ending with `.agda` or `.lagda.md`, put the following on your Emacs configuration file:
```elisp
(setq auto-mode-alist
(append
'(("\\.agda\\'" . agda2-mode)
@ -50,68 +134,12 @@ with `.agda` or `.lagda.md`, put the following on your Emacs configuration file:
auto-mode-alist))
```
The configuration file for Emacs is normally located in `~/.emacs` or `~/.emacs.d/init.el`,
but Aquamacs users might need to move their startup settings to the Preferences.el file in
`~/Library/Preferences/Aquamacs Emacs/Preferences`.
## Unicode characters
If you're having trouble typing the Unicode characters into Emacs, the end of
each chapter should provide a list of the unicode characters introduced in that
chapter.
`agda-mode` and emacs have a number of useful commands.
Two of them are especially useful when you solve exercises.
For a full list of supported characters, use `agda-input-show-translations` with:
M-x agda-input-show-translations
All the supported characters in `agda-mode` are shown.
If you want to know how you input a specific Unicode character in agda file,
move the cursor onto the character and type the following command:
M-x quail-show-key
You'll see the key sequence of the character in mini buffer.
The configuration file for Emacs is normally located in `~/.emacs` or `~/.emacs.d/init.el`, but Aquamacs users might need to move their startup settings to the `Preferences.el` file in `~/Library/Preferences/Aquamacs Emacs/Preferences`.
## Using `agda-mode`
### Using mononoki in Emacs
? hole
{!...!} hole with contents
C-c C-l load buffer
Command to give when in a hole:
C-c C-c x split on variable x
C-c C-space fill in hole
C-c C-r refine with constructor
C-c C-a automatically fill in hole
C-c C-, Goal type and context
C-c C-. Goal type, context, and inferred type
See
[the emacs-mode docs](https://agda.readthedocs.io/en/latest/tools/emacs-mode.html)
for more details.
If you want to see messages beside rather than below your Agda code,
you can do the following:
- Load your Agda file and do `C-c C-l`;
- type `C-x 1` to get only your Agda file showing;
- type `C-x 3` to split the window horizontally;
- move your cursor to the right-hand half of your frame;
- type `C-x b` and switch to the buffer called "Agda information"
Now, error messages from Agda will appear next to your file, rather than
squished beneath it.
## Fonts in Emacs
It is recommended that you install the font [mononoki](https://madmalik.github.io/mononoki/), and add the following to the end of your emacs configuration file at `~/.emacs`:
It is recommended that you install the font [mononoki][mononoki], and add the following to the end of your emacs configuration file at `~/.emacs`:
``` elisp
;; default to mononoki
@ -123,58 +151,68 @@ It is recommended that you install the font [mononoki](https://madmalik.github.i
```
# Building the book
### Unicode characters
To build and host a local copy of the book, there are several tools you need *in addition to those listed above*:
If you're having trouble typing the Unicode characters into Emacs, the end of each chapter should provide a list of the unicode characters introduced in that chapter.
- [Ruby](https://www.ruby-lang.org/en/documentation/installation/)
- [Bundler](https://bundler.io/#getting-started)
`agda-mode` and emacs have a number of useful commands. Two of them are especially useful when you solve exercises.
For most of the tools, you can simply follow their respective build instructions.
Most recent versions of Ruby should work.
You install the Ruby dependencies---[Jekyll](https://jekyllrb.com/), [html-proofer](https://github.com/gjtorikian/html-proofer), *etc.*---using Bundler:
For a full list of supported characters, use `agda-input-show-translations` with:
bundle install
M-x agda-input-show-translations
Once you have installed all of the dependencies, you can build a copy of the book by running:
All the supported characters in `agda-mode` are shown.
make build
If you want to know how you input a specific Unicode character in agda file, move the cursor onto the character and type the following command:
You can host your copy of the book locally by running:
M-x quail-show-key
make serve
You'll see the key sequence of the character in mini buffer.
## Dependencies for developers
Building PLFA is currently supported on Linux and macOS.
PLFA is written in literate Agda with [Kramdown Markdown][kramdown].
The book is built in three stages:
1. The `.lagda.md` files are compiled to Markdown using Agda’s highlighter.
(This requires several POSIX tools, such as `bash`, `sed`, and `grep`.)
2. The Markdown files are converted to HTML using [Jekyll][ruby-jekyll], a widely-used static site builder.
(This requires [Ruby][ruby] and [Jekyll][ruby-jekyll].)
3. The HTML is checked using [html-proofer][ruby-html-proofer].
(This requires [Ruby][ruby] and [html-proofer][ruby-html-proofer].)
Most recent versions of [Ruby][ruby] should work. The easiest way to install [Jekyll][ruby-jekyll] and [html-proofer][ruby-html-proofer] is using [Bundler][ruby-bundler]. You can install [Bundler][ruby-bundler] by running:
```bash
gem install bundler
```
You can install the remainder of the dependencies---[Jekyll][ruby-jekyll], [html-proofer][ruby-html-proofer], *etc.*---by running:
```bash
bundle install
```
Once you have installed all of the dependencies, you can build a copy of the book, and host it locally, by running:
```bash
make build
make serve
```
The Makefile offers more than just these options:
make (see make test)
make build (builds lagda->markdown and the website)
make build-incremental (builds lagda->markdown and the website incrementally)
make test (checks all links are valid)
make test-offline (checks all links are valid offline)
make serve (starts the server)
make server-start (starts the server in detached mode)
make server-stop (stops the server, uses pkill)
make clean (removes all ~unnecessary~ generated files)
make clobber (removes all generated files)
If you simply wish to have a local copy of the book, e.g. for offline reading,
but don't care about editing and rebuilding the book, you can grab a copy of the
[master branch](https://github.com/plfa/plfa.github.io/archive/master.zip),
which is automatically built using Travis. You will still need Ruby and Bundler
to host the book (see above). To host the book this way, download a copy of the
[master branch](https://github.com/plfa/plfa.github.io/archive/master.zip),
unzip, and from within the directory run
bundle install
bundle exec jekyll serve
## Markdown
The book is written in
[Kramdown Markdown](https://kramdown.gettalong.org/syntax.html).
## Travis Continuous Integration
You can view the build history of PLFA at [travis-ci.org](https://travis-ci.org/plfa/plfa.github.io).
```bash
make # see make test
make build # builds lagda->markdown and the website
make build-incremental # builds lagda->markdown and the website incrementally
make test # checks all links are valid
make test-offline # checks all links are valid offline
make serve # starts the server
make server-start # starts the server in detached mode
make server-stop # stops the server, uses pkill
make clean # removes all ~unnecessary~ generated files
make clobber # removes all generated files
```
If you simply wish to have a local copy of the book, e.g. for offline reading, but don't care about editing and rebuilding the book, you can grab a copy of the [master branch][plfa-master], which is automatically built using Travis. You will still need [Jekyll][ruby-jekyll] and preferably [Bundler][ruby-bundler] to host the book (see above). To host the book this way, download a copy of the [master branch][plfa-master], unzip, and from within the directory run
```bash
bundle install
bundle exec jekyll serve
```

576
extra/842Inference.agda Normal file
View file

@ -0,0 +1,576 @@
module 842Inference where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.String using (String; _≟_)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Relation.Nullary using (¬_; Dec; yes; no)
import plfa.part2.DeBruijn as DB
-- Syntax.
infix 4 _∋_⦂_
infix 4 _⊢_↑_
infix 4 _⊢_↓_
infixl 5 _,_⦂_
infixr 7 _⇒_
infix 5 ƛ_⇒_
infix 5 μ_⇒_
infix 6 _↑
infix 6 _↓_
infixl 7 _·_
infix 8 `suc_
infix 9 `_
Id : Set
Id = String
data Type : Set where
`ℕ : Type
_⇒_ : Type → Type → Type
data Context : Set where
∅ : Context
_,_⦂_ : Context → Id → Type → Context
data Term⁺ : Set
data Term⁻ : Set
data Term⁺ where
`_ : Id → Term⁺
_·_ : Term⁺ → Term⁻ → Term⁺
_↓_ : Term⁻ → Type → Term⁺
data Term⁻ where
ƛ_⇒_ : Id → Term⁻ → Term⁻
`zero : Term⁻
`suc_ : Term⁻ → Term⁻
`case_[zero⇒_|suc_⇒_] : Term⁺ → Term⁻ → Id → Term⁻ → Term⁻
μ_⇒_ : Id → Term⁻ → Term⁻
_↑ : Term⁺ → Term⁻
-- Examples of terms.
two : Term⁻
two = `suc (`suc `zero)
plus : Term⁺
plus = (μ "p" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
`case (` "m") [zero⇒ ` "n" ↑
|suc "m" ⇒ `suc (` "p" · (` "m" ↑) · (` "n" ↑) ↑) ])
↓ (`ℕ ⇒ `ℕ ⇒ `ℕ)
2+2 : Term⁺
2+2 = plus · two · two
Ch : Type
Ch = (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ
twoᶜ : Term⁻
twoᶜ = (ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · (` "z" ↑) ↑) ↑)
plusᶜ : Term⁺
plusᶜ = (ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
` "m" · (` "s" ↑) · (` "n" · (` "s" ↑) · (` "z" ↑) ↑) ↑)
↓ (Ch ⇒ Ch ⇒ Ch)
sucᶜ : Term⁻
sucᶜ = ƛ "x" ⇒ `suc (` "x" ↑)
2+2ᶜ : Term⁺
2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
-- Lookup judgments.
data _∋_⦂_ : Context → Id → Type → Set where
Z : ∀ {Γ x A}
--------------------
→ Γ , x ⦂ A ∋ x ⦂ A
S : ∀ {Γ x y A B}
→ x ≢ y
→ Γ ∋ x ⦂ A
-----------------
→ Γ , y ⦂ B ∋ x ⦂ A
-- Synthesis and inheritance.
data _⊢_↑_ : Context → Term⁺ → Type → Set
data _⊢_↓_ : Context → Term⁻ → Type → Set
data _⊢_↑_ where
⊢` : ∀ {Γ A x}
→ Γ ∋ x ⦂ A
-----------
→ Γ ⊢ ` x ↑ A
_·_ : ∀ {Γ L M A B}
→ Γ ⊢ L ↑ A ⇒ B
→ Γ ⊢ M ↓ A
-------------
→ Γ ⊢ L · M ↑ B
⊢↓ : ∀ {Γ M A}
→ Γ ⊢ M ↓ A
---------------
→ Γ ⊢ (M ↓ A) ↑ A
data _⊢_↓_ where
⊢ƛ : ∀ {Γ x N A B}
→ Γ , x ⦂ A ⊢ N ↓ B
-------------------
→ Γ ⊢ ƛ x ⇒ N ↓ A ⇒ B
⊢zero : ∀ {Γ}
--------------
→ Γ ⊢ `zero ↓ `ℕ
⊢suc : ∀ {Γ M}
→ Γ ⊢ M ↓ `ℕ
---------------
→ Γ ⊢ `suc M ↓ `ℕ
⊢case : ∀ {Γ L M x N A}
→ Γ ⊢ L ↑ `ℕ
→ Γ ⊢ M ↓ A
→ Γ , x ⦂ `ℕ ⊢ N ↓ A
-------------------------------------
→ Γ ⊢ `case L [zero⇒ M |suc x ⇒ N ] ↓ A
⊢μ : ∀ {Γ x N A}
→ Γ , x ⦂ A ⊢ N ↓ A
-----------------
→ Γ ⊢ μ x ⇒ N ↓ A
⊢↑ : ∀ {Γ M A B}
→ Γ ⊢ M ↑ A
→ A ≡ B
-------------
→ Γ ⊢ (M ↑) ↓ B
-- PLFA exercise: write the term for multiplication (from Lambda)
-- PLFA exercise: extend the rules to support products (from More)
-- PLFA exercise (stretch): extend the rules to support the other
-- constructs from More
-- Equality of types.
_≟Tp_ : (A B : Type) → Dec (A ≡ B)
`ℕ ≟Tp `ℕ = yes refl
`ℕ ≟Tp (A ⇒ B) = no λ()
(A ⇒ B) ≟Tp `ℕ = no λ()
(A ⇒ B) ≟Tp (A′ ⇒ B′)
with A ≟Tp A′ | B ≟Tp B′
... | no A≢ | _ = no λ{refl → A≢ refl}
... | yes _ | no B≢ = no λ{refl → B≢ refl}
... | yes refl | yes refl = yes refl
-- Helpers: domain and range of equal function types are equal,
-- `ℕ is not a function type.
dom≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → A ≡ A′
dom≡ refl = refl
rng≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → B ≡ B′
rng≡ refl = refl
ℕ≢⇒ : ∀ {A B} → `ℕ ≢ A ⇒ B
ℕ≢⇒ ()
-- Lookup judgments are unique.
uniq-∋ : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B
uniq-∋ Z Z = refl
uniq-∋ Z (S x≢y _) = ⊥-elim (x≢y refl)
uniq-∋ (S x≢y _) Z = ⊥-elim (x≢y refl)
uniq-∋ (S _ ∋x) (S _ ∋x′) = uniq-∋ ∋x ∋x′
-- A synthesized type is unique.
uniq-↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → Γ ⊢ M ↑ B → A ≡ B
uniq-↑ (⊢` ∋x) (⊢` ∋x′) = uniq-∋ ∋x ∋x′
uniq-↑ (⊢L · ⊢M) (⊢L′ · ⊢M′) = rng≡ (uniq-↑ ⊢L ⊢L′)
uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′) = refl
-- Failed lookups still fail if a different binding is added.
ext∋ : ∀ {Γ B x y}
→ x ≢ y
→ ¬ ∃[ A ]( Γ ∋ x ⦂ A )
-----------------------------
→ ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
ext∋ x≢y _ ⟨ A , Z ⟩ = x≢y refl
ext∋ _ ¬∃ ⟨ A , S _ ⊢x ⟩ = ¬∃ ⟨ A , ⊢x ⟩
-- Decision procedure for lookup judgments.
lookup : ∀ (Γ : Context) (x : Id)
-----------------------
→ Dec (∃[ A ](Γ ∋ x ⦂ A))
lookup ∅ x = no (λ ())
lookup (Γ , y ⦂ B) x with x ≟ y
... | yes refl = yes ⟨ B , Z ⟩
... | no x≢y with lookup Γ x
... | no ¬∃ = no (ext∋ x≢y ¬∃)
... | yes ⟨ A , ⊢x ⟩ = yes ⟨ A , S x≢y ⊢x ⟩
-- Helpers for promoting a failure to type.
¬arg : ∀ {Γ A B L M}
→ Γ ⊢ L ↑ A ⇒ B
→ ¬ Γ ⊢ M ↓ A
-------------------------
→ ¬ ∃[ B′ ](Γ ⊢ L · M ↑ B′)
¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
¬switch : ∀ {Γ M A B}
→ Γ ⊢ M ↑ A
→ A ≢ B
---------------
→ ¬ Γ ⊢ (M ↑) ↓ B
¬switch ⊢M A≢B (⊢↑ ⊢M′ A′≡B) rewrite uniq-↑ ⊢M ⊢M′ = A≢B A′≡B
-- Mutually-recursive synthesize and inherit functions.
synthesize : ∀ (Γ : Context) (M : Term⁺)
-----------------------
→ Dec (∃[ A ](Γ ⊢ M ↑ A))
inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
---------------
→ Dec (Γ ⊢ M ↓ A)
synthesize Γ (` x) with lookup Γ x
... | no ¬∃ = no (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ })
... | yes ⟨ A , ∋x ⟩ = yes ⟨ A , ⊢` ∋x ⟩
synthesize Γ (L · M) with synthesize Γ L
... | no ¬∃ = no (λ{ ⟨ _ , ⊢L · _ ⟩ → ¬∃ ⟨ _ , ⊢L ⟩ })
... | yes ⟨ `ℕ , ⊢L ⟩ = no (λ{ ⟨ _ , ⊢L′ · _ ⟩ → ℕ≢⇒ (uniq-↑ ⊢L ⊢L′) })
... | yes ⟨ A ⇒ B , ⊢L ⟩ with inherit Γ M A
... | no ¬⊢M = no (¬arg ⊢L ¬⊢M)
... | yes ⊢M = yes ⟨ B , ⊢L · ⊢M ⟩
synthesize Γ (M ↓ A) with inherit Γ M A
... | no ¬⊢M = no (λ{ ⟨ _ , ⊢↓ ⊢M ⟩ → ¬⊢M ⊢M })
... | yes ⊢M = yes ⟨ A , ⊢↓ ⊢M ⟩
inherit Γ (ƛ x ⇒ N) `ℕ = no (λ())
inherit Γ (ƛ x ⇒ N) (A ⇒ B) with inherit (Γ , x ⦂ A) N B
... | no ¬⊢N = no (λ{ (⊢ƛ ⊢N) → ¬⊢N ⊢N })
... | yes ⊢N = yes (⊢ƛ ⊢N)
inherit Γ `zero `ℕ = yes ⊢zero
inherit Γ `zero (A ⇒ B) = no (λ())
inherit Γ (`suc M) `ℕ with inherit Γ M `ℕ
... | no ¬⊢M = no (λ{ (⊢suc ⊢M) → ¬⊢M ⊢M })
... | yes ⊢M = yes (⊢suc ⊢M)
inherit Γ (`suc M) (A ⇒ B) = no (λ())
inherit Γ (`case L [zero⇒ M |suc x ⇒ N ]) A with synthesize Γ L
... | no ¬∃ = no (λ{ (⊢case ⊢L _ _) → ¬∃ ⟨ `ℕ , ⊢L ⟩})
... | yes ⟨ _ ⇒ _ , ⊢L ⟩ = no (λ{ (⊢case ⊢L′ _ _) → ℕ≢⇒ (uniq-↑ ⊢L′ ⊢L) })
... | yes ⟨ `ℕ , ⊢L ⟩ with inherit Γ M A
... | no ¬⊢M = no (λ{ (⊢case _ ⊢M _) → ¬⊢M ⊢M })
... | yes ⊢M with inherit (Γ , x ⦂ `ℕ) N A
... | no ¬⊢N = no (λ{ (⊢case _ _ ⊢N) → ¬⊢N ⊢N })
... | yes ⊢N = yes (⊢case ⊢L ⊢M ⊢N)
inherit Γ (μ x ⇒ N) A with inherit (Γ , x ⦂ A) N A
... | no ¬⊢N = no (λ{ (⊢μ ⊢N) → ¬⊢N ⊢N })
... | yes ⊢N = yes (⊢μ ⊢N)
inherit Γ (M ↑) B with synthesize Γ M
... | no ¬∃ = no (λ{ (⊢↑ ⊢M _) → ¬∃ ⟨ _ , ⊢M ⟩ })
... | yes ⟨ A , ⊢M ⟩ with A ≟Tp B
... | no A≢B = no (¬switch ⊢M A≢B)
... | yes A≡B = yes (⊢↑ ⊢M A≡B)
-- Copied from Lambda.
_≠_ : ∀ (x y : Id) → x ≢ y
x ≠ y with x ≟ y
... | no x≢y = x≢y
... | yes _ = ⊥-elim impossible
where postulate impossible : ⊥
-- Computed by evaluating 'synthesize ∅ 2+2' and editing.
⊢2+2 : ∅ ⊢ 2+2 ↑ `ℕ
⊢2+2 =
(⊢↓
(⊢μ
(⊢ƛ
(⊢ƛ
(⊢case (⊢` (S (λ()) Z)) (⊢↑ (⊢` Z) refl)
(⊢suc
(⊢↑
(⊢`
(S (λ())
(S (λ())
(S (λ()) Z)))
· ⊢↑ (⊢` Z) refl
· ⊢↑ (⊢` (S (λ()) Z)) refl)
refl))))))
· ⊢suc (⊢suc ⊢zero)
· ⊢suc (⊢suc ⊢zero))
-- Check that synthesis is correct (more below).
_ : synthesize ∅ 2+2 ≡ yes ⟨ `ℕ , ⊢2+2 ⟩
_ = refl
-- Example: 2+2 for Church numerals.
⊢2+2ᶜ : ∅ ⊢ 2+2ᶜ ↑ `ℕ
⊢2+2ᶜ =
⊢↓
(⊢ƛ
(⊢ƛ
(⊢ƛ
(⊢ƛ
(⊢↑
(⊢`
(S (λ())
(S (λ())
(S (λ()) Z)))
· ⊢↑ (⊢` (S (λ()) Z)) refl
·
⊢↑
(⊢`
(S (λ())
(S (λ()) Z))
· ⊢↑ (⊢` (S (λ()) Z)) refl
· ⊢↑ (⊢` Z) refl)
refl)
refl)))))
·
⊢ƛ
(⊢ƛ
(⊢↑
(⊢` (S (λ()) Z) ·
⊢↑ (⊢` (S (λ()) Z) · ⊢↑ (⊢` Z) refl)
refl)
refl))
·
⊢ƛ
(⊢ƛ
(⊢↑
(⊢` (S (λ()) Z) ·
⊢↑ (⊢` (S (λ()) Z) · ⊢↑ (⊢` Z) refl)
refl)
refl))
· ⊢ƛ (⊢suc (⊢↑ (⊢` Z) refl))
· ⊢zero
_ : synthesize ∅ 2+2ᶜ ≡ yes ⟨ `ℕ , ⊢2+2ᶜ ⟩
_ = refl
-- Testing error cases.
_ : synthesize ∅ ((ƛ "x" ⇒ ` "y" ↑) ↓ (`ℕ ⇒ `ℕ)) ≡ no _
_ = refl
-- Bad argument type.
_ : synthesize ∅ (plus · sucᶜ) ≡ no _
_ = refl
-- Bad function types.
_ : synthesize ∅ (plus · sucᶜ · two) ≡ no _
_ = refl
_ : synthesize ∅ ((two ↓ `ℕ) · two) ≡ no _
_ = refl
_ : synthesize ∅ (twoᶜ ↓ `ℕ) ≡ no _
_ = refl
-- A natural can't have a function type.
_ : synthesize ∅ (`zero ↓ `ℕ ⇒ `ℕ) ≡ no _
_ = refl
_ : synthesize ∅ (two ↓ `ℕ ⇒ `ℕ) ≡ no _
_ = refl
-- Can't hide a bad type.
_ : synthesize ∅ (`suc twoᶜ ↓ `ℕ) ≡ no _
_ = refl
-- Can't case on a function type.
_ : synthesize ∅
((`case (twoᶜ ↓ Ch) [zero⇒ `zero |suc "x" ⇒ ` "x" ↑ ] ↓ `ℕ) ) ≡ no _
_ = refl
-- Can't hide a bad type inside case.
_ : synthesize ∅
((`case (twoᶜ ↓ `ℕ) [zero⇒ `zero |suc "x" ⇒ ` "x" ↑ ] ↓ `ℕ) ) ≡ no _
_ = refl
-- Mismatch of inherited and synthesized types.
_ : synthesize ∅ (((ƛ "x" ⇒ ` "x" ↑) ↓ `ℕ ⇒ (`ℕ ⇒ `ℕ))) ≡ no _
_ = refl
-- Erasure: Taking the evidence provided by synthesis on a decorated term
-- and producing the corresponding inherently-typed term.
-- Erasing a type.
∥_∥Tp : Type → DB.Type
∥ `ℕ ∥Tp = DB.`ℕ
∥ A ⇒ B ∥Tp = ∥ A ∥Tp DB.⇒ ∥ B ∥Tp
-- Erasing a context.
∥_∥Cx : Context → DB.Context
∥ ∅ ∥Cx = DB.∅
∥ Γ , x ⦂ A ∥Cx = ∥ Γ ∥Cx DB., ∥ A ∥Tp
-- Erasing a lookup judgment.
∥_∥∋ : ∀ {Γ x A} → Γ ∋ x ⦂ A → ∥ Γ ∥Cx DB.∋ ∥ A ∥Tp
∥ Z ∥∋ = DB.Z
∥ S x≢ ⊢x ∥∋ = DB.S ∥ ⊢x ∥∋
-- Mutually-recursive functions to erase typing judgments.
∥_∥⁺ : ∀ {Γ M A} → Γ ⊢ M ↑ A → ∥ Γ ∥Cx DB.⊢ ∥ A ∥Tp
∥_∥⁻ : ∀ {Γ M A} → Γ ⊢ M ↓ A → ∥ Γ ∥Cx DB.⊢ ∥ A ∥Tp
∥ ⊢` ⊢x ∥⁺ = DB.` ∥ ⊢x ∥∋
∥ ⊢L · ⊢M ∥⁺ = ∥ ⊢L ∥⁺ DB.· ∥ ⊢M ∥⁻
∥ ⊢↓ ⊢M ∥⁺ = ∥ ⊢M ∥⁻
∥ ⊢ƛ ⊢N ∥⁻ = DB.ƛ ∥ ⊢N ∥⁻
∥ ⊢zero ∥⁻ = DB.`zero
∥ ⊢suc ⊢M ∥⁻ = DB.`suc ∥ ⊢M ∥⁻
∥ ⊢case ⊢L ⊢M ⊢N ∥⁻ = DB.case ∥ ⊢L ∥⁺ ∥ ⊢M ∥⁻ ∥ ⊢N ∥⁻
∥ ⊢μ ⊢M ∥⁻ = DB.μ ∥ ⊢M ∥⁻
∥ ⊢↑ ⊢M refl ∥⁻ = ∥ ⊢M ∥⁺
-- Tests that erasure works.
_ : ∥ ⊢2+2 ∥⁺ ≡ DB.2+2
_ = refl
_ : ∥ ⊢2+2ᶜ ∥⁺ ≡ DB.2+2ᶜ
_ = refl
-- PLFA exercise: demonstrate that synthesis on your decorated multiplication
-- followed by erasure gives your inherently-typed multiplication.
-- PLFA exercise: extend the above to include products.
-- PLFA exercise (stretch): extend the above to include
-- the rest of the features added in More.
-- Additions by PR:
-- From Lambda, with type annotation added
data Term : Set where
`_ : Id → Term
ƛ_⇒_ : Id → Term → Term
_·_ : Term → Term → Term
`zero : Term
`suc_ : Term → Term
`case_[zero⇒_|suc_⇒_] : Term → Term → Id → Term → Term
μ_⇒_ : Id → Term → Term
_⦂_ : Term → Type → Term
-- Mutually-recursive decorators.
decorate⁻ : Term → Term⁻
decorate⁺ : Term → Term⁺
decorate⁻ (` x) = ` x ↑
decorate⁻ (ƛ x ⇒ M) = ƛ x ⇒ decorate⁻ M
decorate⁻ (M · M₁) = (decorate⁺ M) · (decorate⁻ M₁) ↑
decorate⁻ `zero = `zero
decorate⁻ (`suc M) = `suc (decorate⁻ M)
decorate⁻ `case M [zero⇒ M₁ |suc x ⇒ M₂ ]
= `case (decorate⁺ M) [zero⇒ (decorate⁻ M₁) |suc x ⇒ (decorate⁻ M₂) ]
decorate⁻ (μ x ⇒ M) = μ x ⇒ decorate⁻ M
decorate⁻ (M ⦂ x) = decorate⁻ M
decorate⁺ (` x) = ` x
decorate⁺ (ƛ x ⇒ M) = ⊥-elim impossible
where postulate impossible : ⊥
decorate⁺ (M · M₁) = (decorate⁺ M) · (decorate⁻ M₁)
decorate⁺ `zero = ⊥-elim impossible
where postulate impossible : ⊥
decorate⁺ (`suc M) = ⊥-elim impossible
where postulate impossible : ⊥
decorate⁺ `case M [zero⇒ M₁ |suc x ⇒ M₂ ] = ⊥-elim impossible
where postulate impossible : ⊥
decorate⁺ (μ x ⇒ M) = ⊥-elim impossible
where postulate impossible : ⊥
decorate⁺ (M ⦂ x) = decorate⁻ M ↓ x
ltwo : Term
ltwo = `suc `suc `zero
lplus : Term
lplus = (μ "p" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
`case ` "m"
[zero⇒ ` "n"
|suc "m" ⇒ `suc (` "p" · ` "m" · ` "n") ])
⦂ (`ℕ ⇒ `ℕ ⇒ `ℕ)
l2+2 : Term
l2+2 = lplus · ltwo · ltwo
ltwoᶜ : Term
ltwoᶜ = ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")
lplusᶜ : Term
lplusᶜ = (ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
` "m" · ` "s" · (` "n" · ` "s" · ` "z"))
⦂ (Ch ⇒ Ch ⇒ Ch)
lsucᶜ : Term
lsucᶜ = ƛ "x" ⇒ `suc (` "x")
l2+2ᶜ : Term
l2+2ᶜ = lplusᶜ · ltwoᶜ · ltwoᶜ · lsucᶜ · `zero
_ : decorate⁻ ltwo ≡ two
_ = refl
_ : decorate⁺ lplus ≡ plus
_ = refl
_ : decorate⁺ l2+2 ≡ 2+2
_ = refl
_ : decorate⁻ ltwoᶜ ≡ twoᶜ
_ = refl
_ : decorate⁺ lplusᶜ ≡ plusᶜ
_ = refl
_ : decorate⁻ lsucᶜ ≡ sucᶜ
_ = refl
_ : decorate⁺ l2+2ᶜ ≡ 2+2ᶜ
_ = refl
{-
Unicode used in this chapter:
↓ U+2193: DOWNWARDS ARROW (\d)
↑ U+2191: UPWARDS ARROW (\u)
∥ U+2225: PARALLEL TO (\||)
-}

13
highlight.sh
View file

@ -23,9 +23,18 @@ function html_path {
HTML_DIR="$2"
# Extract the module name from the Agda file
# NOTE: this fails if there is more than a single space after 'module'
#
# NOTE: This fails when there is no module statement,
# or when there is more than one space after 'module'.
#
MOD_NAME=`grep -o -m 1 "module\\s*\\(\\S\\S*\\)\\s.*where$" "$SRC" | cut -d ' ' -f 2`
if [ -z "$MOD_NAME" ]
then
echo "Error: No module header detected in '$SRC'" 1>&2
exit 1
fi
# Extract the extension from the Agda file
SRC_EXT="$(basename $SRC)"
SRC_EXT="${SRC_EXT##*.}"
@ -44,7 +53,7 @@ set -o pipefail \
# Check if the highlighted file was successfully generated
if [[ ! -f "$HTML" ]]; then
echo "File not generated: $FILE"
echo "Error: File not generated: '$FILE'" 1>&2
exit 1
fi

20
src/plfa/part2/Substitution.lagda.md
View file

@ -346,15 +346,15 @@ cong-ext{Γ}{Δ}{ρ}{ρ′}{B} rr {A} = extensionality λ x → lemma {x}
```
```
cong-rename : ∀{Γ Δ}{ρ ρ′ : Rename Γ Δ}{B}{M M′ : Γ ⊢ B}
→ (∀{A} → ρ ≡ ρ′ {A}) → M ≡ M′
------------------------------
cong-rename : ∀{Γ Δ}{ρ ρ′ : Rename Γ Δ}{B}{M : Γ ⊢ B}
→ (∀{A} → ρ ≡ ρ′ {A})
------------------------
→ rename ρ M ≡ rename ρ′ M
cong-rename {M = ` x} rr refl = cong `_ (cong-app rr x)
cong-rename {ρ = ρ} {ρ′ = ρ′} {M = ƛ N} rr refl =
cong ƛ_ (cong-rename {ρ = ext ρ}{ρ′ = ext ρ′}{M = N} (cong-ext rr) refl)
cong-rename {M = L · M} rr refl =
cong₂ _·_ (cong-rename rr refl) (cong-rename rr refl)
cong-rename {M = ` x} rr = cong `_ (cong-app rr x)
cong-rename {ρ = ρ} {ρ′ = ρ′} {M = ƛ N} rr =
cong ƛ_ (cong-rename {ρ = ext ρ}{ρ′ = ext ρ′}{M = N} (cong-ext rr))
cong-rename {M = L · M} rr =
cong₂ _·_ (cong-rename rr) (cong-rename rr)
```
```
@ -670,7 +670,7 @@ compose-rename {Γ}{Δ}{Σ}{A}{ƛ N}{ρ}{ρ′} = cong ƛ_ G
rename (ext ρ) (rename (ext ρ′) N)
≡⟨ compose-rename{ρ = ext ρ}{ρ′ = ext ρ′} ⟩
rename ((ext ρ) ∘ (ext ρ′)) N
≡⟨ cong-rename compose-ext refl ⟩
≡⟨ cong-rename compose-ext ⟩
rename (ext (ρ ∘ ρ′)) N
∎
compose-rename {M = L · M} = cong₂ _·_ compose-rename compose-rename
@ -705,7 +705,7 @@ commute-subst-rename{Γ}{Δ}{ƛ N}{σ}{ρ} r =
rename S_ (rename ρ (σ y))
≡⟨ compose-rename ⟩
rename (S_ ∘ ρ) (σ y)
≡⟨ cong-rename refl refl ⟩
≡⟨ cong-rename refl ⟩
rename ((ext ρ) ∘ S_) (σ y)
≡⟨ sym compose-rename ⟩
rename (ext ρ) (rename S_ (σ y))

3
src/plfa/part3/Compositional.lagda.md
View file

@ -213,8 +213,7 @@ describe the proof below.
... | inj₂ ⟨ v₁′ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ | inj₂ ⟨ v₁′′ , ⟨ L↓v12′ , M↓v3′ ⟩ ⟩ =
let L↓⊔ = ⊔-intro L↓v12 L↓v12′ in
let M↓⊔ = ⊔-intro M↓v3 M↓v3′ in
let x = inj₂ ⟨ v₁′ ⊔ v₁′′ , ⟨ sub L↓⊔ ⊔↦⊔-dist , M↓⊔ ⟩ ⟩ in
x
inj₂ ⟨ v₁′ ⊔ v₁′′ , ⟨ sub L↓⊔ ⊔↦⊔-dist , M↓⊔ ⟩ ⟩
ℰ·→●ℰ {Γ}{γ}{L}{M}{v} (sub d lt)
with ℰ·→●ℰ d
... | inj₁ lt2 = inj₁ (⊑-trans lt lt2)