added directory wrong place

src/plfa/DeBruijn.lagda

@@ -102,8 +102,8 @@ The other important feature of our chosen representation is
 that it is _inherently typed_.  In the previous two chapters,
 the definition of terms and the definition of types are
 completely separate.  All terms have type `Term`, and nothing
-in Agda prevents one from writing a nonsense term such as ``
-`zero · `suc `zero `` which has no type.  Such terms that
+in Agda prevents one from writing a nonsense term such as
+`` `zero · `suc `zero `` which has no type.  Such terms that
 exist independent of types are sometimes called _preterms_ or
 _raw terms_.  Here we are going to replace the type `Term` of
 raw terms by the more sophisticated type `Γ ⊢ A` of inherently
@@ -158,8 +158,8 @@ Note the two lookup judgments `∋m` and `∋m′` refer to two
 different bindings of variables named `"m"`.  In contrast, the
 two judgments `∋n` and `∋n′` both refer to the same binding
 of `"n"` but accessed in different contexts, the first where
-"n" is the last binding in the context, and the second after
-"m" is bound in the successor branch of the case.
+`"n"` is the last binding in the context, and the second after
+`"m"` is bound in the successor branch of the case.
 
 Here is the term and its type derivation in the notation of this chapter:
 
@@ -450,14 +450,10 @@ two = `suc `suc `zero
 
 plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
 plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
-
-2+2 : ∅ ⊢ `ℕ
-2+2 = plus · two · two
 \end{code}
 We specify that `two` and `plus` can be typed in an arbitrary environment,
 rather than just the empty environment, because later we will give examples
-where they appear nested inside binders.  We need not do the same with `2+2`,
-which will only appear at the top-level of a term.
+where they appear nested inside binders.
 
 Next, computing two plus two on Church numerals:
 \begin{code}
@@ -472,11 +468,8 @@ plusᶜ = ƛ ƛ ƛ ƛ (# 3 · # 1 · (# 2 · # 1 · # 0))
 
 sucᶜ : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ
 sucᶜ = ƛ `suc (# 0)
-
-2+2ᶜ : ∅ ⊢ `ℕ
-2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
 \end{code}
-As before we generalise everything save `2+2ᶜ` to arbitrary
+As before we generalise everything to arbitrary
 contexts.  While we are at it, we also generalise `twoᶜ` and
 `plusᶜ` to Church numerals over arbitrary types.
 

src/plfa/Lambda.lagda

@@ -59,6 +59,7 @@ open import Data.Nat using (ℕ; zero; suc)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Relation.Nullary using (Dec; yes; no; ¬_)
 open import Relation.Nullary.Negation using (¬?)
+open import Data.List using (List; _∷_; [])
 \end{code}
 
 ## Syntax of terms
@@ -136,9 +137,6 @@ plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
          case ` "m"
            [zero⇒ ` "n"
            |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]
-
-2+2 : Term
-2+2 = plus · two · two
 \end{code}
 The recursive definition of addition is similar to our original
 definition of `_+_` for naturals, as given in
@@ -171,9 +169,6 @@ plusᶜ =  ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
 
 sucᶜ : Term
 sucᶜ = ƛ "n" ⇒ `suc (` "n")
-
-fourᶜ : Term
-fourᶜ = plusᶜ · twoᶜ · twoᶜ
 \end{code}
 The Church numeral for two takes two arguments `s` and `z`
 and applies `s` twice to `z`.
@@ -258,8 +253,8 @@ for a term that is a variable. Agda requires we distinguish.
 
 Similarly, informal presentation often use the same notation for
 function types, lambda abstraction, and function application in both
-the object language (the language one is describing) and the
-meta-language (the language in which the description is written),
+the _object language_ (the language one is describing) and the
+_meta-language_ (the language in which the description is written),
 trusting readers can use context to distinguish the two.  Agda is
 not quite so forgiving, so here we use `ƛ x ⇒ N` and `L · M` for the
 object language, as compared to `λ x → N` and `L M` in our
@@ -401,17 +396,18 @@ in the body of the function abstraction.
 
 We write substitution as `N [ x := V ]`, meaning
 "substitute term `V` for free occurrences of variable `x` in term `N`",
