12
$\begingroup$

What are the tradeoffs between untyped and type-directed conversion in dependent type theory, and is there any consensus on what's "better"?

Background

Generally speaking, in dependent type theory the conversion rule can depend either on an untyped equality judgment ($t = u$, typically built over untyped reduction) or a typed equality judgment ($\Gamma ⊨ t = u : T$).

In https://proofassistants.stackexchange.com/a/272/393 we read that:

From my perspective, the move from untyped to typed conversion is simply an example of technology improving over time.

and http://www2.tcs.ifi.lmu.de/~abel/lics07.pdf has some arguments on why typed conversion is theoretically better.

OTOH, a comment by @ionchy wonders how strong the consensus is.

For instance, because of performance concerns Coq sticks to untyped reduction (plus eta-expansion, and even that is syntax-directed): that avoids reducing types, but prevents adding judgmental eta for the unit type.

$\endgroup$
3
  • $\begingroup$ Not enough to be an answer, but this paper about normalization by evaluation states that "Untyped terms allow us to separate concerns: we can first specify operations on untyped terms and then prove typing properties of these operations. Typed terms do not give us this flexibility; everything has to be well-typed from the beginning." And it is de facto more easy to deal with untyped conversion. $\endgroup$
    – Trebor
    Feb 19 at 14:47
  • $\begingroup$ You can still have a weaker eta for unit with untyped conversion (unit ~ t, for any t). That's enough to prove induction. $\endgroup$ Feb 19 at 22:33
  • 2
    $\begingroup$ Eta-expansion in Coq is not type-directed. Rather, it morally exploits a property of invertibility of typing for neutral terms. For instance, when asked t ≅ fun (x : A) => u it will check t x ≅ u because the lhs must have a product type. At no point we have access to the actual type of those terms. $\endgroup$ Feb 20 at 13:37

2 Answers 2

6
$\begingroup$

From the perspective of implementation of conversion checking, it really depends on the specific setting.

For vanilla intuitionistic type theories without more exotic features (like cubical TT, observational TT or fancy rewrite rules), untyped conversion is generally quite favorable. Here, the only standard feature that untyped conversion does not easily support, is the full $\eta$-rule for the unit type. However, it still supports a weaker $\eta$-rule, which says that $t = \mathsf{tt}$ for all $t : \mathsf{unit}$. This might look ugly from the theoretical point of view, but it still covers many practical use cases, and we can simplify the implementation a lot compared to full type tracking.

It's also possible to shift work from the conversion checker to the elaborator: we can track whether types are judgmentally proof-irrelevant during elaboration, and marks irrelevant terms as such. In this case, the conversion checker doesn't have to track types. AFAIK this is related to how SProp is implemented in Coq. From the perspective of conversion checking performance, this is clearly superior. However, it can complicate elaboration in annoying ways. If we have metavariables and/or postponed constraints, we might not learn about the proof-relevance of a given term until well after it is elaborated.

For deciding $\eta$ for $\Sigma$ and $\Pi$, which is the great majority of practical cases, it makes little sense to do type-directed $\eta$-expansion, because the syntax-directed version is already complete, and much more efficient. For example, Agda has typed conversion, but it still uses syntax-directed expansion for records because of performance concerns.

If we allow typed custom computation rules, like the custom $\eta$-like rules in Andromeda, then typed conversion is a must. If we move to cubical type theories, then I believe that typed conversion is not essential per se, but it can be convenient in the implementation.

If we add strict Prop, that can be viewed as a generalization of full $\eta$ for unit types, and once again we have the choice of distributing work between conversion checking and elaboration. I personally experimented with conversion checking which is universe-directed but not type-directed. This seems to work well for strict Prop: we track whether a type is in a Prop universe or in a proof-relevant Type universe, and we can shortcut conversion when we are comparing proof-irrelevant things.

$\endgroup$
1
  • 1
    $\begingroup$ Strict propositions in Coq are still tracked by the kernel as a sort annotation on variables. Morally, a binding is of the form x : A ∈ s where s is the sort quality of A, namely relevant or irrelevant in the current implementation. The absence of SProp ⊆ Type implicit cumulativity is critical for this to work. So it's another kind of trade-off. $\endgroup$ Feb 20 at 14:06
3
$\begingroup$

Typed conversion makes establishing metatheoretical properties of the syntax overwhelmingly easier, especially if you want to prove things like decidability of typechecking.

Basically, when showing decidability, the natural thing to do is to give one type system which is the specification, and a second one which is the algorithm, and establish their soundness and completeness with respect to one another. This requires two logical relations (one for soundness, one for completeness), but even showing the well-foundedness of the definition of a logical relation for dependent types is a very long proof. This is really unpleasant, since the two proofs are actually almost, but not quite, the same.

As far as I know, the state-of-the-art approach is Abel, Öhman, and Vezzosi's Decidability of conversion for type theory in type theory, which very nicely factors the proof so you only have to do it once. But to do so, you have to work with an abstraction of judgemental equality they call "generic equality", and that is a typed equality.

$\endgroup$
1
  • 1
    $\begingroup$ I'd say the state of the art in terms of mathematical convenience is NbE + HOAS, like in "synthetic Tait computability". Although that's not feasible to fully machine-check now, because it uses switching between internal and external languages, which is basically not possible in any current proof assistant. $\endgroup$ Feb 21 at 15:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.