Chapter 4: Quantifiers

Six months on, Hughes’s release bot is still running the same code. On a Monday morning Hughes finds that version 2.4 of the library went out over the weekend at the request of a contributor called Reyes, who has no access of any kind. The log says what happened. None of it is a bug in the usual sense. Remember the arrangement: a request to publish carries its own ticket, a value of type MayPublish, and all the bot does is check the ticket’s type before it acts. I praised this as how access control ought to be done, and I still think so. The declarations were

smith            :: Maintainer
maintainersWrite :: Maintainer -> WriteAccess
writeMayPublish  :: WriteAccess -> MayPublish

so the only way to make a MayPublish was to apply the two policy functions to evidence that somebody is a maintainer. The ticket for Smith’s release of 2.3 was

writeMayPublish (maintainersWrite smith)

and the bot’s job log, which is public, printed it. Reyes copied the ticket out of the log, attached it to a request of his own, and sent it. The bot checked the ticket. It was a MayPublish. It published.

What did the type say? MayPublish is a claim about somebody: they may publish. The evidence inside the ticket was about Smith, and it was good evidence. But the type the bot checked doesn’t say whom it’s about, so to the checker a ticket made for Smith is just a ticket. The checker did refuse Jones, when he wanted to rotate the signing key, because the only evidence in scope for him was a WriteAccess and no function in the policy turns that into a Maintainer. Reyes has no evidence in scope at all. He doesn’t need any. Hand him somebody else’s MayPublish and the compiler has nothing to say. Security people have a name for this, a confused deputy.¹ The bot has authority, the credential it was given is genuine, and it used that credential on behalf of the wrong person, because nothing in the credential says whose it is.

Hughes’s first thought is the right one, and I want to watch it fail. The propositional letters stood for whole claims: $p$ was “Smith is a maintainer”, $r$ was “Smith may publish”. If the trouble is that $r$ doesn’t say Smith, write a letter that does. Let $p_{\mathrm{smith}}$ be “Smith is a maintainer”, $q_{\mathrm{smith}}$ “Smith has write access” and $r_{\mathrm{smith}}$ “Smith may publish”. Do the same for Brown and everyone else, and write the policy once per person:

Now a ticket proves $r_{\mathrm{smith}}$, which isn’t $r_{\mathrm{brown}}$, and Reyes’s replay fails. So far so good. But look at what she’s had to write. MAINTAINERS.md lists thirty-seven people, so the policy is now a hundred and eleven letters and seventy-four implications, every one of them a copy of the same two sentences with a different subscript. The same thing written thirty-seven times is wrong in one of them. Worse, the file changes. Somebody joins on Tuesday. The policy now has seventy-six implications, and the proof Hughes checked on Monday was checked against the wrong one. And there’s a third problem, the one the chapter is about. The clerk who checks a proof by comparing symbols can’t see the subscript. To him $p_{\mathrm{smith}}$ and $r_{\mathrm{smith}}$ are two letters, as unrelated as $p$ and $r$ were. Nothing in his list of shapes says that the “smith” in the one is the “smith” in the other, and $p_{\mathrm{smith}}\to r_{\mathrm{brown}}$ is as well formed as any formula on the page. Hughes has written the name inside the letter, and inside the letter is where the clerk can’t look.

What MAINTAINERS.md actually says is one sentence: every maintainer has write access. Every maintainer, including the one who joins on Tuesday: nothing so far can say that. It keeps coming up. Baker’s runbook said what happens on every payment, and she wrote it for the one on her ticket. A sorting routine promises that every element of its output is at most the next. A sale gives its discount on every day from the start to the end. A bug report said “discount not applied on the last day of the sale”; a patch changed <= to < at both ends; the tests passed; and the discount quietly disappeared from the first day. None of these is a finite list, and the one we tried to write as a finite list has just failed in three ways.

