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

updated pairs in Connectives

Browse source
This commit is contained in:
wadler 2018-03-20 18:32:08 -03:00
parent a647ee9f9d
commit b263d68c7d
5 changed files with 194 additions and 245 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
_config.yml
View file

@ -1,4 +1,4 @@
title: Software Foundations in Agda title: Programming Language Theory in Agda
# the author field should not be used in the template # the author field should not be used in the template
author: Wen Kokke author: Wen Kokke
@ -14,7 +14,7 @@ contributors:
twitter_username: philipwadler twitter_username: philipwadler
description: > description: >
Software Foundations in Agda. Programming Language Theory in Agda.
# include disqus to allow comments e.d. # include disqus to allow comments e.d.
disqus: disqus:

288
src/Connectives.lagda
View file

@ -44,25 +44,31 @@ if both `A` holds and `B` holds. We formalise this idea by
declaring a suitable inductive type. declaring a suitable inductive type.
\begin{code} \begin{code}
data _×_ : Set → Set → Set where data _×_ : Set → Set → Set where
_,_ : ∀ {A B : Set} → A → B → A × B ⟨_,_⟩ : ∀ {A B : Set} → A → B → A × B
\end{code} \end{code}
Evidence that `A × B` holds is of the form Evidence that `A × B` holds is of the form
`(M , N)`, where `M` is evidence that `A` holds and `⟨ M , N ⟩`, where `M` provides evidence that `A` holds and
`N` is evidence that `B` holds. By convention, we `N` provides evidence that `B` holds. In the standard library,
parenthesise pairs, even though `M , N` is also the pair constructor is `_,_`, but here we rename it to
`⟨_,_⟩` so that comma is available for other notations
(in particular, lists and environments).
<!--
By convention, we parenthesise pairs, even though `M , N` is also
accepted by Agda. accepted by Agda.
-->
Given evidence that `A × B` holds, we can conclude that either Given evidence that `A × B` holds, we can conclude that either
`A` holds or `B` holds. `A` holds or `B` holds.
\begin{code} \begin{code}
proj₁ : ∀ {A B : Set} → A × B → A proj₁ : ∀ {A B : Set} → A × B → A
proj₁ (x , y) = x proj₁ ⟨ x , y ⟩ = x
proj₂ : ∀ {A B : Set} → A × B → B proj₂ : ∀ {A B : Set} → A × B → B
proj₂ (x , y) = y proj₂ ⟨ x , y ⟩ = y
\end{code} \end{code}
If `L` is evidence that `A × B` holds, then `fst L` is evidence If `L` provides evidence that `A × B` holds, then `proj₁ L` provides evidence
that `A` holds, and `proj₂ L` is evidence that `B` holds. that `A` holds, and `proj₂ L` provides evidence that `B` holds.
Equivalently, we could also declare conjunction as a record type. Equivalently, we could also declare conjunction as a record type.
\begin{code} \begin{code}
@ -81,39 +87,41 @@ Here record construction
corresponds to the term corresponds to the term
( M , N ) ⟨ M , N ⟩
where `M` is a term of type `A` and `N` is a term of type `B`. where `M` is a term of type `A` and `N` is a term of type `B`.
When `(_,_)` appears on the right-hand side of an equation we When `⟨_,_⟩` appears in a term on the right-hand side of an equation
refer to it as a *constructor*, and when it appears on the we refer to it as a *constructor*, and when it appears in a pattern on
left-hand side we refer to it as a *destructor*. We also refer the left-hand side of an equation we refer to it as a *destructor*.
to `proj₁` and `proj₂` as destructors, since they play a similar role. We also refer to `proj₁` and `proj₂` as destructors, since they play a
Other terminology refers to constructor as *introducing* a conjunction, similar role. Other terminology refers to a constructor as
and to a destructor as *eliminating* a conjunction. *introducing* a conjunction, and to a destructor as *eliminating* a
Indeed, `proj₁` and `proj₂` are sometimes given the names conjunction. Indeed, `proj₁` and `proj₂` are sometimes given the
`×-elim₁` and `×-elim₂`. names `×-elim₁` and `×-elim₂`.
Applying each destructor and reassembling the results with the Applying each destructor and reassembling the results with the
constructor is the identity over products. constructor is the identity over products.
\begin{code} \begin{code}
η-× : ∀ {A B : Set} (w : A × B) → (proj₁ w , proj₂ w) ≡ w η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× (x , y) = refl η-× ⟨ x , y ⟩ = refl
\end{code} \end{code}
The pattern matching on the left-hand side is essential, since The pattern matching on the left-hand side is essential, since
replacing `w` by `(x , y)` allows both sides of the equation to replacing `w` by `⟨ x , y ⟩` allows both sides of the equation to
simplify to the same term. simplify to the same term.
We set the precedence of conjunction so that it binds less We set the precedence of conjunction so that it binds less
tightly than anything save disjunction, and of the pairing tightly than anything save disjunction.
operator so that it binds less tightly than any arithmetic
operator.
\begin{code} \begin{code}
infixr 2 _×_ infixr 2 _×_
infixr 4 _,_
\end{code} \end{code}
Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)` and Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)`.
<!--
and of the pairing operator so that it binds less tightly
than any arithmetic operator.
`(m * n , p)` parses as `((m * n) , p)`. `(m * n , p)` parses as `((m * n) , p)`.
-->
Given two types `A` and `B`, we refer to `A x B` as the Given two types `A` and `B`, we refer to `A x B` as the
*product* of `A` and `B`. In set theory, it is also sometimes *product* of `A` and `B`. In set theory, it is also sometimes
@ -136,19 +144,19 @@ data Tri : Set where
\end{code} \end{code}
Then the type `Bool × Tri` has six members: Then the type `Bool × Tri` has six members:
(true , aa) (true , bb) (true , cc) ⟨ true , aa ⟩ ⟨ true , bb ⟩ ⟨ true , cc ⟩
(false , aa) (false , bb) (false , cc) ⟨ false , aa ⟩ ⟨ false , bb ⟩ ⟨ false , cc ⟩
For example, the following function enumerates all For example, the following function enumerates all
possible arguments of type `Bool × Tri`: possible arguments of type `Bool × Tri`:
\begin{code} \begin{code}
×-count : Bool × Tri → ℕ ×-count : Bool × Tri → ℕ
×-count (true , aa) = 1 ×-count ⟨ true , aa ⟩ = 1
×-count (true , bb) = 2 ×-count ⟨ true , bb ⟩ = 2
×-count (true , cc) = 3 ×-count ⟨ true , cc ⟩ = 3
×-count (false , aa) = 4 ×-count ⟨ false , aa ⟩ = 4
×-count (false , bb) = 5 ×-count ⟨ false , bb ⟩ = 5
×-count (false , cc) = 6 ×-count ⟨ false , cc ⟩ = 6
\end{code} \end{code}
Product on types also shares a property with product on numbers in Product on types also shares a property with product on numbers in
@ -162,13 +170,13 @@ Instantiating the patterns correctly in `from∘to` and `to∘from` is essential
Replacing the definition of `from∘to` by `λ w → refl` will not work; Replacing the definition of `from∘to` by `λ w → refl` will not work;
and similarly for `to∘from`, which does the same (up to renaming). and similarly for `to∘from`, which does the same (up to renaming).
\begin{code} \begin{code}
×-comm : ∀ {A B : Set} → (A × B) ≃ (B × A) ×-comm : ∀ {A B : Set} → A × B ≃ B × A
×-comm = ×-comm =
record record
{ to = λ{ (x , y) → (y , x)} { to = λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ }
; from = λ{ (y , x) → (x , y)} ; from = λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ }
; from∘to = λ{ (x , y) → refl } ; from∘to = λ{ ⟨ x , y ⟩ → refl }
; to∘from = λ{ (y , x) → refl } ; to∘from = λ{ ⟨ y , x ⟩ → refl }
} }
\end{code} \end{code}
@ -191,13 +199,13 @@ taking `((x , y) , z)` to `(x , (y , z))`, and the `from` function does
the inverse. Again, the evidence of left and right inverse requires the inverse. Again, the evidence of left and right inverse requires
matching against a suitable pattern to enable simplification. matching against a suitable pattern to enable simplification.
\begin{code} \begin{code}
×-assoc : ∀ {A B C : Set} → ((A × B) × C) ≃ (A × (B × C)) ×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
×-assoc = ×-assoc =
record record
{ to = λ{ ((x , y) , z) → (x , (y , z)) } { to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → ⟨ x , ⟨ y , z ⟩ ⟩ }
; from = λ{ (x , (y , z)) → ((x , y) , z) } ; from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → ⟨ ⟨ x , y ⟩ , z ⟩ }
; from∘to = λ{ ((x , y) , z) → refl } ; from∘to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → refl }
; to∘from = λ{ (x , (y , z)) → refl } ; to∘from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → refl }
} }
\end{code} \end{code}
@ -250,12 +258,12 @@ identity, the `to` function takes `(tt , x)` to `x`, and the `from`
function does the inverse. The evidence of left inverse requires function does the inverse. The evidence of left inverse requires
matching against a suitable pattern to enable simplification. matching against a suitable pattern to enable simplification.
\begin{code} \begin{code}
⊤-identityˡ : ∀ {A : Set} → (⊤ × A) ≃ A ⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A
⊤-identityˡ = ⊤-identityˡ =
record record
{ to = λ{ (tt , x) → x } { to = λ{ ⟨ tt , x ⟩ → x }
; from = λ{ x → (tt , x) } ; from = λ{ x → ⟨ tt , x ⟩ }
; from∘to = λ{ (tt , x) → refl } ; from∘to = λ{ ⟨ tt , x ⟩ → refl }
; to∘from = λ{ x → refl } ; to∘from = λ{ x → refl }
} }
\end{code} \end{code}
@ -300,8 +308,8 @@ data _⊎_ : Set → Set → Set where
inj₂ : ∀ {A B : Set} → B → A ⊎ B inj₂ : ∀ {A B : Set} → B → A ⊎ B
\end{code} \end{code}
Evidence that `A ⊎ B` holds is either of the form `inj₁ M`, where `M` Evidence that `A ⊎ B` holds is either of the form `inj₁ M`, where `M`
is evidence that `A` holds, or `inj₂ N`, where `N` is evidence that provides evidence that `A` holds, or `inj₂ N`, where `N` provides
`B` holds. evidence that `B` holds.
Given evidence that `A → C` and `B → C` both hold, then given Given evidence that `A → C` and `B → C` both hold, then given
evidence that `A ⊎ B` holds we can conclude that `C` holds. evidence that `A ⊎ B` holds we can conclude that `C` holds.
@ -356,19 +364,19 @@ a type `Tri` with three members, as defined earlier.
Then the type `Bool ⊎ Tri` has five Then the type `Bool ⊎ Tri` has five
members: members:
(inj₁ true) (inj₂ aa) inj₁ true inj₂ aa
(inj₁ false) (inj₂ bb) inj₁ false inj₂ bb
(inj₂ cc) inj₂ cc
For example, the following function enumerates all For example, the following function enumerates all
possible arguments of type `Bool ⊎ Tri`: possible arguments of type `Bool ⊎ Tri`:
\begin{code} \begin{code}
⊎-count : Bool ⊎ Tri → ℕ ⊎-count : Bool ⊎ Tri → ℕ
⊎-count (inj₁ true) = 1 ⊎-count (inj₁ true) = 1
⊎-count (inj₁ false) = 2 ⊎-count (inj₁ false) = 2
⊎-count (inj₂ aa) = 3 ⊎-count (inj₂ aa) = 3
⊎-count (inj₂ bb) = 4 ⊎-count (inj₂ bb) = 4
⊎-count (inj₂ cc) = 5 ⊎-count (inj₂ cc) = 5
\end{code} \end{code}
Sum on types also shares a property with sum on numbers in that it is Sum on types also shares a property with sum on numbers in that it is
@ -382,18 +390,18 @@ does the same (up to renaming).
\begin{code} \begin{code}
⊎-comm : ∀ {A B : Set} → (A ⊎ B) ≃ (B ⊎ A) ⊎-comm : ∀ {A B : Set} → (A ⊎ B) ≃ (B ⊎ A)
⊎-comm = record ⊎-comm = record
{ to = λ{ (inj₁ x) → (inj₂ x) { to = λ{ (inj₁ x) → (inj₂ x)
; (inj₂ y) → (inj₁ y) ; (inj₂ y) → (inj₁ y)
} }
; from = λ{ (inj₁ y) → (inj₂ y) ; from = λ{ (inj₁ y) → (inj₂ y)
; (inj₂ x) → (inj₁ x) ; (inj₂ x) → (inj₁ x)
} }
; from∘to = λ{ (inj₁ x) → refl ; from∘to = λ{ (inj₁ x) → refl
; (inj₂ y) → refl ; (inj₂ y) → refl
} }
; to∘from = λ{ (inj₁ y) → refl ; to∘from = λ{ (inj₁ y) → refl
; (inj₂ x) → refl ; (inj₂ x) → refl
} }
} }
\end{code} \end{code}
Being *commutative* is different from being *commutative up to Being *commutative* is different from being *commutative up to
@ -413,24 +421,24 @@ For associativity, the `to` function reassociates, and the `from` function does
the inverse. Again, the evidence of left and right inverse requires the inverse. Again, the evidence of left and right inverse requires
matching against a suitable pattern to enable simplification. matching against a suitable pattern to enable simplification.
\begin{code} \begin{code}
⊎-assoc : ∀ {A B C : Set} → ((A ⊎ B) ⊎ C) ≃ (A ⊎ (B ⊎ C)) ⊎-assoc : ∀ {A B C : Set} → (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C)
⊎-assoc = record ⊎-assoc = record
{ to = λ{ (inj₁ (inj₁ x)) → (inj₁ x) { to = λ{ (inj₁ (inj₁ x)) → (inj₁ x)
; (inj₁ (inj₂ y)) → (inj₂ (inj₁ y)) ; (inj₁ (inj₂ y)) → (inj₂ (inj₁ y))
; (inj₂ z) → (inj₂ (inj₂ z)) ; (inj₂ z) → (inj₂ (inj₂ z))
} }
; from = λ{ (inj₁ x) → (inj₁ (inj₁ x)) ; from = λ{ (inj₁ x) → (inj₁ (inj₁ x))
; (inj₂ (inj₁ y)) → (inj₁ (inj₂ y)) ; (inj₂ (inj₁ y)) → (inj₁ (inj₂ y))
; (inj₂ (inj₂ z)) → (inj₂ z) ; (inj₂ (inj₂ z)) → (inj₂ z)
} }
; from∘to = λ{ (inj₁ (inj₁ x)) → refl ; from∘to = λ{ (inj₁ (inj₁ x)) → refl
; (inj₁ (inj₂ y)) → refl ; (inj₁ (inj₂ y)) → refl
; (inj₂ z) → refl ; (inj₂ z) → refl
} }
; to∘from = λ{ (inj₁ x) → refl ; to∘from = λ{ (inj₁ x) → refl
; (inj₂ (inj₁ y)) → refl ; (inj₂ (inj₁ y)) → refl
; (inj₂ (inj₂ z)) → refl ; (inj₂ (inj₂ z)) → refl
} }
} }
\end{code} \end{code}
@ -451,13 +459,12 @@ data ⊥ : Set where
\end{code} \end{code}
There is no possible evidence that `⊥` holds. There is no possible evidence that `⊥` holds.
Given evidence that `⊥` holds, we might conclude anything! Since Since false never holds, knowing that it holds tells us we are in a
false never holds, knowing that it holds tells us we are in a paradoxical situation. Given evidence that `⊥` holds, we might
paradoxical situation. This is a basic principle of logic, conclude anything! This is a basic principle of logic, known in
known in medieval times by the latin phrase *ex falso*, medieval times by the latin phrase *ex falso*, and known to children
and known to children through phrases such as through phrases such as "if pigs had wings, then I'd be the Queen of
"if pigs had wings, then I'd be the Queen of Sheba". Sheba". We formalise it as follows.
We formalise it as follows.
\begin{code} \begin{code}
⊥-elim : ∀ {A : Set} → ⊥ → A ⊥-elim : ∀ {A : Set} → ⊥ → A
⊥-elim () ⊥-elim ()
@ -473,8 +480,7 @@ is equal to any arbitrary function from `⊥`.
uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w
uniq-⊥ h () uniq-⊥ h ()
\end{code} \end{code}
The pattern matching on the left-hand side is essential. Using Using the absurd pattern asserts there are no possible values for `w`,
the absurd pattern asserts there are no possible values for `w`,
so the equation holds trivially. so the equation holds trivially.
We refer to `⊥` as *empty* type. And, indeed, We refer to `⊥` as *empty* type. And, indeed,
@ -497,16 +503,14 @@ a suitable pattern to enable simplification.
⊥-identityˡ : ∀ {A : Set} → (⊥ ⊎ A) ≃ A ⊥-identityˡ : ∀ {A : Set} → (⊥ ⊎ A) ≃ A
⊥-identityˡ = ⊥-identityˡ =
record record
{ to = λ{ (inj₁ ()) { to = λ{ (inj₁ ())
; (inj₂ x) → x ; (inj₂ x) → x
} }
; from = λ{ x → inj₂ x ; from = λ{ x → inj₂ x }
} ; from∘to = λ{ (inj₁ ())
; from∘to = λ{ (inj₁ ()) ; (inj₂ x) → refl
; (inj₂ x) → refl }
} ; to∘from = λ{ x → refl }
; to∘from = λ{ x → refl
}
} }
\end{code} \end{code}
@ -609,15 +613,15 @@ arguments of the type `Bool → Tri`:
\begin{code} \begin{code}
→-count : (Bool → Tri) → ℕ →-count : (Bool → Tri) → ℕ
→-count f with f true | f false →-count f with f true | f false
... | aa | aa = 1 ... | aa | aa = 1
... | aa | bb = 2 ... | aa | bb = 2
... | aa | cc = 3 ... | aa | cc = 3
... | bb | aa = 4 ... | bb | aa = 4
... | bb | bb = 5 ... | bb | bb = 5
... | bb | cc = 6 ... | bb | cc = 6
... | cc | aa = 7 ... | cc | aa = 7
... | cc | bb = 8 ... | cc | bb = 8
... | cc | cc = 9 ... | cc | cc = 9
\end{code} \end{code}
Exponential on types also share a property with exponential on Exponential on types also share a property with exponential on
@ -640,10 +644,10 @@ The proof of the right inverse requires extensionality.
currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C) currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
currying = currying =
record record
{ to = λ{ f → λ{ (x , y) → f x y }} { to = λ{ f → λ{ ⟨ x , y ⟩ → f x y }}
; from = λ{ g → λ{ x → λ{ y → g (x , y) }}} ; from = λ{ g → λ{ x → λ{ y → g ⟨ x , y ⟩ }}}
; from∘to = λ{ f → refl } ; from∘to = λ{ f → refl }
; to∘from = λ{ g → extensionality λ{ (x , y) → refl }} ; to∘from = λ{ g → extensionality λ{ ⟨ x , y ⟩ → refl }}
} }
\end{code} \end{code}
@ -658,7 +662,7 @@ is isomorphic to a function that accepts a pair of arguments:
_+′_ : (ℕ × ℕ) → ℕ _+′_ : (ℕ × ℕ) → ℕ
Agda is optimised for currying, so `2 + 3` abbreviates `_+_ 2 3`. Agda is optimised for currying, so `2 + 3` abbreviates `_+_ 2 3`.
In a language optimised for pairing, we would take `2 +′ 3` as In a language optimised for pairing, we would instead take `2 +′ 3` as
an abbreviation for `_+′_ (2 , 3)`. an abbreviation for `_+′_ (2 , 3)`.
Corresponding to the law Corresponding to the law
@ -676,10 +680,10 @@ is the same as the assertion that if `A` holds then `C` holds and if
→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C)) →-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
→-distrib-⊎ = →-distrib-⊎ =
record record
{ to = λ{ f → ( (λ{ x → f (inj₁ x) }) , (λ{ y → f (inj₂ y) }) ) } { to = λ{ f → ⟨ f ∘ inj₁ , f ∘ inj₂ ⟩ }
; from = λ{ (g , h) → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } } ; from = λ{ ⟨ g , h ⟩ → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } }
; from∘to = λ{ f → extensionality λ{ (inj₁ x) → refl ; (inj₂ y) → refl } } ; from∘to = λ{ f → extensionality λ{ (inj₁ x) → refl ; (inj₂ y) → refl } }
; to∘from = λ{ (g , h) → refl } ; to∘from = λ{ ⟨ g , h ⟩ → refl }
} }
\end{code} \end{code}
@ -699,10 +703,10 @@ and the rule `η-×` for products.
→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C) →-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
→-distrib-× = →-distrib-× =
record record
{ to = λ{ f → ( (λ{ x → proj₁ (f x) }) , (λ{ y → proj₂ (f y)}) ) } { to = λ{ f → ⟨ proj₁ ∘ f , proj₂ ∘ f ⟩ }
; from = λ{ (g , h) → λ{ x → (g x , h x) } } ; from = λ{ ⟨ g , h ⟩ → λ{ x → ⟨ g x , h x ⟩ } }
; from∘to = λ{ f → extensionality λ{ x → η-× (f x) } } ; from∘to = λ{ f → extensionality λ{ x → η-× (f x) } }
; to∘from = λ{ (g , h) → refl } ; to∘from = λ{ ⟨ g , h ⟩ → refl }
} }
\end{code} \end{code}
@ -715,17 +719,17 @@ this fact is similar in structure to our previous results.
×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C) ×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)
×-distrib-⊎ = ×-distrib-⊎ =
record record
{ to = λ{ ((inj₁ x) , z) → (inj₁ (x , z)) { to = λ{ ⟨ inj₁ x , z ⟩ → (inj₁ ⟨ x , z ⟩)
; ((inj₂ y) , z) → (inj₂ (y , z)) ; ⟨ inj₂ y , z ⟩ → (inj₂ ⟨ y , z ⟩)
} }
; from = λ{ (inj₁ (x , z)) → ((inj₁ x) , z) ; from = λ{ (inj₁ ⟨ x , z ⟩) → ⟨ inj₁ x , z ⟩
; (inj₂ (y , z)) → ((inj₂ y) , z) ; (inj₂ ⟨ y , z ⟩) → ⟨ inj₂ y , z ⟩
} }
; from∘to = λ{ ((inj₁ x) , z) → refl ; from∘to = λ{ ⟨ inj₁ x , z ⟩ → refl
; ((inj₂ y) , z) → refl ; ⟨ inj₂ y , z ⟩ → refl
} }
; to∘from = λ{ (inj₁ (x , z)) → refl ; to∘from = λ{ (inj₁ ⟨ x , z ⟩) → refl
; (inj₂ (y , z)) → refl ; (inj₂ ⟨ y , z ⟩) → refl
} }
} }
\end{code} \end{code}
@ -735,21 +739,21 @@ Sums do not distribute over products up to isomorphism, but it is an embedding.
⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C) ⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C)
⊎-distrib-× = ⊎-distrib-× =
record record
{ to = λ{ (inj₁ (x , y)) → (inj₁ x , inj₁ y) { to = λ{ (inj₁ ⟨ x , y ⟩) → ⟨ inj₁ x , inj₁ y ⟩
; (inj₂ z) → (inj₂ z , inj₂ z) ; (inj₂ z) → ⟨ inj₂ z , inj₂ z ⟩
} }
; from = λ{ (inj₁ x , inj₁ y) → (inj₁ (x , y)) ; from = λ{ ⟨ inj₁ x , inj₁ y ⟩ → (inj₁ ⟨ x , y ⟩)
; (inj₁ x , inj₂ z) → (inj₂ z) ; ⟨ inj₁ x , inj₂ z ⟩ → (inj₂ z)
; (inj₂ z , _ ) → (inj₂ z) ; ⟨ inj₂ z , _ ⟩ → (inj₂ z)
} }
; from∘to = λ{ (inj₁ (x , y)) → refl ; from∘to = λ{ (inj₁ ⟨ x , y ⟩) → refl
; (inj₂ z) → refl ; (inj₂ z) → refl
} }
} }
\end{code} \end{code}
Note that there is a choice in how we write the `from` function. Note that there is a choice in how we write the `from` function.
As given, it takes `(inj₂ z , inj₂ z′)` to `(inj₂ z)`, but it is As given, it takes `⟨ inj₂ z , inj₂ z′ ⟩` to `inj₂ z`, but it is
easy to write a variant that instead returns `(inj₂ z′)`. We have easy to write a variant that instead returns `inj₂ z′`. We have
an embedding rather than an isomorphism because the an embedding rather than an isomorphism because the
`from` function must discard either `z` or `z′` in this case. `from` function must discard either `z` or `z′` in this case.
@ -796,7 +800,7 @@ Show that `A ⇔ B` is isomorphic to `(A → B) × (B → A)`.
Definitions similar to those in this chapter can be found in the standard library. Definitions similar to those in this chapter can be found in the standard library.
\begin{code} \begin{code}
import Data.Product using (_×_; _,_; proj₁; proj₂) import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
import Data.Unit using (⊤; tt) import Data.Unit using (⊤; tt)
import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to ⊎-elim) import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to ⊎-elim)
import Data.Empty using (⊥; ⊥-elim) import Data.Empty using (⊥; ⊥-elim)