-or, more compactly, "substitute `V` for `x` in `N`".
+or, more compactly, "substitute `V` for `x` in `N`",
+or equivalently, "in `N` replace `x` by `V`".
 Substitution works if `V` is any closed term;
 it need not be a value, but we use `V` since in fact we
 usually substitute values.
 
 Here are some examples:
 
-* `` (sucᶜ · (sucᶜ · ` "z")) [ "z" := `zero ] `` yields
-  `` sucᶜ · (sucᶜ · `zero) ``
 * `` (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ] `` yields
   `` ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z") ``
+* `` (sucᶜ · (sucᶜ · ` "z")) [ "z" := `zero ] `` yields
+  `` sucᶜ · (sucᶜ · `zero) ``
 * `` (ƛ "x" ⇒ ` "y") [ "y" := `zero ] `` yields `` ƛ "x" ⇒ `zero ``
 * `` (ƛ "x" ⇒ ` "x") [ "x" := `zero ] `` yields `` ƛ "x" ⇒ ` "x" ``
 * `` (ƛ "y" ⇒ ` "y") [ "x" := `zero ] `` yields `` ƛ "y" ⇒ ` "y" ``
@@ -431,7 +427,7 @@ substitution by terms that are _not_ closed may require renaming
 of bound variables. For example:
 
 * `` (ƛ "x" ⇒ ` "x" · ` "y") [ "y" := ` "x" · `zero] `` should not yield <br/>
-  `` (ƛ "x" ⇒ ` "x" · (` "x" · ` `zero)) ``
+  `` (ƛ "x" ⇒ ` "x" · (` "x" · `zero)) ``
 
 Instead, we should rename the bound variable to avoid capture:
 
@@ -489,10 +485,10 @@ simply push substitution recursively into the subterms.
 Here is confirmation that the examples above are correct:
 
 \begin{code}
-_ : (sucᶜ · (sucᶜ · ` "z")) [ "z" := `zero ] ≡  sucᶜ · (sucᶜ · `zero)
+_ : (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ] ≡  ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")
 _ = refl
 
-_ : (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ] ≡  ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")
+_ : (sucᶜ · (sucᶜ · ` "z")) [ "z" := `zero ] ≡  sucᶜ · (sucᶜ · `zero)
 _ = refl
 
 _ : (ƛ "x" ⇒ ` "y") [ "y" := `zero ] ≡ ƛ "x" ⇒ `zero
@@ -521,7 +517,7 @@ What is the result of the following substitution?
 #### Exercise `_[_:=_]′` (stretch)
 
 The definition of substitution above has three clauses (`ƛ`, `case`,
-and `μ`) that invoke a with clause to deal with bound variables.
+and `μ`) that invoke a `with` clause to deal with bound variables.
 Rewrite the definition to factor the common part of these three
 clauses into a single function, defined by mutual recursion with
 substitution.
@@ -564,6 +560,12 @@ consist of a constructor and a deconstructor, in our case `ƛ` and `·`,
 which reduces directly.  We give them names starting with the Greek
 letter `β` (_beta_) and such rules are traditionally called _beta rules_.
 
+A bit of terminology: A term that matches the left-hand side of a
+reduction rule is called a _redex_. In the redex `(ƛ x ⇒ N) · V`, we
+may refer to `x` as the _formal parameter_` of the function, and `V`
+as the _actual parameter_ of the function application.  Beta reduction
+replaces the formal parameter by the actual parameter.
+
 If a term is a value, then no reduction applies; conversely,
 if a reduction applies to a term then it is not a value.
 We will show in the next chapter that for well-typed terms
@@ -857,7 +859,7 @@ _ =
 
 And here is a similar sample reduction for Church numerals:
 \begin{code}
-_ : fourᶜ · sucᶜ · `zero —↠ `suc `suc `suc `suc `zero
+_ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero —↠ `suc `suc `suc `suc `zero
 _ =
   begin
     (ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ ` "m" · ` "s" · (` "n" · ` "s" · ` "z"))
@@ -993,6 +995,22 @@ data Context : Set where
   _,_⦂_ : Context → Id → Type → Context
 \end{code}
 