So: how do you say every and some, in a type and in a proof, and what does saying it cost? The language is Frege’s, and in the types the quantifiers turn out to be two things you’ve programmed with for years. Rubbing out the programs, as before, leaves the proof rules, and by then you’ll know the trick well enough to guess them before I give them; I’d like you to try. Pointed at types instead of people, the same quantifier gives generics. The chapter ends where Hughes began, with sentences about things, her policy among them, written down as specifications and proved from. A last section, which you may skip, runs the story the other way round, from a logic to its programs.

4.1 Predicates and quantifiers

The subscript was the right instinct. A letter with a name inside it is two things, a claim with a gap in it and a name, and Hughes’s only mistake was to glue them together where the clerk couldn’t see the join. Pull them apart:

“Smith is a maintainer”, where $\mathsf{Maint}$ is a predicate, a claim with a hole in it, and $\mathsf{smith}$ is a name that fills the hole. Now $\mathsf{Maint}(\mathsf{smith})$ and $\mathsf{Pub}(\mathsf{smith})$ visibly share a part, and the clerk, who compares symbols, can see that they do. The sentence $\mathsf{Maint}(\mathsf{smith})\to \mathsf{Pub}(\mathsf{reyes})$ is still well formed, but it’s now visibly a different sentence from $\mathsf{Maint}(\mathsf{smith})\to \mathsf{Pub}(\mathsf{smith})$, and a policy that said the first would be seen to say it.

This is Frege’s move, and it’s the one his notation of 1879 was built around. Logic before him analysed a sentence into a subject and a predicate, “Smith” and “is a maintainer”, which is the grammar of Latin; Frege analysed it instead into a function and an argument, $\mathsf{Maint}()$ and $\mathsf{smith}$, which is the grammar of mathematics. He thought it the most important thing in the book.² It matters here because a function can take a variable as its argument. The formula $\mathsf{Maint}(x)\to \mathsf{Write}(x)$ is the policy sentence with the name left out, a claim about whoever $x$ is, and it’s one formula, not thirty-seven. On the type side the same move turns Maintainer from a type into a function from people to types, Maintainer smith, Maintainer x, a type with a hole for a name.

Universal and existential quantifiers

A formula with a hole in it isn’t a claim yet, any more than $x+1$ is a number. There are two ways to close the hole, and they’re the two things Hughes was trying to write. The first is to say that the claim holds whoever fills it. For the thirty-seven that would be the conjunction

with one conjunct per person, except that the list won’t be complete on Tuesday and the clerk, as we saw, can’t tell that the conjuncts are alike. So write the conjunct once, hole and all, with a mark in front that says “for every way of filling it”:

That’s for all, and it’s an and with one case for every thing there is, written once with a parameter. The second way to close the hole is to say that something fills it: the review rule, “some maintainer approved this pull request”, is the disjunction

with one disjunct per person, and we write it once:

That’s there is, an or with one case for every thing, and the thing is the tag. Logicians call it the witness. The quantifiers are $\wedge$ and $\vee$ with the list of cases made unbounded, and I’ll say so twice more before the chapter is out. Everything else about them (the programs, the proof rules, the side conditions) is the bill for that.

You’ve met both ideas as a programmer. A test suite checks finitely many inputs: it is the long and with its cases written out, Hughes’s thirty-seven letters again, and it says nothing about input thirty-eight. A function says something about every input, because its body is written once, for a parameter, and has to work for whatever arrives: that is for all, in code. And a single failing test settles “some input breaks this” by exhibiting the input: a witness.

Frege’s language, in the notation everyone now uses, comes in three layers: the symbols; the terms built from them, which name things; and the formulas, which make claims.

Three conventions make formulas readable. First, $\mathrm{\neg }A$ abbreviates $A\to \mathrm{\perp }$. Second, familiar symbols such as $<$ and $+$ are written between their arguments, so that $x+1<y$ is the atomic formula $<(+(x,1),y)$. Third, brackets are left out where nothing is lost: the outermost pair goes; $\wedge$ and $\vee$ bind more tightly than $\to$; the arrow groups to the right; and $\mathrm{\neg }$ and the quantifiers bind most tightly of all. So $\mathrm{\forall }xA\to B$ is $(\mathrm{\forall }xA)\to B$, and a quantifier whose scope is meant to be larger is followed by brackets, as in $\mathrm{\forall }x(A\to B)$. With the conventions in force, the two definitions fit on two lines:

