`⊥` is `Recomputable` about agda-stdlib HOT 7 CLOSED

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.

from agda-stdlib.

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'.

from agda-stdlib.

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'.

from agda-stdlib.

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

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

Would this constitute a breaking change?

from agda-stdlib.

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.

from agda-stdlib.

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!

from agda-stdlib.

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!

from agda-stdlib.