agda
Runtime irrelevance
Hi. I'm trying to use erased annotations but as I can see agda stdlib doesn't really support them. What I stumbled upon so far:
-
⊥-elimcan't take an erased⊥argument which is often needed when all proofs are erased. - Idris defines
Σvariants with erased first and second values called Exists and Subset which are also quite convenient to erase proofs.
Here is an example.
Should maybe agda stdlib have something similar? That would require agda stdlib to have --erasure option enabled which requires all dependent modules to have it.
See #2346 for an earlier version of a similar line of thought... I'd be broadly in favour, but for the complicated balance of forces/compatibility issues (esp. wrt infective options) involved in what constitutes a 'standard' library.
Note that you can implement
recover : @0 ⊥ → ⊥
recover ()
so you can plug your contradiction into a call to ⊥-elim.
Cf. Relation.Nullary.Recomputable.⊥-recompute... ob @gallais 's observation, while your other examples from Idris seem to be related to the other combinators defined there...?
while your other examples from Idris seem to be related to the other combinators defined there...?
Is it a question to me? :) I meant that it's sometimes useful to have dependent sum types with erased first/second values, and Idris has them. For instance, using my own definition of such type gave me almost 2x speed up in runtime for my code :)
See also: Data.Refinement for a version of "dependent sum types with erased second values" at least.
Agree that erased first projections are independently interesting, though...
There's also the issue of Irrelevant vs. @0 annotation. I don't think we have anything @0-related in the lib at the minute.
There's also the issue of
Irrelevantvs.@0annotation. I don't think we have anything@0-related in the lib at the minute.
Absolutely! I raised this explicitly as a point for us to discuss after the merge of experimental following the v2.7.0 release...