A term names a thing and a formula makes a claim. Keep the two apart, as a parser would by giving them different types. In $x+1<y$ the symbols $1$ and $+$ are a constant and a function symbol, $<$ is a predicate symbol, and $x$ and $y$ are variables; $x+1$ is a term and $x+1<y$ a formula. Writing either where the other belongs would be a type error.

Hughes’s signature, which the chapter uses throughout, has constants for the people and the pull requests, $\mathsf{smith}$, $\mathsf{reyes}$, $\mathsf{brown}$, $\mathsf{pr}$; a function symbol $\mathsf{author}(p)$, the person who opened pull request $p$; and five predicates:

People and pull requests are things of one kind as far as the language goes. A variable ranges over both; the predicates say which is which. So $\mathsf{Maint}(\mathsf{pr})$ is a formula, though not one anybody would assert. (Logics with several sorts of thing, each with its own variables, avoid that at the cost of more bookkeeping.) With these, MAINTAINERS.md is three sentences, which I’ll call ${\mathrm{\Gamma }}_{\mathrm{pol}}$:

The merge rule as the file states it, “a pull request needs a maintainer’s approval, and its author needs write access”, is $\mathrm{\exists }x(\mathsf{Maint}(x)\wedge \mathsf{Appr}(x,p))$ $\wedge \mathsf{Write}(\mathsf{author}(p))$. The term $\mathsf{author}(p)$ names a person without saying who; that is what a function symbol is for. The sentence is the kind a security team writes in English and would rather a machine checked.

Reading quantified sentences

The order of the quantifiers matters, and so does the connective under them. $\mathrm{\forall }x\mathrm{\exists }p\mathsf{Appr}(x,p)$ says that everybody approved some pull request, perhaps each a different one; $\mathrm{\exists }p\mathrm{\forall }x\mathsf{Appr}(x,p)$ says that one pull request was approved by everybody. The symbols are the same and the claims are very different. The file’s first sentence is $\mathrm{\forall }x(\mathsf{Maint}(x)\to \mathsf{Write}(x))$. Written with $\wedge$, as $\mathrm{\forall }x(\mathsf{Maint}(x)\wedge \mathsf{Write}(x))$, it would say that everyone is a maintainer with write access, which no file says. Under $\mathrm{\exists }$ the trap runs the other way. Some maintainer approved is $\mathrm{\exists }x(\mathsf{Maint}(x)\wedge \mathsf{Appr}(x,\mathsf{pr}))$, with $\wedge$; written with $\to$, as $\mathrm{\exists }x(\mathsf{Maint}(x)\to \mathsf{Appr}(x,\mathsf{pr}))$, it could be established by anybody known not to be a maintainer, whether or not they approved anything.

In $\mathrm{\forall }x\mathrm{\exists }y(x<y)$, “every number has a larger one”, every occurrence of a variable is bound, and the formula is a sentence. Free and bound occurrences can also mix, even of one variable. In $\mathrm{\forall }x(x<y)\to \mathrm{\exists }y(x<y)$ the first two occurrences of $x$ are bound and the third is free, and the first $y$ is free and the other two are bound. So this is a formula and not a sentence. Everything in ${\mathrm{\Gamma }}_{\mathrm{pol}}$ is a sentence, which is what makes it a policy rather than a remark about somebody. The merge rule is not: its $p$ is free, and it becomes a claim about a particular pull request only when a term is put in for $p$. That operation needs care.

So $A(t/x)$ puts $t$ in for the free occurrences of $x$, and only those: clause (c) stops at a quantifier on $x$, because every $x$ in its scope is bound. Substitutability is what makes clause (d) safe. If $y$ occurred in $t$ and $x$ occurred free under the $Qy$, pushing $t$ under the quantifier would turn that $y$ into a bound one and change what $t$ means. The term $y$ is not substitutable for $x$ in $\mathrm{\exists }y(x<y)$, for this reason; the terms $z$ and $\mathsf{smith}$ are. When a term isn’t substitutable, rename the bound variable first, to one that occurs nowhere else. Two formulas that differ only in the names of their bound variables are treated as the same formula, so after renaming every term is substitutable. Ignoring the condition produces a bug that the section on side conditions runs all the way to $\mathrm{\perp }$.