82
src/Lists.lagda
View file

@ -4,8 +4,8 @@ layout : page
permalink : /Lists permalink : /Lists
--- ---
This chapter discusses the list data type. It uses many of the techniques This chapter discusses the list data type. It gives further examples
developed for natural numbers in a different context, and provides of many of the techniques we have developed so far, and provides
examples of polymorphic types and functions. examples of polymorphic types and functions.
## Imports ## Imports
@ -26,52 +26,44 @@ open import Isomorphism using (_≃_)
Lists are defined in Agda as follows. Lists are defined in Agda as follows.
\begin{code} \begin{code}
data List (A : Set) : Set where data List (A : Set) : Set where
[] : List A [] : List A
_∷_ : A → List A → List A _∷_ : A → List A → List A
infixr 5 _∷_ infixr 5 _∷_
\end{code} \end{code}
Let's unpack this definition. The phrase Let's unpack this definition. If `A` is a set, then `List A` is a set.
The next two lines tell us that `[]` (pronounced *nil*) is a list of
List (A : Set) : Set type `A` (often called the *empty* list), and that `_∷_` (pronounced
*cons*, short for *constructor*) takes a value of type `A` and a `List
tells us that `List` is a function from a `Set` to a `Set`. A` and returns a `List A`. Operator `_∷_` has precedence level 5 and
We write `A` consistently for the argument of `List` throughout associates to the right.
the declaration. The next two lines tell us that `[]` (pronounced *nil*)
is the empty list of type `A`, and that `_∷_` (pronounced *cons*,
short for *constructor*) takes a value of type `A` and a `List A` and
returns a `List A`. Operator `_∷_` has precedence level 5 and associates
to the right.
For example, For example,
\begin{code} \begin{code}
ex₀ : List ℕ _ : List ℕ
ex₀ = 0 ∷ 1 ∷ 2 ∷ [] _ = 0 ∷ 1 ∷ 2 ∷ []
\end{code} \end{code}
denotes the list of the first three natural numbers. Since `_::_` denotes the list of the first three natural numbers. Since `_::_`
associates to the right, the term above parses as `0 ∷ (1 ∷ (2 ∷ []))`. associates to the right, the term parses as `0 ∷ (1 ∷ (2 ∷ []))`.
Here `0` is the first element of the list, called the *head*, Here `0` is the first element of the list, called the *head*,
and `1 ∷ (2 ∷ [])` is a list of the remaining elements, called the and `1 ∷ (2 ∷ [])` is a list of the remaining elements, called the
*tail*. Lists are a rather strange beast: a head and a tail, *tail*. Lists are a rather strange beast: they have a head and a tail,
nothing in between, and the tail is itself another list! nothing in between, and the tail is itself another list!
The definition of lists could also be written as follows. As we've seen, parameterised types can be translated to
indexed types. The definition above is equivalent to the following.
\begin{code} \begin{code}
data List′ : Set → Set where data List′ : Set → Set where
[]′ : ∀ {A : Set} → List′ A []′ : ∀ {A : Set} → List′ A
_∷′_ : ∀ {A : Set} → A → List′ A → List′ A _∷′_ : ∀ {A : Set} → A → List′ A → List′ A
\end{code} \end{code}
This is essentially equivalent to the previous definition, Each constructor takes the parameter as an implicit argument.
and lets us see that constructors `[]` and `_∷_` each act as Thus, our example list could also be written
if they take an implicit argument, the type of the list. \begin{code}
_ : List ℕ
The previous form is preferred because it is more compact _ = _∷_ {ℕ} 0 (_∷_ {ℕ} 1 (_∷_ {ℕ} 2 ([] {ℕ})))
and easier to read; using it also improves Agda's ability to \end{code}
reason about when a function definition based on pattern matching where here we have made the implicit parameters explicit.
is well defined. An important difference is that in the previous
form we must write `List A` consistently everywhere, whereas in
the second form it would be permitted to replace an occurrence
of `List A` by `List ℕ`, say.
Including the lines Including the lines
@ -81,37 +73,25 @@ tells Agda that the type `List` corresponds to the Haskell type
list, and the constructors `[]` and `_∷_` correspond to nil and list, and the constructors `[]` and `_∷_` correspond to nil and
cons respectively, allowing a more efficient representation of lists. cons respectively, allowing a more efficient representation of lists.
## List syntax ## List syntax
We can write lists more conveniently by introducing the following definitions. We can write lists more conveniently by introducing the following definitions.
\begin{code} \begin{code}
-- [_] : ∀ {A : Set} → A → List A
-- pattern [ z ] = z ∷ []
pattern [_] z = z ∷ [] pattern [_] z = z ∷ []
-- [_,_] : ∀ {A : Set} → A → A → List A
-- pattern [ y , z ] = y ∷ z ∷ []
pattern [_,_] y z = y ∷ z ∷ [] pattern [_,_] y z = y ∷ z ∷ []
-- [_,_,_] : ∀ {A : Set} → A → A → A → List A
-- pattern [ x , y , z ] = x ∷ y ∷ z ∷ []
pattern [_,_,_] x y z = x ∷ y ∷ z ∷ [] pattern [_,_,_] x y z = x ∷ y ∷ z ∷ []
-- [_,_,_,_] : ∀ {A : Set} → A → A → A → A → List A
-- pattern [ w , x , y , z ] = w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ [] pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ []
-- [_,_,_,_,_] : ∀ {A : Set} → A → A → A → A → A → List A
-- pattern [ v , w , x , y , z ] = v ∷ w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ [] pattern [_,_,_,_,_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ []
-- [_,_,_,_,_,_] : ∀ {A : Set} → A → A → A → A → A → A → List A
-- pattern [ u , v , w , x , y , z ] = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ [] pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []
\end{code} \end{code}
Agda recognises that this is a bracketing notation, This is our first use of pattern declarations. For instance,
and hence we can write things like `length [ 0 , 1 , 2 ]` the third line tells us that `[ x , y , z ]` is equivalent to
rather than `length ([ 0 , 1 , 2 ])`. `x ∷ y ∷ z ∷ []`, and permits the former to appear either in
a pattern on the left-hand side of an equation, or a term
on the right-hand side of an equation.
Agda recognises `[_,_,_]` as a bracketing notation, and hence `length
[ 0 , 1 , 2 ]` parses as `length ([ 0 , 1 , 2 ])`.
## Append ## Append

23
src/Preface.lagda
View file

@ -13,15 +13,21 @@ March 2018. When that is done it will be announced here, and that would be
an excellent time to comment on the first part. an excellent time to comment on the first part.
## Personal remarks ## Personal remarks: From TAPL to PLTA
Since 2013, I teach a course on Types and Semantics for Programming I, along with many others, am a fan of Peirce's [Types and Programming
Languages to fourth-year undergraduates and masters students at the Languages][tapl], known by the acronym TAPL. One of my best students
University of Edinburgh. That course had been based on the textbook started writing his own systems with no help from me, trained by that
[Software Foundations][sf], by Pierce and others, written in Coq. I book.
am convinced of Pierce's claim that basing a course around a proof
assistant aids learning, as summarised in his ICFP Keynote, [Lambda, Since 2013, I have taught a course on Types and Semantics for
The Ultimate TA][ta]. Programming Languages to fourth-year undergraduates and masters
students at the University of Edinburgh. That course is not based on
TAPL, but on Pierce's subsequent textbook, [Software Foundations],
written in collaboration with others and based on 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 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 that Coq may not be the best vehicle. Too much of the course needs to
@ -69,6 +75,7 @@ Most of the text was written during a sabbatical in the first half of 2018.
-- Philip Wadler, Rio de Janeiro, January--June 2018 -- Philip Wadler, Rio de Janeiro, January--June 2018
[tapl]: http://www.cis.upenn.edu/~bcpierce/tapl/index.html
[sf]: https://softwarefoundations.cis.upenn.edu/ [sf]: https://softwarefoundations.cis.upenn.edu/
[ta]: http://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf [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 [stump]: http://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?cPath=24&products_id=908