+
+#### Exercise `Context-≃`
+
+Show that `Context` is isomorphic to `List (Id × Type)`.
+For instance, the isomorphism relates the context
+
+    `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ``
+
+to the list
+
+    `` [ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ] ``.
+
+\begin{code}
+-- Your code goes here
+\end{code}
+
 ### Lookup judgment
 
 We have two forms of _judgment_.  The first is written
@@ -1181,7 +1199,7 @@ where `∋s` and `∋z` abbreviate the two derivations,
     ----------------------------- S       ------------- Z
     Γ₂ ∋ "s" ⦂ A ⇒ A                       Γ₂ ∋ "z" ⦂ A
 
-and where `Γ₁ = Γ , s ⦂ A ⇒ A` and `Γ₂ = Γ , s ⦂ A ⇒ A , z ⦂ A`.
+and where `Γ₁ = Γ , "s" ⦂ A ⇒ A` and `Γ₂ = Γ , "s" ⦂ A ⇒ A , "z" ⦂ A`.
 The typing derivation is valid for any `Γ` and `A`, for instance,
 we might take `Γ` to be `∅` and `A` to be `` `ℕ ``.
 

src/plfa/Properties.lagda

@@ -10,12 +10,6 @@ next      : /DeBruijn/
 module plfa.Properties where
 \end{code}
 
-[PLW:
-  Perhaps break this into three chapters:
-  The denotational semantics.
-  The proof that the semantics is compositional.
-  The proof that reduction preserves and reflects the semantics.]
-
 This chapter covers properties of the simply-typed lambda calculus, as
 introduced in the previous chapter.  The most important of these
 properties are progress and preservation.  We introduce these below,
@@ -1275,7 +1269,7 @@ _ = refl
 And again, the example in the previous section was derived by editing the
 above.
 
-#### Exercise `mul-example` (recommended)
+#### Exercise `mul-eval` (recommended)
 
 Using the evaluator, confirm that two times two is four.
 

src/plfa/Untyped.lagda

@@ -728,18 +728,15 @@ four = `suc `suc `suc `suc `zero
 
 plus : ∀ {Γ} → Γ ⊢ ★
 plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
-
-2+2 : ∅ ⊢ ★
-2+2 = plus · two · two
 \end{code}
 Because `` `suc `` is now a defined term rather than primitive,
-it is no longer the case that `2+2` reduces to `four`, but they
-do both reduce to the same normal term. 
+it is no longer the case that `plus · two · two` reduces to `four`,
+but they do both reduce to the same normal term. 
 
-#### Exercise `2+2≡four`
+#### Exercise `plus-eval`
 
-Use the evaluator to confirm that `2+2` and `four` normalise to
-the same term.
+Use the evaluator to confirm that `plus · two · two` and `four`
+normalise to the same term.
 
 \begin{code}
 -- Your code goes here

tspl/Assignment3.lagda

@@ -342,7 +342,7 @@ defined by mutual recursion with the proof that substitution
 preserves types.
 
 
-#### Exercise `mul-example` (recommended)
+#### Exercise `mul-eval` (recommended)
 
 Using the evaluator, confirm that two times two is four.
 

tspl/Assignment4.lagda

@@ -76,7 +76,7 @@ not reduce, and its corollary, terms that reduce are not
 values.
 
 
-#### Exercise `mul-example` (recommended)
+#### Exercise `mul-eval` (recommended)
 
 Using the evaluator, confirm that two times two is four.
 