4.2 Dependent types

What type should maintainersWrite have? In the bot’s old code it was an arrow from Maintainer to WriteAccess, and we’ve seen what that cost. The policy function has to do two things the old type couldn’t say. It has to work for every person, Tuesday’s included. And it has to say, in its result, which person it was given, so that the ticket it makes for Smith is a ticket for Smith. Frege’s move gives the types. With Maintainer x and WriteAccess x as types with a hole in them, Hughes writes

smith            : Person
smithMaint       : Maintainer smith          -- MAINTAINERS.md
maintainersWrite : (x : Person) -> Maintainer x -> WriteAccess x
writeMayPublish  : (x : Person) -> WriteAccess x -> MayPublish x
publish          : (x : Person) -> MayPublish x -> IO ()

Read the third line slowly, because it’s the only new thing here. The function maintainersWrite takes a person $x$, then evidence that $x$ is a maintainer, and returns evidence that $x$ has write access. The result type mentions the argument. In the old code the name and the evidence were one value, smith :: Maintainer, and that was the bug. Here they’re two: the person, and a separate value smithMaint that’s about him, whose type has the person in it. So the type of the function is an arrow whose right-hand side depends on what went in on the left. None of the type systems so far can write that.³

On the program side, the long and is a record with one field per maintainer: thirty-seven tickets, one for each person. A function from maintainers to tickets holds the same information (hand it Smith and it returns Smith’s field), and when you don’t know how many fields there will be, a function is the only way to write the record down. So a proof of for all is a function from things. The long or is a thirty-seven-way Either: a value with a tag saying which case it is. Here the tags are people, so the value is a pair of a person and evidence about that person. So a proof of there is is a pair of a thing and evidence about it.

One change of notation comes with the types. Logic writes $\mathrm{\forall }$, $\mathrm{\exists }$, $\wedge$ and $\vee$; type theory writes $\mathrm{\Pi }$, $\mathrm{\Sigma }$, $\times$ and $+$ for the same four things. This section uses the type theorist’s letters, the next goes back to the logician’s, and the table at the end of the section lines them up.

A declared variable $x$ is a thing nobody has chosen yet, a parameter, and the four new rules all turn on it. Here is the whole system. The rules for $\to$, $\times$, $+$ and $\mathrm{\perp }$ are the propositional ones, except that a context may now contain declarations.

Read ($\mathrm{\Pi }$E) first, because it’s a function call. You have a program that works for every $x$ and you call it on the $t$ in hand. The type of the result is the body with $t$ put in for $x$: substitution. And $t$ has to be in scope, because a program can mention only declared names. ($\mathrm{\Pi }$I) is what happens when a definition is finished. You typed the body with $x$ declared and nothing said about it, so the program works for every $x$, and you may say so. Proved for an arbitrary $x$, hence for all. ($\mathrm{\Sigma }$I) is the constructor: supply a thing and evidence about it, and out comes a value whose type mentions neither. ($\mathrm{\Sigma }$E) is the pattern match. Open the pair, giving names $x$ and $h$ to the thing and the evidence, and go on to produce something. The something may use $x$ and $h$, but its type may not mention $x$, because $x$ was a name you made up for the duration of the match. Compare the rules for $\times$ and $+$, which are these four with the list of cases cut down to two: a pair with two fixed fields instead of a function from things, a tag from $\{\mathit{Left},\mathit{Right}\}$ instead of a thing. That’s why the letters are $\mathrm{\Pi }$ and $\mathrm{\Sigma }$: a function from things is a product with one factor per thing, and a pair with a tag is a member of a sum with one summand per thing, just as $\sum _{r=1}^n{a}_r$ is a sum with one term for each $r$.

Side conditions and the context

