9
$\begingroup$

I am wondering whether a rule like the following is consistent with decidable conversion and type-checking for dependent type theory:

$$ \frac{f\, g : (x:\mathsf{bool}) \to C~x\quad f~\mathsf{tt} \equiv g~\mathsf{tt} \quad f~\mathsf{ff} \equiv g~\mathsf{ff}}{f\equiv g} $$

That is, if two functions with domain $\mathsf{bool}$ agree definitionally on $\mathsf{tt}$ and $\mathsf{ff}$, then they are convertible. An analogous rule for functions on general inductive types like $\mathbb{N}$ is certainly bad, but it seems not too ridiculous to me to wonder whether the special case of $\mathsf{bool}$ (and other non-recursive inductive types, like sum-types and enumerated types) might be possible.

One thing that makes me somewhat hopeful is that this rule would make $(x:\mathsf{bool}) \to C~x$ behave very much like $C~\mathsf{tt} \times C~\mathsf{ff}$, and indeed be definitionally isomorphic to it if the latter also has an $\eta$-rule. Since such a rule for products is possible, I thought maybe it could also be possible for the function-type. And implementation-wise, I could imagine a bidirectional conversion-checking algorithm noticing when the type is a function with domain $\mathsf{bool}$ and deciding to apply this rule instead of the ordinary $\eta$-rule for functions.

$\endgroup$

1 Answer 1

9
$\begingroup$

If we have $\eta$ for functions and also your pointwise conversion rule, that implies the full $\eta$ rule for the (finite) domain type. When checking conversion of arbitrary $t,u$, we can abstract over an arbitrary $\mathsf{bool}$ subterm $v$ to get an equivalent conversion problem

$$(\lambda~(x:\mathsf{bool}).~ t')~v\equiv(\lambda~(x:\mathsf{bool}).~ u')~v$$

For instance

$$\mathsf{if}~b~\mathsf{then}~t~\mathsf{else}~t \equiv (\lambda~x.~\mathsf{if}~x~\mathsf{then}~t~\mathsf{else}~t)~b \equiv (\lambda~x.t)~b \equiv t$$

The full $\eta$-rules for finite sums are rather complicated and expensive to check. There's a reference for STLC with finite sums and products. However, I do not know any reference for deciding finite sum $\eta$ in richer systems.

I expect that $\eta$ for non-empty finite sums remains decidable even in the fully dependent type theories. $\eta$ for the empty type is decidable only when consistency of typing contexts is decidable.

More specifically for our current case, let's assume that $\bot \to A$ is definitionally irrelevant. Then, if we have $p : \bot$ and $t,~u : A$, then

$$t \equiv (\lambda~x.~t)~p \equiv (\lambda~x.~u)~p \equiv u$$

Therefore, if $\bot$ is provable then all terms are convertible. This is undecidable for the usual $\bot$ in type theories, but it might be decidable in other settings. For example, in ABCFHL cubical type theory all judgments hold when the empty cofibration is implied by the context. This is still decidable because cofibrations are decidable. This is implemented in cooltt.

Alternatively, we can drop the function $\eta$ rule. Then, we recover the finite product types as $(x : A) \to C~x$ for finite $A$, and everything is decidable. I don't think this configuration is useful for anything though.

$\endgroup$
7
  • 2
    $\begingroup$ Thanks! Can you say anything about why you expect $\eta$ for non-empty finite sums to still be decidable in dependent type theories? $\endgroup$ Commented Dec 10, 2022 at 16:02
  • $\begingroup$ I haven't looked deeply into this topic so I only have pretty naive intuition. My naive algorithm would be something like: for comparing $\beta$-normal $t$ and $u$, we pick a $\mathsf{Bool}$-typed neutral subterm, in either $t$ or $u$, then rewrite all occurrences of that subterm to $\mathsf{true}$ and $\mathsf{false}$ to get two sub-problems. We repeat until there are no neutral $\mathsf{Bool}$ subterms, then check conversion. I'd be glad to be told by experts if this doesn't work or is incomplete, though. $\endgroup$ Commented Dec 10, 2022 at 18:32
  • $\begingroup$ @AndrásKovács in order to be complete, I guess you would need to keep track of the true/false assignements for the boolean subterms and be able to check that your assignment is valid (in the sense that you didn't assign true and false to two subterms that turn up to be convertible, possibly up to some previous assignments). $\endgroup$ Commented Dec 12, 2022 at 14:24
  • $\begingroup$ @kyodralliam That's a good point. What about this refinement: at each step I pick a neutral Bool subterm which doesn't have any neutral Bool subterms. I think that this would ensure that assignments stay compatible. $\endgroup$ Commented Dec 12, 2022 at 14:56
  • 1
    $\begingroup$ Martin Baillon and Pierre-Marie Pédrot provided me with the following example of a "tricky" conversion problem: α : ℕ → 𝔹 ⊢ match α 42 as b return ∀ (n : ℕ), b = α n → ℕ with | true => 5 | false => 5 end 42 refl ≡ 5 : ℕ In that case, brutally rewriting the neutral subterm α 42 with true and false yield terms that are not well-typed (because you lose the fact that refl has the adequate type unless you track the assignement in the conversion) $\endgroup$ Commented Dec 14, 2022 at 13:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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