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