Logic textbooks give the rule for for all a proviso: $x$ must not occur free in any hypothesis. The proviso is needed; without it the rules prove $\mathrm{\perp }$, as an exercise at the end of the chapter shows. Yet ($\mathrm{\Pi }$I) above carries no proviso, because the context already enforces it. In $\mathrm{\Gamma },x$ the variable $x$ is the last thing declared. By the definition of a context, an entry $h:A$ may mention only variables declared before it, so no $h:A$ in $\mathrm{\Gamma }$ can say anything about $x$. If you want to generalise over $x$ while some hypothesis about $x$ is still in force, the rule doesn’t apply, because $x$ isn’t last. You have to discharge every hypothesis that mentions $x$ first, with a $\lambda h$ each, and only then does $x$ come to the top. A context is a stack, and you can only pop $x$ when everything pushed after it has gone.⁴

The one condition the stack can’t enforce is the one written on ($\mathrm{\Sigma }$E). The type $C$ of the result isn’t in the context, so nothing stops it mentioning $x$ unless the rule says so. That is why ($\mathrm{\Sigma }$E) is the only rule with a freshness condition; the conditions on ($\mathrm{\Pi }$E) and ($\mathrm{\Sigma }$I) only ask that $t$ use names already declared. It is also the condition a module system enforces: the part of a language that lets a library hide how it is built.

Now some typings, as sequent-style trees, in which every node is a whole judgement with its context. Hughes’s declarations become one context. The people are constants of the signature, which are always in scope, so they need no declaring, and what is left is the evidence: the three policy functions ($\mathsf{mw}$ and $\mathsf{wp}$ for the two above, and $\mathsf{rel}$ for the review rule), publish, and $\mathsf{sm}$ for smithMaint. With the types written in the predicates of Hughes’s signature, that context is

It stays the same in every tree below; whatever a rule adds to it is written out in full.

Reduction

Running a program means rewriting an introduction met by its own elimination, and the quantifiers add two such steps, with the shapes of $\beta$ and of a case on a tag.

The last two are the new ones. Call a function on a thing and the thing goes in for the parameter. Open a pair that was packed and the thing and the evidence go in for the two names. The table of connectives and types gains two rows:

A function from things, and a pair of a thing and evidence: that’s what Hughes’s bot checks. The first two columns are a dictionary between two notations: $\times$ for $\wedge$, $+$ for $\vee$, $\mathrm{\Pi }$ for $\mathrm{\forall }$ and $\mathrm{\Sigma }$ for $\mathrm{\exists }$, with $\to$ and $\mathrm{\perp }$ the same on both sides.

Types that mention values weren’t invented for Hughes. In 1967 Nicolaas de Bruijn, a mathematician at Eindhoven, set out to have a machine check a whole mathematics textbook, and found that a checker couldn’t do it unless the types were allowed to mention the things the theorems were about. The language he built for the job, Automath, has the rules above, and in 1977 one of his students fed it the whole of Landau’s Foundations of Analysis, every lemma, and it checked.⁶ Most proof assistants built on dependent types count it as an ancestor.

4.3 First-order natural deduction

Twice now a typing has had its programs rubbed out to leave a logic: Hilbert’s proofs under the combinators, and Gentzen’s under $\lambda$, pairs and tags. The Curry–Howard correspondence says this always works. Beside every type system there’s a logic, and the logic is what the typing rules say once the terms are deleted. We’ve just built a type system, so there’s a logic standing beside it.

Before you look for it, one thing changes on the page, and it’s the letters. Peirce, who found the quantifiers at about the same time as Frege and without knowing of him, wrote them as $\mathrm{\Pi }$ and $\mathrm{\Sigma }$, for the reason given in the first section: a long and is a product and a long or a sum (Peirce, 1885). Logic traded his letters for $\mathrm{\forall }$ and $\mathrm{\exists }$, and nearly every logic book since has used those. Type theory took them back: ninety years after Peirce, Martin-Löf wrote the two dependent types as $\mathrm{\Pi }$ and $\mathrm{\Sigma }$, for the reason given with the typing rules above.⁷ So rubbing out the programs means renaming as well as deleting: $\mathrm{\Pi }$ becomes $\mathrm{\forall }$ and $\mathrm{\Sigma }$ becomes $\mathrm{\exists }$, along with $\times$ to $\wedge$ and $+$ to $\vee$. The logic is written in the logic’s letters from here on, and before I write it down I’d like you to find it.

