About a Proof Pearl: A Purported Solution to
a PoplMark Challenge Problem that Is Not One

Challenge 1A relates solely to the type language that includes subtyping but does not encompass record types. The two syntactic entities that are relevant to describing the subtyping relation in this context are types and type environments. Expressions in these categories are given by the following grammar rules:

The token $X$ represents variables in these rules. A type of the form $\forall X\,\mbox{\tt<\!:}\,T_{1}.T_{2}$ represents a binding of $X$ over the type $T_{2}$. Type environments bind variables that occur in types within their scope and they identify subtyping constraints for the variables so bound. Variables bound by an environment are assumed to be named uniquely and the subtyping rules implicitly permit the renaming of bound variables in types to ensure that this property holds. The presentation in [1] uses the same symbol for both <​: and $\mbox{\tt<\!:\!}_{b}$. We avoid this overloading here to highlight issues that arise from the confusion of the two in [3].

The subtyping relation that is of interest is written as $\Gamma\vdash S\,\mbox{\tt<\!:}\,T$, to be read as “$S$ is a subtype of $T$ relative to the type environment $\Gamma$.” This relation is determined by the rules in Figure 1. The SA-Top rule has the requirement that $S$ must be well-scoped with respect to $\Gamma$, i.e. all its free variables must be bound in $\Gamma$. Similarly, the SA-Refl-TVar rule has the proviso that the variable $X$ must be bound in $\Gamma$.¹¹1It can be shown that these assumptions suffice to ensure that $\Gamma\vdash U\,\mbox{\tt<\!:}\,V$ is derivable only for types $U$ and $V$ that are well-scoped. It may be desirable to impose well-scoping requirements on $\Gamma$ as well, in which case the order in which bindings appear in it will be important. We discuss this observation further later in the note. This collection of rules has an algorithmic flavor in that it determines a process for checking a purported subtyping relation that is syntax-directed. The form of the SA-Trans-TVar rule is crucial to this property. Note that because of the form of this rule it is not automatically the case that $\Gamma\vdash X\,\mbox{\tt<\!:}\,U$ is derivable if $X\,\mbox{\tt<\!:\!}_{b}\,U$ appears in $\Gamma$. However, this turns out to be the case if $U$ is well-scoped with respect to $\Gamma$ because then $\Gamma\vdash U\,\mbox{\tt<\!:}\,U$ is derivable.

Challenge 1A consists of providing a mechanized proof of the fact that the subtyping relation defined by the rules in Figure 1 is transitive. Specifically, a proof is to be provided for the following proposition within a chosen system for formal reasoning:

The difficulty in showing this property, and the reason why it is interesting as a challenge problem, is that it must be proved simultaneously with the following property that is called narrowing:

In the standard informal proof, the properties are established by an induction on the structure of $Q$, with the first property being shown first and then used in showing the second. The proof of the first property requires an additional induction on the derivation of $\Gamma\vdash S\,\mbox{\tt<\!:}\,Q$ and that of the second property similarly requires an additional induction on the derivation of $\Gamma_{1},X\,\mbox{\tt<\!:\!}_{b}\,Q,\Gamma_{2}\vdash M\,\mbox{\tt<\!:}\,N$.

While the description of the challenge allows for small changes to the subtyping rules, such as those needed to accommodate a higher-order abstract syntax style of formalization, it places a requirement that these such changes should result in an “obviously equivalent” system. As an example, mention is made in [1] of a declarative presentation of subtyping that explicitly include rules for reflexivity and transitivity. Such a presentation obviates a proof of transitivity of subtyping and thus constitutes another “nice example how the original problem specification influences the proofs about it” in the sense hinted at at the end of Section 2 in [3]. However, it also illustrates fairly starkly how changing the “problem specification” in such ways is not acceptable because it undermines the intended challenge.

The claimed solution to the challenge in [3] uses an encoding of the subtyping rules in LF that is based on a higher-order abstract syntax style. However, it is unnecessary to get into the details of this encoding to illuminate the difficulty with the claims therein. For simplicity of presentation, we will adhere to a presentation style that is close to that of the original description of the challenge. We note that this style is also used at the outset in [3].

The presentation of subtyping in [3] begins by confusing subtyping in bindings in type environments with subtyping judgements. In the description of the challenge in this note, we have highlighted the distinction between the two by deliberately using the symbol $\mbox{\tt<\!:\!}_{b}$ for one and <​: for the other. In keeping with the presentation in [1], the symbol <​: is used in [3] for both.²²2The symbol that is actually used in [3] is $\leq$ but we will assume it to be <​: here to ensure consistency with the earlier discussion. However, unlike in [1] where a distinction is maintained despite the overloading of notation, the two notions are conflated in [3] by the inclusion of the following rule:

A further distinction between the subtyping rules in the original presentation and the one in [3] is that the latter builds in transitivity with respect to variable subtyping directly by replacing the SA-Trans-TVar rule with the following:

The changes to the formulation of subtyping that are described above are substantial and do not satisfy the criterion of obvious equivalence required by the challenge. In particular, they considerably simplify the informal proof of transitivity of subtyping. Unlike with the original presentation of subtyping, the narrowing lemma can be proved independently of the transitivity property. Further, Prop 1, the transitivity property, can be proved by an induction only on $Q$; the additional induction on the derivation of $\Gamma\vdash S\,\mbox{\tt<\!:}\,Q$ is not needed.³³3The development in [3] continues to use an induction on both but the second induction can be avoided.

In the above discussion, we have assumed that the narrowing lemma still needs to be proved. The claim in [3] is that this lemma is obtained for free. A closer look at the development shows that this “simplification” is actually the result of assuming the validity of a further rule related to subtyping that has the following form:

Observe that the sensibility of this rule depends on the conflation of subtyping in bindings in type environments with the subtyping judgement. While the narrowing lemma is an easy consequence of this rule in a situation where the SA-Tr-TVar rule is also present, the assumption of such a rule represents a significant deviation from the formulation of subtyping in Challenge 1A. We note that this rule can be shown to be admissible in the typing calculus of interest, but doing this requires an argument that is as complicated as the direct proof of narrowing. This observation raises in a different way the question of what it means to get something for free.

Typing calculi often attribute a significance to the order of bindings in contexts or type environments. In the discussions here, this sensitivity is manifest specifically in the statement of Prop 2. While order is important for well-scoping of type environments, the proofs of transitivity of subtyping and narrowing are not dependent on order. Moreover, ignoring order has the effect of simplifying the formalization of the arguments. It is possible to realize such an effect in a system like Abella [2], which treats contexts by default as multisets, by not imposing a well-scoping constraint initially on type environments. Once the desired properties have been proved when type environments have this less constrained form, it is easy to show that they must also hold when type environments are required to be well-scoped.