plfa
Possibly Sparse Description on `Set` and Predicates
Dear Agda-Team,
First of all, thanks for this awesome book and language! The book is a pleasure to read and doing the exercise within the book itself works like a charm and is a lot of fun. 😃
When facing Chapter 4 (Equality) of Part 1, I had trouble following the use and definition of predicates. In particular, the definition of substitution
subst : ∀ {A : Set} {x y : A} (P : A → Set)
→ x ≡ y
---------
→ P x → P y
subst P refl px = px
is the first occurence of predicates as parameters (of type A → Set). This is also the first time Set is used as a type. Previously, Set was used and introduced only in terms of T : Set, as a way to describe that T is a type in Agda (in Chapter 1 (Naturals) of Part 1). So it was unclear to me, how to interpret the use of Set within a function signature.
Moreover, the signature P : A → Set collided with my usual understanding of predicates as a function A → Bool. While the second signature A → Bool models predicates as functions, the first one A → Set models predicates as (dependent) types. This mental hop was a challenge to me as an apprentice of dependent types and is not explained or suggested within the chapter. (I am also unsure whether I fully understood it by now and got it right here.)
Potentially, it would have helped me as a reader of the book to
- have an explicit explanation about the meaning of
Set. I suppose it is the type of all types which is itself a type, giving rise to levels mentioned first in the paragraph onLeibniz equality? IsSetthe type denoted by U in The Little Typer? While there might be an explanation ofSetin future chapters, this was the point where I was lost (at first). - have explanations or guidance towards the mental hop of expressing predicates as types instead of functions. I think
EvenandOddare good examples here, which are predicates we already saw in an earlier chapter. Another option could be having an exercise for navigating the reader towards making this observation (in case they are not too familiar with dependent types yet).
This is just a suggestion and every reader might come with a different background of course.
Kind regards, Paul
Thank you for the feedback. It is helpful to understand what readers find difficult.
However, your claim that subst is the first use of Set other than T : Set is incorrect. Did you read Chapter 3 (Relations) before reading Chapter 4 (Equality)? It has many examples: data ≤ : ℕ → ℕ → Set data < : ℕ → ℕ → Set data even : ℕ → Set data odd : ℕ → Set If you have further comments, taking into account the above, I'd be happy to see them.
Thank you very much for the fast response. I've read chapter 3 before 4 but with a few days inbetween. I see and agree that my claim was wrong.
Yet, my first issue remains. While the examples in chapter 3 use Set within another syntax (explained by the Total example), it remained unclear to me what Set itself is. In chapter 3, I've read signatures such as data even : ℕ → Set as: "something that when given a ℕ produces a value of some type". It was unclear to me, that given an ℕ, even yields a type (which is what Set denotes) but not a value of some unkown thing called Set. If I am not mistaken, it is not before the section on Universe Polymorphism in chapter 4 that Set is (implicitly) defined as "not every type belongs to Set" implying that Set is a type denoting all types except for itself. I guess this is the key information I was missing (especially when reading the section on Leibniz equality).
Regarding my second issue, I suppose when seeing subst in chapter 4, it should have been clear to me that even and odd from chapter 3 are predicates and that their signature indeed matched A → Set with A being ℕ. Maybe, a short hint pointing back to these examples from chapter 3 would have helped me.
@pmbittner I'd be happy to merge a PR adding a sentence pointing back to the examples from chapter 3 (preferably the even and odd predicates, as the inequalities would need to be partially applied to yield unary predicates).