Here’s what’s left, with the declarations kept, since a declaration is a name and not evidence:

with the side conditions carried over unchanged ($t$ in scope in the second and third, $x$ not free in $C$ in the fourth), and here’s where you’ve heard them. Let $x$ be arbitrary: the first. In particular, for $t$: the second. Take $x$ to be $t$: the third. Let $y$ be such a thing; then: the fourth. You’ve used all four as a programmer. A function body, written for its parameter without knowing which value will arrive, is let $x$ be arbitrary. Calling the function on the value in hand is in particular, for $t$. A failing test is take $x$ to be $t$: one input, exhibited, settles “some input breaks this”. And code that receives “some maintainer approved” and works with whoever it was, without being told who, is let $y$ be such a thing.

Gentzen had the four rules in 1934. Natural deduction was first-order from the day it was invented, and the propositional rules are the half of his system without quantifiers.⁸ Here is the whole system as trees.

A tree has no declarations. It records what a context records by computing $\mathrm{OH}$, and it records the stack in the same way. Where the type system said $x$ is the last thing declared, the ($\mathrm{\forall }$I) clause says two things: $y$ is free in no open hypothesis, which is the same fact read off the leaves; and $y$ is not free in $\mathrm{\forall }xA$, which a fresh declaration guarantees. The ($\mathrm{\exists }$E) clause states the one condition the type system had to write, $y$ not free in $C$, and two that the context gave for free: $y$ is fresh for $\mathrm{\exists }xA$ and for the other open hypotheses.

Set the two clauses beside the turnstile, writing $\mathrm{\Delta }$ for the open hypotheses of the tree above the bar, and the correspondence is visible bar for bar. On the left is the tree; on the right, what it witnesses:

with $y$ free in no formula of $\mathrm{\Delta }$, nor in $\mathrm{\forall }xA$; and

with $y$ free in none of $C$, $\mathrm{\exists }xA$ and the formulas of ${\mathrm{\Delta }}_1$. Read on the right, the conditions are the erased rules with the declaration turned into a test: where the context declared $y$ last, the turnstile asks that nothing to the left of it mention $y$.

Erasure treats the two kinds of variable differently, and that is the difference between quantifiers and connectives. Erasing $\lambda h.M$ deletes $h$, since a variable standing for evidence has nothing to say once the evidence is gone. Erasing $\lambda x.M$ doesn’t delete $x$, though, because a declared thing isn’t evidence but a name, and the formula $\mathrm{\forall }xA$ still needs it. So a logic keeps its variables when it loses its programs, and derivations with quantifiers have variables in them, where propositional derivations had none.

Normalisation and consistency

The theorems about running programs carry over, each with two more cases. A lemma proved for an arbitrary $x$ and then used at a particular $t$ is a detour, ($\mathrm{\forall }$I) met by ($\mathrm{\forall }$E), and it is removed by the step $(\lambda x.M)t⇝M(t/x)$. A witness packed and at once unpacked is ($\mathrm{\exists }$I) met by ($\mathrm{\exists }$E), and it is removed by the step for $\mathbf{let}$.

In words: running a program never changes its type.

$\mathrm{\Sigma }$ breaks the count as $+$ does, and for the same reason: $\mathrm{\exists }$ is an $\vee$ whose tags are things. A step on a $\mathbf{let}$ puts its body $N$ where the $\mathbf{let}$ stood, and $N$ has the result type $C$, which can have any degree at all. If the $\mathbf{let}$ stood under an elimination, the new redex can have a larger degree than the one removed. Prawitz’s proof covers every connective and both quantifiers, with the permutative conversions added; Tait’s method of computable terms extends to the quantifiers too. For terms with $+$ or $\mathrm{\Sigma }$ we take the theorem on trust.

