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

Mon Oct 29 02:20:48 CET 2018

Regarding Irrelevance as an optimization, I think that it is easy to
determine it. Correct me if I am wrong.

Assuming that we perform optimization knowing all the code, definitions and
for simplicity that there are no let statements,
in the Treeless representation , one would identify a variable as unused if
it is not used in an application TApp or in TCase.

The algorithm would remove the specific argument from the function and it
will find all the functions that use this function and remove terms that
are applied to it at this position.

The fact that we removed the use of some terms as arguments to an
application, gives us new opportunities for optimization.
We perform the above steps iteratively till no more changes are possible.

In this algorithm, we also remove terms due to "global" reasons.
Computational irrelevance can be introduced in the middle of the algorithm,
it would be impossible to know it from the beginning.

Personally, I am optimistic that it can be done. I haven't though
implemented this yet, so I might be wrong in my assumptions.

On Mon, Oct 29, 2018 at 2:32 AM Jon Sterling <jon at jonmsterling.com> wrote:

> Dear Jesper,
>
> I feel that these are two separate issues getting conflated -- on the one
> hand, a compiler may infer that something is irrelevant, and then erase it
> in order to achieve a more efficient execution. On the other hand, there is
> proof irrelevance which is used for *semantic* reasons: irrelevance is part
> of the specification of some function, and whether or not it executes in an
> irrelevant or erased way is really beside the point (of course, in such a
> case, the compiler *should* erase it because it is low hanging fruit).
>
> The latter (semantic) kind of proof irrelevance could be used, for
> instance, in order to achieve the following things:
>
> - to specify that some function is parametric in its indices: for
> instance, operations on vectors
>
> - relatedly, to force *coherence*: for instance, when defining some
> interpretation of some language, you can use proof irrelevence + some
> inversion lemmas to formalize the old pattern (from Streicher) of defining
> your function by recursion on the labels of the derivation rather than on
> the derivation itself. In old school math, this required defining a partial
> function and then establishing that it terminates, but in very fancy type
> theory we can use proof irrelevance to do this simultaneously and get a
> total function all at once.
>
> - and of course, to obtain more definitional equivalences where possible
>
> Let me unleash a kind of important point: as I mentioned, in all these
> cases, erasure should obviously be done, but there are cases where a good
> compiler would perform erasure even when it is not possible to type the
> term using the irrelevant types. Something might be erasable for global
> reasons. Anyway, it's not so important to me that Agda catch all of these
> cases, because I'm not using Agda for executing code (but others might be).
>
> What I'm saying is that inferring when something is computationally
> irrelevant must be treated as orthogonal to whether something can be typed
> with a proof irrelevance modality. Computational irrelevance is a property
> of code in the compilation target language (which could be anything), not a
> property of code in the Agda language.
>
> We should take compilation seriously, and not conflate it with
> typechecking and elaboration. Dependently typed languages have *two*
> computational semantics: the one which generates definitional equivalence
> of terms, and the one which executes.
>
> Best,
> Jon
>
>
>
>
> On Sun, Oct 28, 2018, at 2:01 PM, Jesper Cockx wrote:
> > 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
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181029/ab8aab5f/attachment.html>