@@ -839,9 +839,6 @@ Remember to indent all code by two spaces.
             `case (` "m") [zero⇒ ` "n" ↑
                           |suc "m" ⇒ `suc (` "p" · (` "m" ↑) · (` "n" ↑) ↑) ])
               ↓ `ℕ ⇒ `ℕ ⇒ `ℕ
-
-  2+2 : Term⁺
-  2+2 = plus · two · two
 \end{code}
 
 ### Lookup 
@@ -1148,12 +1145,12 @@ unless both terms are in normal form.
 How would the rules change if we want call-by-value where terms
 do not reduce underneath lambda?  Assume that `β`
 permits reduction when both terms are values (that is, lambda
-abstractions).  What would `2+2ᶜ` reduce to in this case?
+abstractions).  What would `plusᶜ · twoᶜ · twoᶜ` reduce to in this case?
 
-#### Exercise `2+2≡four`
+#### Exercise `plus-eval`
 
-Use the evaluator to confirm that `2+2` and `four` normalise to
-the same term.
+Use the evaluator to confirm that `plus · two · two` and `four`
+normalise to the same term.
 
 #### Exercise `multiplication-untyped` (recommended)
 

tspl/PUC-Assignment5.lagda

@@ -0,0 +1,455 @@
+---
+title     : "PUC-Assignment5: PUC Assignment 5"
+layout    : page
+permalink : /PUC-Assignment5/
+---
+
+\begin{code}
+module PUC-Assignment5 where
+\end{code}
+
+## YOUR NAME AND EMAIL GOES HERE
+
+
+## Introduction
+
+You must do _all_ the exercises labelled "(recommended)".
+
+Exercises labelled "(stretch)" are there to provide an extra challenge.
+You don't need to do all of these, but should attempt at least a few.
+
+Exercises without a label are optional, and may be done if you want
+some extra practice.
+
+Please ensure your files execute correctly under Agda!
+
+**IMPORTANT** For ease of marking, when modifying the given code please write
+
+    -- begin
+    -- end
+
+before and after code you add, to indicate your changes.
+
+
+## Imports
+
+\begin{code}
+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.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
+open import Data.String using (String)
+open import Data.String.Unsafe using (_≟_)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+\end{code}
+
+
+## Inference
+
+\begin{code}
+module Inference where
+\end{code}
+
+Remember to indent all code by two spaces.
+
+### Imports
+
+\begin{code}
+  import plfa.More as DB
+\end{code}
+
+### Syntax
+
+\begin{code}
+  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  `_
+\end{code}
+
+### Identifiers, types, and contexts
+
+\begin{code}
+  Id : Set
+  Id = String
+
+  data Type : Set where
+    `ℕ    : Type
+    _⇒_   : Type → Type → Type
+
+  data Context : Set where
+    ∅     : Context
+    _,_⦂_ : Context → Id → Type → Context
+\end{code}
+
+### Terms
+
+\begin{code}
+  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⁻
+\end{code}
+
+### Sample terms
+
+\begin{code}
+  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
+\end{code}
+
+### Lookup 
+
+\begin{code}
+  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
+\end{code}
+
+### Bidirectional type checking
+
+\begin{code}
+  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
+\end{code}
+
+
+### Type equality
+
+\begin{code}
+  _≟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
+\end{code}
+
+### Prerequisites
+
+\begin{code}
+  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
+  ℕ≢⇒ ()
+\end{code}
+
+
+### Unique lookup
+
+\begin{code}
+  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′
+\end{code}
+
+### Unique synthesis
+
+\begin{code}
+  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 
+\end{code}
+
+## Lookup type of a variable in the context
+
+\begin{code}
+  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 ⟩
+
+  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 ⟩
+\end{code}
+
+### Promoting negations
+
+\begin{code}
+  ¬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
+\end{code}
+
+
+## Synthesize and inherit types
+
+\begin{code}
+  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)
+\end{code}
+
+### Erasure
+
+\begin{code}
+  ∥_∥Tp : Type → DB.Type
+  ∥ `ℕ ∥Tp             =  DB.`ℕ
+  ∥ A ⇒ B ∥Tp          =  ∥ A ∥Tp DB.⇒ ∥ B ∥Tp
+
+  ∥_∥Cx : Context → DB.Context
+  ∥ ∅ ∥Cx              =  DB.∅
+  ∥ Γ , x ⦂ A ∥Cx      =  ∥ Γ ∥Cx DB., ∥ A ∥Tp
+
+  ∥_∥∋ : ∀ {Γ x A} → Γ ∋ x ⦂ A → ∥ Γ ∥Cx DB.∋ ∥ A ∥Tp
+  ∥ Z ∥∋               =  DB.Z
+  ∥ S x≢ ⊢x ∥∋         =  DB.S ∥ ⊢x ∥∋
+
+  ∥_∥⁺ : ∀ {Γ 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 ∥⁺
+\end{code}
+
+
+#### Exercise `bidirectional-mul` (recommended) {#bidirectional-mul}
+
+Rewrite your definition of multiplication from
+Chapter [Lambda][plfa.Lambda], decorated to support inference.
+
+
+#### Exercise `bidirectional-products` (recommended) {#bidirectional-products}
+
+Extend the bidirectional type rules to include products from
+Chapter [More][plfa.More].
+
+
+#### Exercise `bidirectional-rest` (stretch)
+
+Extend the bidirectional type rules to include the rest of the constructs from
+Chapter [More][plfa.More].
+
+
+#### Exercise `inference-mul` (recommended)
+
+Using the definition from exercise [bidirectional-mul](#bidirectional-mul),
+infer the corresponding inherently typed term.
+Show that erasure of the inferred typing yields your definition of
+multiplication from Chapter [DeBruijn][plfa.DeBruijn].
+
+
+#### Exercise `inference-products` (recommended)
+
+Extend bidirectional inference to include products from
+Chapter [More][plfa.More].
+
+
+#### Exercise `inference-rest` (stretch)
+
+Extend bidirectional inference to include the rest of the constructs from
+Chapter [More][plfa.More].
+
+## Untyped
+
+#### Exercise (`Type≃⊤`)
+
+Show that `Type` is isomorphic to `⊤`, the unit type.
+
+#### Exercise (`Context≃ℕ`)
+
+Show that `Context` is isomorphic to `ℕ`.
+
+#### Exercise (`variant-1`)
+
+How would the rules change if we want call-by-value where terms
+normalise completely?  Assume that `β` should not permit reduction
+unless both terms are in normal form.
+
+#### Exercise (`variant-2`)
+
+How would the rules change if we want call-by-value where terms
+do not reduce underneath lambda?  Assume that `β`
+permits reduction when both terms are values (that is, lambda
+abstractions).  What would `2+2ᶜ` reduce to in this case?
+
+#### Exercise `plus-eval`
+
+Use the evaluator to confirm that `plus · two · two` and `four`
+normalise to the same term.
+
+#### Exercise `multiplication-untyped` (recommended)
+
+Use the encodings above to translate your definition of
+multiplication from previous chapters with the Scott
+representation and the encoding of the fixpoint operator.
+Confirm that two times two is four.
+
+#### Exercise `encode-more` (stretch)
+
+Along the lines above, encode all of the constructs of
+Chapter [More][plfa.More],
+save for primitive numbers, in the untyped lambda calculus.

tspl/PUC.lagda

@@ -91,14 +91,15 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
 
 For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/).
 
-* [PUC-Assignment 1](/PUC-Assignment1/) due Friday 26 April.
-* [PUC-Assignment 2](/PUC-Assignment2/) due Wednesday 22 May.
-* [PUC-Assignment 3](/PUC-Assignment3/) due Wednesday 12 June.
-* [PUC-Assignment 4](/PUC-Assignment4/) due Tuesday 25 June.
-* [Assignment 5](/tspl/Assignment5.pdf) due Tuesday 25 June.
+* [PUC Assignment 1][PUC-Assignment1] due Friday 26 April.
+* [PUC Assignment 2][PUC-Assignment2] due Wednesday 22 May.
+* [PUC Assignment 3][PUC-Assignment3] due Wednesday 5 June.
+* [PUC Assignment 4][PUC-Assignment4] due Wednesday 19 June.
+* [PUC Assignment 5][PUC-Assignment5] due Tuesday 25 June.
+* [PUC Assignment 6](/tspl/first-mock.pdf) due Tuesday 25 June.
   Use file [Exam][Exam]. Despite the rubric, do **all three questions**.
 
 Submit assignments by email to [wadler@inf.ed.ac.uk](mailto:wadler@inf.ed.ac.uk).
 Attach a single file named Assignment1.lagda or the like.  Include
-your name and email in the submitted file.  Ignore instructions to use
-"submit".
+your name and email in the submitted file.
+

tspl/TSPL.lagda

@@ -101,7 +101,7 @@ For instructions on how to set up Agda for PLFA see [Getting Started](/GettingSt
 * [Assignment 2][Assignment2] cw2 due 4pm Thursday 18 October (Week 5)
 * [Assignment 3][Assignment3] cw3 due 4pm Thursday 1 November (Week 7)
 * [Assignment 4][Assignment4] cw4 due 4pm Thursday 15 November (Week 9)
-* [Assignment 5](/tspl/Assignment5.pdf) cw5 due 4pm Thursday 22 November (Week 10)
+* [Assignment 5](/tspl/first-mock.pdf) cw5 due 4pm Thursday 22 November (Week 10)
   <br />
   Use file [Exam][Exam]. Despite the rubric, do **all three questions**.
   
@@ -114,5 +114,5 @@ where N is the number of the assignment.
 
 ## Mock exam
 
-Here is the text of the [mock](/tspl/mock.pdf)
+Here is the text of the [second mock](/tspl/second-mock.pdf)
 and the exam [instructions](/tspl/instructions.pdf).