<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    Dear everyone,<br>
    <br>
    Another dimension (or is it again the compile/run-time dimension?)
    is that of type-level vs. value-level annotations.<br>
    We can consider `IrrFun = .(x : A) -> B x` a subtype of `RelFun =
    (x : A) -> B x`. In this view, RelFun may be inhabited by lambdas
    that are in fact known to be irrelevant and whose argument can
    therefore be erased, both at compile and at run-time.<br>
    <br>
    My (draft of a) suggestion is the following: when the Agda user
    types a lambda-expression `λ (x : A) -> b[x]`, it is inferred
    from `b[x]` whether this is an irrelevant lambda. Of course, if the
    type given by the user is `IrrFun`, then this only type-checks if
    the lambda is inferred to be irrelevant. However, if the type given
    by the user is `RelFun` but the lambda is irrelevant, then this fact
    is remembered in the form of an internal annotation on the lambda,
    as it allows erasure of the argument both at compile and at runtime.
    Without the annotation on the lambda, erasure could only happen
    after beta-reducing the lambda, which is probably less efficient.<br>
    This behaviour would be in accordance to what happens if you
    explicitly coerce a function `f : IrrFun` to `RelFun` by
    lambda-expanding. It then becomes `λ (x : A) -> f _`.<br>
    <br>
    When it comes to inferring type-level annotations: this is a problem
    quite similar to inferring universe levels. When a user does not
    specify a universe level, do you want to infer the smallest one, or
    do you want to complain? (I think Agda currently complains about an
    unresolved meta, although C-c C-= will fill out the smallest
    option?) Similarly, when a user does not specify a modality, do you
    want to infer the most informative one (irrelevance, if possible),
    or do you want to complain? (I don't have any answers here, just
    pointing out the similarity of the problems.)<br>
    <br>
    Best regards,<br>
    <br>
    Andreas Nuyts<br>
    (not the Andreas mentioned in Jesper's emails)<br>
    <br>
    <div class="moz-cite-prefix">On 29/10/2018 09:28, Jesper Cockx
      wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CAEm=boz5eB1nEpyj4Ta5fwP0mHmxphU=EOPNDoG1X22bMmtanQ@mail.gmail.com">
      <meta http-equiv="content-type" content="text/html; charset=UTF-8">
      <div dir="ltr">
        <div>Dear Jon,</div>
        <div><br>
        </div>
        <div>Thanks for your answer. I see these two not so much as two
          different kinds of proof irrelevance, but as two separate
          dimensions: compile-time vs run-rime irrelevance and annotated
          vs inferred irrelevance. For example, Agda has annotated
          compile-time irrelevance (irrelevant functions and Prop),
          inferred run-time irrelevance (type erasure, forcing analysis,
          detection of unused arguments), Andreas recently added
          annotated run-time irrelevance (the @erased annotation), but
          it has very little inferred compile-time irrelevance (the only
          thing that comes to mind is the unit type, which is
          automatically proof-irrelevant because of eta).</div>
        <div><br>
        </div>
        <div>It seems to me you like a combination of annotated
          compile-time irrelevance and inferred run-time irrelevance, is
          that correct?</div>
        <div><br>
        </div>
        <div>What Wolfram seemed to suggest however is to infer more
          *compile-time* irrelevance. For example, we could infer that
          the empty type is proof-irrelevant and automatically discard
          any equation at the empty type during conversion (i.e. have
          eta for the empty type). Or we could detect that the identity
          type has a single constructor and (assuming --with-K) replace
          all proofs of identity by primTrustMe during elaboration.</div>
        <div><br>
        </div>
        <div>The thing is, such automatically inferred irrelevance
          wouldn't work very well in some cases, and it would certainly
          not help for the fancy applications of irrelevance you
          describe (enforcing parametricity or coherence). However it
          *would* give some benefits of irrelevance to people who use
          Agda but don't want to add extra irrelevance annotations, or
          indeed even to people who don't know about irrelevance at all.
          So it has a much greater potential impact than the annotated
          style of irrelevance.</div>
        <div><br>
        </div>
        <div>Of course, much depends on how often we could actually
          detect irrelevance automatically, which in turn would depend
          greatly on the concrete codebase. But perhaps doing the
          experiment could give us a better idea.</div>
        <div><br>
        </div>
        <div>-- Jesper<br>
        </div>
      </div>
      <br>
      <div class="gmail_quote">
        <div dir="ltr">On Mon, Oct 29, 2018 at 1:33 AM Jon Sterling <<a
            href="mailto:jon@jonmsterling.com" moz-do-not-send="true">jon@jonmsterling.com</a>>
          wrote:<br>
        </div>
        <blockquote class="gmail_quote" style="margin:0 0 0
          .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Jesper,<br>
          <br>
          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).<br>
          <br>
          The latter (semantic) kind of proof irrelevance could be used,
          for instance, in order to achieve the following things:<br>
          <br>
          - to specify that some function is parametric in its indices:
          for instance, operations on vectors<br>
          <br>
          - 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.<br>
          <br>
          - and of course, to obtain more definitional equivalences
          where possible<br>
          <br>
          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).<br>
          <br>
          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.<br>
          <br>
          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.<br>
          <br>
          Best,<br>
          Jon<br>
          <br>
          <br>
          <br>
          <br>
          On Sun, Oct 28, 2018, at 2:01 PM, Jesper Cockx wrote:<br>
          > Hi Agda people,<br>
          > <br>
          > In the comments on issue #3334<br>
          > <<a
            href="https://github.com/agda/agda/issues/3334#issuecomment-433730080"
            rel="noreferrer" target="_blank" moz-do-not-send="true">https://github.com/agda/agda/issues/3334#issuecomment-433730080</a>>,
          Wolfram<br>
          > wrote:<br>
          > <br>
          > I consider it counterproductive to be able to declare
          irreleveance, and<br>
          > > even more counterproductive to have to do it for
          efficiency reasons,<br>
          > > because that encourages premature optimisations. The
          compiler (including<br>
          > > the type checker) should detect it whenever
          possible, and optimise it away<br>
          > > as soon as possible.<br>
          > <br>
          > <br>
          > To which I replied:<br>
          > <br>
          > Often the fact that a certain term is irrelevant is
          obvious to *you* as the<br>
          > > Agda programmer but there's no way for Agda to
          figure this out from the<br>
          > > code. If it's possible that you will use the term at
          any point in the<br>
          > > future, Agda cannot (and should not) erase it. So
          any automatic detection<br>
          > > of irrelevance would probably be very disappointing.
          (The alternative where<br>
          > > Agda would eagerly erase things without asking and
          then complaining later<br>
          > > when you try to use them is arguably worse). Another
          advantage of<br>
          > > annotating irrelevant things, is that Agda can warn
          you when you use it<br>
          > > accidentally in a non-erased position, instead of
          removing the irrelevance<br>
          > > silently and causing hard-to-explain performance
          regressions.<br>
          > ><br>
          > <br>
          > But I realized this is based mostly on speculation and
          not hard facts.<br>
          > Historically, Agda has focused on the annotated style of
          proof-irrelevance<br>
          > (Andreas' irrelevant functions and irrelevant fields, and
          more recently my<br>
          > implementation of Prop). Maybe inferred proof irrelevance
          would work better<br>
          > than expected?<br>
          > <br>
          > So now my question to *you*, the Agda community is this:
          do you prefer<br>
          > Agda's current style of annotated proof-irrelevance, or
          would you rather<br>
          > have Agda infer things for you (and perhaps fail to do so
          in some cases)?<br>
          > <br>
          > I won't promise I will remove Prop and focus all my
          attention on inferring<br>
          > irrelevance even if everyone votes for the latter option,
          but it would be<br>
          > interesting to know going forward what you think.<br>
          > <br>
          > -- Jesper<br>
          > _______________________________________________<br>
          > Agda mailing list<br>
          > <a href="mailto:Agda@lists.chalmers.se" target="_blank"
            moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
          > <a
            href="https://lists.chalmers.se/mailman/listinfo/agda"
            rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
          _______________________________________________<br>
          Agda mailing list<br>
          <a href="mailto:Agda@lists.chalmers.se" target="_blank"
            moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
          <a href="https://lists.chalmers.se/mailman/listinfo/agda"
            rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
        </blockquote>
      </div>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <br>
  </body>
</html>