42
src/Relations.lagda
View file

@ -271,48 +271,6 @@ given `suc m ≤ suc n` and `suc n ≤ suc m` and must show `suc m ≡ suc n`.
The inductive hypothesis `≤-antisym m≤n n≤m` establishes that `m ≡ n`, The inductive hypothesis `≤-antisym m≤n n≤m` establishes that `m ≡ n`,
and our goal follows by congruence. and our goal follows by congruence.
<!--
In the base case, both relations hold by `z≤n`,
so it must be the case that `m` and `n` are both `zero`,
in which case `m ≡ n` holds by reflexivity. (The reflexivity
of `_≡_`, that is, not the reflexivity of `_≤_`.)
In the inductive case, `m ≤ n` holds by `s≤s m≤n` and `n ≤ m` holds by
`s≤s n≤m`, so it must be that `m` is `suc m′` and `n` is `suc n′`, for
some `m′` and `n′`, where `m≤n` is evidence that `m′ ≤ n′` and `n≤m`
is evidence that `n′ ≤ m′`. The inductive hypothesis `≤-antisym m≤n n≤m`
establishes that `m′ ≡ n′`, and so the final result follows by congruence.
-->
<!--
## Disjunction
In order to state totality, we need a way to formalise disjunction,
the notion that given two propositions either one or the other holds.
In Agda, we do so by declaring a suitable inductive type.
\begin{code}
data _⊎_ : Set → Set → Set where
inj₁ : ∀ {A B : Set} → A → A ⊎ B
inj₂ : ∀ {A B : Set} → B → A ⊎ B
\end{code}
This tells us that if `A` and `B` are propositions then `A ⊎ B` is
also a proposition. Evidence that `A ⊎ B` holds is either of the form
`inj₁ x`, where `x` is evidence that `A` holds, or `inj₂ y`, where
`y` is evidence that `B` holds.
We set the precedence of disjunction so that it binds less tightly than
inequality.
\begin{code}
infixr 1 _⊎_
\end{code}
Thus, `m ≤ n ⊎ n ≤ m` parses as `(m ≤ n) ⊎ (n ≤ m)`.
-->
## Total ## Total