Skip to content

Commit

Permalink
update Connectives to put records first
Browse files Browse the repository at this point in the history
  • Loading branch information
wadler committed Oct 15, 2024
1 parent 24e0361 commit 933ef88
Showing 1 changed file with 87 additions and 78 deletions.
165 changes: 87 additions & 78 deletions src/plfa/part1/Connectives.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -43,33 +43,23 @@ Given two propositions `A` and `B`, the conjunction `A × B` holds
if both `A` holds and `B` holds. We formalise this idea by
declaring a suitable datatype:
```agda
data _×_ (A B : Set) : Set where
⟨_,_⟩ :
A
→ B
-----
→ A × B
record _×_ (A B : Set) : Set where
constructor ⟨_,_⟩
field
proj₁ : A
proj₂ : B
open _×_
```
Evidence that `A × B` holds is of the form `⟨ M , N ⟩`, where `M`
provides evidence that `A` holds and `N` provides evidence that `B`
holds.
The record construction `record { proj₁ = M ; proj₂ = N }` corresponds to the
term `⟨ M , N ⟩` where `M` is a term of type `A` and `N` is a term of type `B`.
The constructor declaration allows us to write `⟨ M , N ⟩` in place of the
record construction.

Given evidence that `A × B` holds, we can conclude that both
`A` holds and `B` holds:
```agda
proj₁ : ∀ {A B : Set}
→ A × B
-----
→ A
proj₁ ⟨ x , y ⟩ = x
proj₂ : ∀ {A B : Set}
→ A × B
-----
→ B
proj₂ ⟨ x , y ⟩ = y
```
`A` holds and `B` holds, using the projections `proj₁` and `proj₂` respectively.
If `L` provides evidence that `A × B` holds, then `proj₁ L` provides evidence
that `A` holds, and `proj₂ L` provides evidence that `B` holds.

Expand All @@ -92,15 +82,15 @@ we say the connective holds---how to _define_ the connective. An
elimination rule describes what we may conclude when the connective
holds---how to _use_ the connective.[^from-wadler-2015]

In this case, applying each destructor and reassembling the results with the
Applying each destructor and reassembling the results with the
constructor is the identity over products:
```agda
η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× ⟨ x , y ⟩ = refl
η-× w = refl
```
The pattern matching on the left-hand side is essential, since
replacing `w` by `⟨ x , y ⟩` allows both sides of the
propositional equality to simplify to the same term.
For record types, η-equality holds *by definition*.
While proving `η-×`, we do not have to
pattern match on `w` to know that η-equality holds

We set the precedence of conjunction so that it binds less
tightly than anything save disjunction:
Expand All @@ -109,32 +99,44 @@ infixr 2 _×_
```
Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)`.

Alternatively, we can declare conjunction as a record type:
Alternatively, we can declare conjunction as a data type,
and the projections as functions using pattern matching.
```agda
record _×′_ (A B : Set) : Set where
constructor ⟨_,_⟩′
field
proj₁′ : A
proj₂′ : B
open _×′_
```
The record construction `record { proj₁′ = M ; proj₂′ = N }` corresponds to the
term `⟨ M , N ⟩` where `M` is a term of type `A` and `N` is a term of type `B`.
The constructor declaration allows us to write `⟨ M , N ⟩′` in place of the
record construction.
data _×′_ (A B : Set) : Set where
⟨_,_⟩′ :
A
→ B
-----
→ A ×′ B
proj₁′ : ∀ {A B : Set}
→ A ×′ B
-----
→ A
proj₁′ ⟨ x , y ⟩′ = x
The data type `_×_` and the record type `_×′_` behave similarly. One
difference is that for data types we have to prove η-equality, but for record
types, η-equality holds *by definition*. While proving `η-×′`, we do not have to
pattern match on `w` to know that η-equality holds:
proj₂′ : ∀ {A B : Set}
→ A ×′ B
-----
→ B
proj₂′ ⟨ x , y ⟩′ = y
```
The record type `_×_` and the data type `_×′_` behave similarly. One
difference is that for for record
types, η-equality holds *by definition*,
but for data types have to
pattern match know that η-equality holds:
```agda
η-×′ : ∀ {A B : Set} (w : A ×′ B) → ⟨ proj₁′ w , proj₂′ w ⟩′ ≡ w
η-×′ w = refl
η-×′ ⟨ x , y ⟩′ = refl
```
It can be very convenient to have η-equality *definitionally*, and so the
standard library defines `_×_` as a record type. We use the definition from the
standard library in later chapters.

The pattern matching on the left-hand side is essential, since
replacing `w` by `⟨ x , y ⟩′` allows both sides of the
propositional equality to simplify to the same term.
It is convenient to have η-equality *definitionally*,
so we use records in preference to data types
whenever there is only one constructor.

Given two types `A` and `B`, we refer to `A × B` as the
_product_ of `A` and `B`. In set theory, it is also sometimes
Expand Down Expand Up @@ -188,8 +190,8 @@ and similarly for `to∘from`:
record
{ to = λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ }
; from = λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ }
; from∘to = λ{ ⟨ x , y ⟩ → refl }
; to∘from = λ{ ⟨ y , x ⟩ → refl }
; from∘to = λ{ w → refl }
; to∘from = λ{ w → refl }
}
```