The last three follow from the first three as Theorem 3.15 did. No introduction form has type $\mathrm{\perp }$ or an atomic type, so there is no closed normal term of either. A closed normal term of type $A+B$ is $\mathit{Left}M$ or $\mathit{Right}M$, and its tag says which disjunct holds. A closed normal term of type $\mathrm{\Sigma }xA$ is $⟨t,M⟩$ with $⊢M:A(t/x)$, and its first half is the witness.⁹

4.4 Side conditions

Three things can go wrong with a quantifier rule, and each of them is a bug you’ve met in a program. The examples of the section on dependent types refused two of them already; here all three are set side by side, in both notations. You remember a side condition once you’ve watched its absence prove everything, so the third bug is run all the way to $\mathrm{\perp }$ below; one of the exercises does the same for the first.

Generalising over a fixed variable

Suppose Hughes’s bot is handling a request from some user $u$, and the hypothesis in force is $\mathsf{Maint}(u)$: this requester is a maintainer. One application of ($\mathrm{\forall }$I) would give $\mathrm{\forall }x\mathsf{Maint}(x)$, everyone is a maintainer, from which, with the policy, everyone may publish. Both notations refuse it, and they refuse it for one reason. In the type system, $u$ was declared before $h:\mathsf{Maint}(u)$, so it isn’t on top of the stack and ($\mathrm{\Pi }$I) doesn’t apply. In a tree, $u$ is free in the open hypothesis $\mathsf{Maint}(u)$, and the ($\mathrm{\forall }$I) clause says no. Discharge the hypothesis first, by ($\to$I), and generalising becomes legal. But what you’ve generalised then is $\mathsf{Maint}(u)\to \dots$, and that is harmless.

Of the two, the tree says it more sharply. The context asks that $y$ be free in no hypothesis available; the tree asks that $y$ be free in no hypothesis used. A hypothesis about $y$ lying in the context untouched blocks ($\mathrm{\Pi }$I), but it doesn’t block ($\mathrm{\forall }$I), since it isn’t open. Nothing provable changes, by the Curry–Howard theorem. But the tree states the condition that matters and nothing more, and that is one reason proof theory is written in trees.

Escaping witnesses

“Some maintainer approved the pull request; call them $y$; so $y$ is a maintainer.” We saw the type system refuse this in Example 4.11, with the result type $\mathsf{Maint}(y)$, and the tree refuses it by the first condition of the ($\mathrm{\exists }$E) clause, that $y$ not be free in the conclusion. The other two conditions rule out two more ways of cheating. You might choose as the fresh name a variable that $\mathrm{\exists }xA$ already mentions, or one that some other open hypothesis already says something about. Either way “call them $y$” would be naming a thing that was already in play. Together the three say that you may use the thing and may not learn which thing it is, which is what a module boundary says.

Variable capture

The third bug is the reason ($\mathrm{\forall }$E) asks that $t$ be substitutable. Drop that condition and the system proves $\mathrm{\perp }$ from two hypotheses any programmer would accept of the natural numbers:

“every number has a larger one” and “no number is less than itself”. Take $t$ to be the variable $y$, which is not substitutable for $x$ in $\mathrm{\exists }y(x<y)$, since it would land under the $\mathrm{\exists }y$, and pretend ($\mathrm{\forall }$E) didn’t care. The left-hand bar below is that instance, $t:=y$, and it’s the illegal one.

Four bars, and $\mathrm{OH}$ is the two harmless hypotheses, so the tree would witness $\mathrm{\forall }x\mathrm{\exists }y(x<y),\mathrm{\forall }x\mathrm{\neg }(x<x)⊢\mathrm{\perp }$. The system has proved $\mathrm{\perp }$ from two facts about the natural numbers. The only thing that let it happen is the left-hand bar. (The ($\mathrm{\exists }$E) at the root is legal: $z$ is free in none of $\mathrm{\perp }$, $\mathrm{\exists }y(y<y)$ and $\mathrm{\forall }x\mathrm{\neg }(x<x)$.) You can see what went wrong in the formulas. The $y$ we substituted meant “some given number”. On landing under $\mathrm{\exists }y$ it came to mean “whichever $y$ the quantifier picks”. So $\mathrm{\exists }y(y<y)$ says that some number is less than itself, which the hypothesis never said. With the condition in force the left-hand bar isn’t available. The fix is to rename first: the hypothesis is equally well written $\mathrm{\forall }x\mathrm{\exists }z(x<z)$, its legal instance at $y$ is $\mathrm{\exists }z(y<z)$, and nothing follows from that but what should.

