[Agda] What style of proof irrelevance do you prefer: annotated or inferred?

[Jesper Cockx]

Hi Agda people,

In the comments on issue #3334
<https://github.com/agda/agda/issues/3334#issuecomment-433730080>, Wolfram
wrote:

I consider it counterproductive to be able to declare irreleveance, and
> even more counterproductive to have to do it for efficiency reasons,
> because that encourages premature optimisations. The compiler (including
> the type checker) should detect it whenever possible, and optimise it away
> as soon as possible.


To which I replied:

Often the fact that a certain term is irrelevant is obvious to *you* as the
> Agda programmer but there's no way for Agda to figure this out from the
> code. If it's possible that you will use the term at any point in the
> future, Agda cannot (and should not) erase it. So any automatic detection
> of irrelevance would probably be very disappointing. (The alternative where
> Agda would eagerly erase things without asking and then complaining later
> when you try to use them is arguably worse). Another advantage of
> annotating irrelevant things, is that Agda can warn you when you use it
> accidentally in a non-erased position, instead of removing the irrelevance
> silently and causing hard-to-explain performance regressions.
>

But I realized this is based mostly on speculation and not hard facts.
Historically, Agda has focused on the annotated style of proof-irrelevance
(Andreas' irrelevant functions and irrelevant fields, and more recently my
implementation of Prop). Maybe inferred proof irrelevance would work better
than expected?

So now my question to *you*, the Agda community is this: do you prefer
Agda's current style of annotated proof-irrelevance, or would you rather
have Agda infer things for you (and perhaps fail to do so in some cases)?

I won't promise I will remove Prop and focus all my attention on inferring
irrelevance even if everyone votes for the latter option, but it would be
interesting to know going forward what you think.

-- Jesper
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181028/ff1353d6/attachment.html>