Expand All @@ -216,8 +218,8 @@ matching against a suitable pattern to enable simplification:
record
{ to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → ⟨ x , ⟨ y , z ⟩ ⟩ }
; from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → ⟨ ⟨ x , y ⟩ , z ⟩ }
; from∘to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → refl }
; to∘from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → refl }
; from∘to = λ{ w → refl }
; to∘from = λ{ w → refl }
}
```

Expand Down Expand Up @@ -245,15 +247,15 @@ is isomorphic to `(A → B) × (B → A)`.
## Truth is unit

Truth `` always holds. We formalise this idea by
declaring a suitable datatype:
declaring the empty record type.
```agda
data ⊤ : Set where
record ⊤ : Set where
constructor tt
tt :
--
```
Evidence that `` holds is of the form `tt`.
The record construction `record {}` corresponds to the term `tt`. The
constructor declaration allows us to write `tt′`.

There is an introduction rule, but no elimination rule.
Given evidence that `` holds, there is nothing more of interest we
Expand All @@ -264,34 +266,38 @@ The nullary case of `η-×` is `η-⊤`, which asserts that any
value of type `` must be equal to `tt`:
```agda
η-⊤ : ∀ (w : ⊤) → tt ≡ w
η-⊤ tt = refl
```
The pattern matching on the left-hand side is essential. Replacing
`w` by `tt` allows both sides of the propositional equality to
simplify to the same term.
η-⊤ w = refl
Alternatively, we can declare truth as an empty record:
```
Agda knows that *any* value of type `` must be `tt`, so any time we need a
value of type ``, we can tell Agda to figure it out:
```agda
record ⊤′ : Set where
constructor tt′
truth : ⊤
truth = _
```
The record construction `record {}` corresponds to the term `tt`. The
constructor declaration allows us to write `tt′`.

As with the product, the data type `` and the record type `⊤′` behave
Alternatively, we can declare truth as a data type:
```agda
data ⊤′ : Set where
tt′ :
--
⊤′
```
As with the product, the record type `` and the data type `⊤′` behave
similarly, but η-equality holds *by definition* for the record type. While
proving `η-⊤′`, we do not have to pattern match on `w`---Agda *knows* it is
equal to `tt′`:
```agda
η-⊤′ : ∀ (w : ⊤′) → tt′ ≡ w
η-⊤′ w = refl
```
Agda knows that *any* value of type `⊤′` must be `tt′`, so any time we need a
value of type `⊤′`, we can tell Agda to figure it out:
```agda
truth′ : ⊤′
truth′ = _
η-⊤′ tt′ = refl
```
The pattern matching on the left-hand side is essential. Replacing
`w` by `tt′` allows both sides of the propositional equality to
simplify to the same term.
As with products, it is convenient to have η-equality *definitionally*,
so we use records in preference to data types
whenever there is only one constructor.

We refer to `` as the _unit_ type. And, indeed,
type `` has exactly one member, `tt`. For example, the following
Expand Down Expand Up @@ -504,6 +510,9 @@ uniq-⊥ h ()
Using the absurd pattern asserts there are no possible values for `w`,
so the equation holds trivially.

We can also use `()` in nested patterns. For instance,
`⟨ () , tt ⟩` is a pattern of type `⊥ × ⊤`.

We refer to `` as the _empty_ type. And, indeed,
type `` has no members. For example, the following function
enumerates all possible arguments of type ``:
Expand Down Expand Up @@ -664,7 +673,7 @@ is the same as the assertion that if `A` holds then `C` holds and if
{ to = λ{ f → ⟨ f ∘ inj₁ , f ∘ inj₂ ⟩ }
; from = λ{ ⟨ g , h ⟩ → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } }
; from∘to = λ{ f → extensionality λ{ (inj₁ x) → refl ; (inj₂ y) → refl } }
; to∘from = λ{ ⟨ g , h ⟩ → refl }
; to∘from = λ{ _ → refl }
}
```

Expand Down Expand Up @@ -733,10 +742,10 @@ Sums do not distribute over products up to isomorphism, but it is an embedding:
}
```
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
easy to write a variant that instead returns `inj₂ z′`. We have
As given, it takes `⟨ inj₂ z , inj₂ w` to `inj₂ z`, but it is
easy to write a variant that instead returns `inj₂ w`. We have
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 `w` in this case.

In the usual approach to logic, both of the distribution laws
are given as equivalences, where each side implies the other:
Expand Down

0 comments on commit 933ef88

Please sign in to comment.