8 Isomorphism

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

Considering the amount of space devoted to it, the motivating material in this chapter is used very little in what follows. But it is good practice in using Agda, and a good vehicle for introducing some useful new features.

8.1 Lambda expressions

If you’ve had experience with functional programming, you’ve seen lambdas before. If not, you will quickly grasp the basics (a way of creating a function on the fly without giving it a name) but wonder how useful it can be. The short answer is "incredibly useful", though in the context of Agda "incredibly" becomes "moderately", at least as far as surface syntax is concerned. Many Agda features are just syntactic sugar over lambda, and this is true for other functional languages as well. In the second half of the course, we will look at proving things about models of computation based on lambdas, which is pretty much the basis for modern theories of programming languages (even languages in which lambda plays little or no role).

You may have already seen lambdas if you’ve tried to refine an empty hole which has a function type. This will produce something like λ x → ?, that is, it uses the "pattern is a variable" syntax without curly braces. This is the way lambdas started out (and the way we will study them later, because we’re not going to model pattern matching). But the version PLFA introduces first, with curly braces, allows patterns and is more expressive. Unfortunately, refining will not give us a curly-brace lambda. We have to add the curly braces ourselves, by hand (which is worth doing, as it allows us to case-split on the variable).

8.2 Function composition

As with lambdas, using the function composition operator ∘ may not come naturally at first. But used judiciously, it can improve expressivity. You may find that you only see a composition emerging during interaction, and it needs to be explicitly edited in later.

8.3 Extensionality

Extensionality is an axiom that means "pointwise equality of functions implies propositional equality". It cannot be proved within intuitionistic logic, but it can be added without resulting in inconsistency, and it is sometimes useful. Adding it with a postulate means it cannot be used in computation, only in typechecking. This will not be a problem in what we are doing. But please do not use postulates in your work for this course unless they are specifically permitted (as in this instance).

The simple first example of the use of extensionality given in PLFA is in equating two different definitions of addition (the first is the one from the Naturals chapter, and the second splits on the second argument instead of the first). The proof in the asciicast is slightly different from the one in PLFA. Here is the completed code.

_+′_ : ℕ → ℕ → ℕ -- split on n instead, get different code
m +′ zero = m
m +′ suc n = suc (m +′ n)

same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n
same-app m zero = sym (+-identityʳ m)
same-app m (suc n) rewrite +-suc m n | same-app m n = refl

same : _+′_ ≡ _+_  -- this requires extensionality
same =
 extensionality (λ x → extensionality (λ x₁ → same-app x x₁))

Lambda formation is right-associative, that is, the body of a lambda extends as far to the right as possible. This means that the parentheses in the last line can be removed, but it’s best to leave them in unless they diminish readability.

8.4 Introducing isomorphism

In math classes you may have seen isomorphism between sets A and B as the existence of a one-to-one and onto function from A to B. Pictorially this looks like blobs for A and B, with dots for individual elements, and a line from each dot in A to a dot in B representing the function. "One-to-one" means no two lines from A go to the same dot in B, and "onto" means every dot in B has a line to it.

Intuitionistically, this is best represented by two functions, a "to" function from A to B, and a "from" function from B to A. The "to" function follows lines from A to B, and the "from" function follows lines from B to A. The "one-to-one" and "onto" conditions above are handled by saying that from (to a) = a for all a in A, and to (from b) = b for all b in B.

This totals four pieces of evidence needed to establish isomorphism, and we pack these into an Agda record (which resembles records or structures in other programming languages, except for the possibility of dependent types). This is common practice when representing mathematical structures with multiple components and laws in Agda.

8.5 Isomorphism is an equivalence

You should understand record syntax as presented in PLFA. But we will take a step beyond PLFA and build our records using copatterns. A pattern deconstructs a value; a copattern is used to construct a value. (Usually it is used to construct a value of a coinductive datatype, which is a way of representing "infinite" lists, trees, and other data structures. But we will not be looking at those ideas in this course.)

If we are defining name = ? where the hole has a record type, and we refine the empty hole, we get record syntax as presented in PLFA, with holes for the field values. But if we instead case-split on the empty hole, it offers us a choice of typing in one or more variables to split on, or typing nothing and splitting on the result. If we make the latter choice (split on empty), we get copattern syntax. This consists of an equation for each record field name, followed by an argument which is the name we provided. There will be holes on the right-hand side of each equation. This is not only more readable, but we can proceed to define each left-hand side as we are accustomed to, using case-split to generate multiple equations. This is much easier to demonstrate than to describe, as I believe the asciicasts here show.

