⊥ is Recomputable

[jamesmckinna]

The current definition of Data.Empty, and its derivative sub-module Data.Empty.Irrelevant are the basis of the current (re-)definition of Relation.Nullary.Negation and ... everything else involving ⊥ and negation ¬ A etc.

What's at present missing, and responsible for the artificial distinction between

• Data.Empty.Irrelevant.⊥-elim : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
• Data.Empty.⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever

is the equivalence of .⊥ and ⊥... ie that ⊥ is Recomputable.

NB Recomputable seems to be the modern-dress version of the very old idea that certain types (negated formulae, among others) have no computational content, that is, we can't make essential use (eg by pattern-matching) of their inhabitants in order to define/prove... other things.

Well, the use of pattern-matching against the empty pattern () ensures that ⊥ itself is Recomputable:

Recomputable : ∀ {a} (A : Set a) → Set a
Recomputable A = .A → A

-- ⊥ is Recomputable

⊥-recompute : Recomputable ⊥
⊥-recompute ()

... and this is already provable in the current formulation of the library... and hence that the above two elimination principles are interderivable (so: do we need both, or does one suffice? UPDATED: does the asymmetry in the use of irrelevant marks in types between assumptions and conclusions mean that this cannot precisely be the case?). See branch, with no (seemingly!?) wider knock-on consequences for the rest of the library.

So: we should reconcile these things, and their many consequences; esp. wrt proving Recomputable for all kinds of types, notably product types (below), negated types, decidable types, ... in general at least (conjecture!?) the (hereditarily) Harrop formulas, and more generally, any 'Glivenko class' of formulas (ditto.).

Question/Issue: Why haven't we done this before/already? cf. #645 / #652 / #762

[jamesmckinna]

Further evidence towards the identification of Recomputable and Harrop:

Recomputable : ∀ {a} (A : Set a) → Set a
Recomputable A = .A → A

_×-recompute_ : Recomputable A → Recomputable B → Recomputable (A × B)
(rA ×-recompute rB) p = rA (p .proj₁) , rB (p .proj₂)
-- NB this definition fails: (rA ×-recompute rB) (a , b) = rA a , rB b
-- Cannot pattern match against irrelevant argument of type A × B
-- when checking that the pattern a , b has type A × B

→-recompute : Recomputable B → Recomputable (A → B)
→-recompute rB f a = rB (f a)

∀-recompute : (B : A → Set b) → ((x : A) → Recomputable (B x)) → Recomputable ((x : A) → B x)
∀-recompute B rB f a = rB a (f a)

Suggest that this become a focus of effort on reconciling (the) 'classical' fragment(s) of type theory with the ambient intuitionistic.

Or has this already been done somewhere (else) before?
Have now asked on the main Agda Zulip

Nisse's answer there has me needing to think a bit harder. Specifically, I don't think we can make a simple-minded identification of Recomputable and Harrop; rather they have the same/similar closure properties. But for any collection of 'base' types, the Harrop/negative fragment defined over them will satisfy all sorts of things (Recomputable, Decidable, Stable, ...) depending on the corresponding conditions on those base types. So this seems really to be more about 'induction over the negative fragment'.

[JacquesCarette]

This is definitely about Agda's handling of 'irrelevant' (which I've run into quite a bit too). A discussion about it should happen on the Agda side (either Zulip or git issues) as that's where the experts are for that.

[jamesmckinna]

But the main content of the issue: namely reconciling 'irrelevant' ⊥-elim and ⊥-elim, still stands. So at some point I'll turn the branch into a small(er)-scale PR, leaving the 'other' issue: what/where/how should we define Recomputable, and refactor the library to make use of this definition? So... further comments on the issue welcome towards such an eventual 'design'.

[jamesmckinna]

Proposal: replace the type of ⊥-elim with that of ⊥-elim-irr:

⊥-elim : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
⊥-elim ()

Would this constitute a breaking change?

[gallais]

Would this constitute a breaking change?

Given that we don't have subtyping for functions whose domain is irrelevant (the following is rejected:

app : {A B : Set} → (.A → B) → (A → B)
app f = f

) then I'd say yes. It could break strange code that uses ⊥-elim partially applied.

[JacquesCarette]

Good point: I think that the proposal goes one step too far. Indeed it would only break rather strange code, but the debugging pain would be quite something!

[jamesmckinna]

Thanks to both. Indeed, errors arising from (some) partial applications of contradiction was one reason I introduced its friend contradictionᵒ in #2243 , and I won't pursue the more radical proposal on that PR ... or any other, until v3.0! But definitely keen to push on with what's already there. Please review!