16
$\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.

Improve this question
$\endgroup$
4
  • 1
    $\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 ♦
    Commented Feb 19, 2022 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$
    – Albert ten Napel
    Commented Feb 19, 2022 at 22:33
  • 3
    $\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$
    – Pierre-Marie Pédrot
    Commented Feb 20, 2022 at 13:37
  • $\begingroup$ You would think bidirectional typechecking could simplify this a bit with one of the terms being a synthesising term. Then R = M could always infer a type for R and check M against it. But this scheme doesn't handle substitution well. Also bidi has its own awkwardness with positive types and stuff. $\endgroup$
    – Ms. Molly Stewart-Gallus
    Commented Oct 23, 2022 at 20:09

2 Answers 2

Reset to default
11
$\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 mark 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.

Improve this answer
$\endgroup$
5
  • 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$
    – Pierre-Marie Pédrot
    Commented Feb 20, 2022 at 14:06
  • $\begingroup$ Andras, can you say exactly what you mean by the "weaker" eta rule for the unit type? What you wrote seems to be the full eta rule, not a weaker eta rule. Note that the eta rule you describe is not supported in Coq. $\endgroup$
    – Jonathan Sterling
    Commented Oct 24, 2022 at 7:47
  • $\begingroup$ @JonathanSterling what I meant is not a specified equation in an equational theory, but instead a conversion checking rule. If we see tt on one side, the sides are convertible. We can't conclude that two neutrals at unit type are convertible, so conversion checking is not even transitive. It's best viewed as an incomplete algorithm for the proper eta rule. It make no sense in a equational theory because there we always assume transitive closure. $\endgroup$
    – András Kovács
    Commented Oct 24, 2022 at 11:46
  • $\begingroup$ BTW, my views have evolved on type-directed conversion since this answer and actually the "elaboration-time relevance computation" is generally incomplete and I wouldn't use it in practice. I'll try to update this answer. $\endgroup$
    – András Kovács
    Commented Oct 24, 2022 at 11:58
  • 3
    $\begingroup$ Oh, I see. I would say this is not a reasonable choice, because it is not optional for conversion to be transitive. Thanks for clarifying! $\endgroup$
    – Jonathan Sterling
    Commented Oct 24, 2022 at 20:03
5
$\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.

Improve this answer
$\endgroup$
1
  • 2
    $\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$
    – András Kovács
    Commented Feb 21, 2022 at 15:42

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