I find co-patterns easier to read and work with, but as with equational reasoning, you are free to use record syntax in your own work if you wish.

PLFA shows that isomorphism is an equivalence relation (it is reflexive, symmetric, and transitive) and shows how to set up tabular reasoning, if you want to use that. This forms a more general notion of equality than structural equality, and many results in mathematics are stated "up to isomorphism".

Because we are using copatterns, our proofs look rather different from the ones in PLFA, but at heart they are doing the same things. Here is the completed proof of reflexivity.

≃-refl : ∀ {A : Set}
    -----
  → A ≃ A

to ≃-refl x = x
from ≃-refl x = x
from∘to ≃-refl x = refl
to∘from ≃-refl x = refl

Here is the completed proof of symmetry.

≃-sym : ∀ {A B : Set}
  → A ≃ B
    -----
  → B ≃ A

to (≃-sym A≃B) = from A≃B
from (≃-sym A≃B) = to A≃B
from∘to (≃-sym A≃B) = to∘from A≃B
to∘from (≃-sym A≃B) = from∘to A≃B

The asciicast shows some appearance and removal of lambdas (though it would be fine to leave them in).

Here is the completed proof of transitivity.

≃-trans : ∀ {A B C : Set}
  → A ≃ B
  → B ≃ C
    -----
  → A ≃ C

to (≃-trans A≃B B≃C) = to B≃C ∘ to A≃B
from (≃-trans A≃B B≃C) = from A≃B ∘ from B≃C
from∘to (≃-trans A≃B B≃C) x
  rewrite from∘to B≃C (to A≃B x) = from∘to A≃B x
to∘from (≃-trans A≃B B≃C) x
  rewrite to∘from A≃B (from B≃C x) = to∘from B≃C x

The asciicast shows how one can see where composition can be used, as well as exploration of possible expressions using "deduce" (C-c C-d), which will give the type of what is in the hole, if it can be typed. This is useful for constructing expressions that can be used for rewrites, and making sure they will work before moving them to the right location.

8.6 Embedding

PLFA goes on to describe two weaker notions than isomorphism. An embedding of A into B allows B to be larger (it need not be). In mathematical terms, an embedding is one-to-one, but not onto. Only one line touches every element of B, but an element of A can be touched by several lines. In practical terms, this drops the fourth requirement of an isomorphism, the "to (from b) = b for all b in B". Since several lines can touch an element of A, but only one of them can be used by the "to" function, a round trip from B is not guaranteed to end up at the same place.

An even weaker notion drops the third requirement of an isomorphism, "from (to a) = a for all a in A". What is left is the "to" function from A to B, and the "from" function from B to A. Interpreted logically, these functions show A implies B and B implies A, which means A if and only if ("iff") B, or propositional equivalence. Of course, this works for sets A and B which perhaps cannot be interpreted as logical propositions. PLFA (following the Agda standard library) defines embedding and propositional equivalence using records.

These ideas are used to explore the strength of logical identities in the next chapter, so I have moved the conclusion of the binary notation exercise to the end of the 747Isomorphism file. There I define a notion of a canonical binary embedding (as suggested in the Relations chapter in PLFA), ask you to prove some theorems about it, and then finally show how to collect up the canonical binary embeddings into a set. I ask you to show that set is isomorphic to ℕ.

Of course, both sets are countable, so there are many isomorphisms. But I want one that preserves the arithmetic operations we have defined on both unary and binary numbers, so I want you to use the mappings tob and fromb to help demonstrate the isomorphism. PLFA completes this exercise at the end of the Quantifiers chapter, but I have given you enough structure to let you complete it now.

You will notice that the tree structure of a proof that a number has a canonical binary encoding is almost identical to the encoding itself. This idea will come up in the second half of the course, in a different and more general context.

The idea of a canonical representative for a subset of values is of general importance, but in this case it’s possible to define a datatype whose values are exactly the set of canonical representatives. You might think about how this could be done. The price we pay is that the syntax is likely to be somewhat less natural. We may also pay an additional price if the code for computations and proofs becomes more tedious and less readable.