A compiler or interpreter doesn’t substitute text when it calls a function; it carries the argument’s value in an environment. Macros and refactoring tools do substitute text, and that is where you’ve met the bug. The logic side has been known for a century, and every textbook states the condition. What the correspondence adds is that it’s the same condition.

4.5 Generics

The quantifier so far ranges over things. Let it range over types instead and you get something you’ve been writing for years. A type variable $a$ stands for a type nobody has chosen yet, and $\mathrm{\Pi }aA$ is the type of a program that works for every type $a$. Such a program is a type abstraction $\mathrm{\Lambda }a.M$: it takes a type and returns a program. You use it by an instantiation $M[B]$, which hands it a type $B$. The rules are ($\mathrm{\Pi }$I) and ($\mathrm{\Pi }$E) of dependent types with types in the place of things,

where $B$ may mention only type variables declared in $\mathrm{\Gamma }$. The context is the same stack, and running is one more step, $(\mathrm{\Lambda }a.M)[B]⇝M(B/a)$.

The type of length is [a] -> Int, and the a in it is a parameter, a type nobody has chosen yet. Haskell leaves the quantifier out, and writes it forall only when asked. Written in, it reads

so length is a function that works for every element type at once. Without a way to say for every you’d have three options. The first is one copy per element type,

which is Hughes’s thirty-seven letters again. The second is to give it the type [Object] -> Int and cast on the way in and out. Java made people do that until 2004, and a wrong cast is caught only when the program runs. The third is to turn the checker off for that part of the program. With the quantifier you write the code once and check it once, for every type, and that’s why map, filter, sort and every container you’ve used have one in their types. The logic got there first: a generic function is a proof of a schema, written once.

The side condition on ($\mathrm{\forall }$I) turns up as an error message. Try

f :: a -> b
f x = x

and GHC answers couldn’t match expected type b with actual type a, adding that a is a rigid type variable bound by the signature. Here’s what happened in the stack. The signature declared $a$ and $b$ and promised a program that works for both separately. The body can only be typed if $a$ and $b$ are the same, which means a hypothesis about $a$ is still in force when the checker reaches the ($\mathrm{\Pi }$I) that would pop it. Rigid is the compiler’s word for declared and not last, a variable the context has fixed and you may not generalise over.

{-# LANGUAGE ExistentialQuantification #-}
data Counter = forall a. MkCounter a (a -> a) (a -> Int)

intCounter  = MkCounter (0 :: Int)   (+1)    id
listCounter = MkCounter ([] :: [()]) (():)   length

tick3 :: Counter -> Int
tick3 (MkCounter s step out) = out (step (step (step s)))

The generic quantifier, side conditions and all, has been at work every time the compiler has read a definition with a type variable in it. The domain was types rather than people, though, which is why the type never amounted to a specification. Specifications need the first-order quantifier, over things.

4.6 Specifications

Read the consistency theorem with names in the language. The logic proves no atomic sentence: neither $\mathsf{Maint}(\mathsf{smith})$ nor $\mathsf{Pub}(\mathsf{reyes})$ nor $2<3$. Whatever it proves outright has a connective or a quantifier on the outside and is about how claims relate. Every fact about a particular person, element or day has to come from the hypotheses. A specification is a set of sentences taken as hypotheses, and what we prove, we prove from it. Three specifications, then, in increasing order of interest.

sort(lt, xs):
    out = []
    for x in xs:
        i = 0
        while i < length(out) and lt(out[i], x):
            i = i + 1
        insert x into out at position i
    return out