Discussion:
[Agda] What style of proof irrelevance do you prefer: annotated or inferred?
Jesper Cockx
2018-10-28 21:01:28 UTC
Permalink
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
Jon Sterling
2018-10-29 00:32:29 UTC
Permalink
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
Post by Jesper Cockx
Hi Agda people,
In the comments on issue #3334
<https://github.com/agda/agda/issues/3334#issuecomment-433730080>, Wolfram
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.
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
https://lists.chalmers.se/mailman/listinfo/agda
Apostolis Xekoukoulotakis
2018-10-29 01:20:48 UTC
Permalink
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.
Post by Jon Sterling
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
- 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
Post by Jesper Cockx
Hi Agda people,
In the comments on issue #3334
<https://github.com/agda/agda/issues/3334#issuecomment-433730080>,
Wolfram
Post by Jesper Cockx
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
Post by Jesper Cockx
the type checker) should detect it whenever possible, and optimise it
away
Post by Jesper Cockx
as soon as possible.
Often the fact that a certain term is irrelevant is obvious to *you* as
the
Post by Jesper Cockx
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
Post by Jesper Cockx
of irrelevance would probably be very disappointing. (The alternative
where
Post by Jesper Cockx
Agda would eagerly erase things without asking and then complaining
later
Post by Jesper Cockx
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
Post by Jesper Cockx
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
Post by Jesper Cockx
(Andreas' irrelevant functions and irrelevant fields, and more recently
my
Post by Jesper Cockx
implementation of Prop). Maybe inferred proof irrelevance would work
better
Post by Jesper Cockx
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
Post by Jesper Cockx
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
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Jesper Cockx
2018-10-29 08:28:38 UTC
Permalink
Dear Jon,

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

It seems to me you like a combination of annotated compile-time irrelevance
and inferred run-time irrelevance, is that correct?

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.

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.

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.

-- Jesper
Post by Jon Sterling
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
- 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
Post by Jesper Cockx
Hi Agda people,
In the comments on issue #3334
<https://github.com/agda/agda/issues/3334#issuecomment-433730080>,
Wolfram
Post by Jesper Cockx
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
Post by Jesper Cockx
the type checker) should detect it whenever possible, and optimise it
away
Post by Jesper Cockx
as soon as possible.
Often the fact that a certain term is irrelevant is obvious to *you* as
the
Post by Jesper Cockx
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
Post by Jesper Cockx
of irrelevance would probably be very disappointing. (The alternative
where
Post by Jesper Cockx
Agda would eagerly erase things without asking and then complaining
later
Post by Jesper Cockx
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
Post by Jesper Cockx
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
Post by Jesper Cockx
(Andreas' irrelevant functions and irrelevant fields, and more recently
my
Post by Jesper Cockx
implementation of Prop). Maybe inferred proof irrelevance would work
better
Post by Jesper Cockx
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
Post by Jesper Cockx
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
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Andreas Nuyts
2018-10-29 11:32:06 UTC
Permalink
Dear everyone,

Another dimension (or is it again the compile/run-time dimension?) is
that of type-level vs. value-level annotations.
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.

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.
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 _`.

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

Best regards,

Andreas Nuyts
(not the Andreas mentioned in Jesper's emails)
Post by Jesper Cockx
Dear Jon,
Thanks for your answer. I see these two not so much as two different
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
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).
It seems to me you like a combination of annotated compile-time
irrelevance and inferred run-time irrelevance, is that correct?
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.
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.
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.
-- Jesper
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
- 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
Post by Jesper Cockx
Hi Agda people,
In the comments on issue #3334
<https://github.com/agda/agda/issues/3334#issuecomment-433730080>, Wolfram
Post by Jesper Cockx
I consider it counterproductive to be able to declare
irreleveance, and
Post by Jesper Cockx
even more counterproductive to have to do it for efficiency
reasons,
Post by Jesper Cockx
because that encourages premature optimisations. The compiler
(including
Post by Jesper Cockx
the type checker) should detect it whenever possible, and
optimise it away
Post by Jesper Cockx
as soon as possible.
Often the fact that a certain term is irrelevant is obvious to
*you* as the
Post by Jesper Cockx
Agda programmer but there's no way for Agda to figure this out
from the
Post by Jesper Cockx
code. If it's possible that you will use the term at any point
in the
Post by Jesper Cockx
future, Agda cannot (and should not) erase it. So any
automatic detection
Post by Jesper Cockx
of irrelevance would probably be very disappointing. (The
alternative where
Post by Jesper Cockx
Agda would eagerly erase things without asking and then
complaining later
Post by Jesper Cockx
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
Post by Jesper Cockx
accidentally in a non-erased position, instead of removing the
irrelevance
Post by Jesper Cockx
silently and causing hard-to-explain performance regressions.
But I realized this is based mostly on speculation and not hard
facts.
Post by Jesper Cockx
Historically, Agda has focused on the annotated style of
proof-irrelevance
Post by Jesper Cockx
(Andreas' irrelevant functions and irrelevant fields, and more
recently my
Post by Jesper Cockx
implementation of Prop). Maybe inferred proof irrelevance would
work better
Post by Jesper Cockx
than expected?
So now my question to *you*, the Agda community is this: do you
prefer
Post by Jesper Cockx
Agda's current style of annotated proof-irrelevance, or would
you rather
Post by Jesper Cockx
have Agda infer things for you (and perhaps fail to do so in
some cases)?
Post by Jesper Cockx
I won't promise I will remove Prop and focus all my attention on
inferring
Post by Jesper Cockx
irrelevance even if everyone votes for the latter option, but it
would be
Post by Jesper Cockx
interesting to know going forward what you think.
-- Jesper
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
James Chapman
2018-11-19 01:31:00 UTC
Permalink
Dear Jesper,

DON'T STOP THE PROP!

Personally, I like having Prop as I think it is theoretically and
practically interesting in its own right.

I share Wolfgang's sentiments to an extent but restrict them to the
'.dot' notation (sorry Andreas). In the past I used it primarily out of
desperation when formalizing category theoretic stuff. I dotted the
fields that contained equality proofs in the hope of reducing memory
consumption below the amount of memory my computer had. In this case I
wasn't interested in any changes to the theory and it introduced
limitations such as not being able to substitute (transport) via an
irrelevant equation in a type. Later due to improvements in Agda,
I was happy to remove the dots and return to thinking that I am working in
a more standard type theory without '.dot'.

With Prop I am more interested in things like using the opportunity to
squash (truncate) types down to one element and I would be interested
in being able to turn on impredicative quantification for Prop. Agda
is supposed to be based on UTT after all :)

Having a different universe where different rules apply seems nicer to
me than having a different function space. There is also a nice
separation, if you don't like it don't use it.

On a general note I think one can draw a parallel between being a
programmer and a proof engineer. As a programmer I would like to have
a good optimizing compiler but I still expect that different
implementations of a function can have different run time performance
and I might need to hand optimize (and potentially obfuscate) my
program. I think it is the same with proofs, different approaches
might have different type checking performance and I might need to
optimize/consider the trade offs (inc. readability or writability(is
that a word?)).
If my proof is also a program, I care again about run time performance
as well as type checking performance but both are important.

Regards,

James
On Mon, 29 Oct 2018 at 11:34, Andreas Nuyts
Post by Andreas Nuyts
Dear everyone,
Another dimension (or is it again the compile/run-time dimension?) is that of type-level vs. value-level annotations.
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.
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.
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 _`.
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.)
Best regards,
Andreas Nuyts
(not the Andreas mentioned in Jesper's emails)
Dear Jon,
It seems to me you like a combination of annotated compile-time irrelevance and inferred run-time irrelevance, is that correct?
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.
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.
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.
-- Jesper
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).
- 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
Post by Jesper Cockx
Hi Agda people,
In the comments on issue #3334
<https://github.com/agda/agda/issues/3334#issuecomment-433730080>, Wolfram
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.
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
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Thorsten Altenkirch
2018-11-19 09:57:51 UTC
Permalink
I fully agree. Also we use it in the construction of setoid type theory
which is a cheap way to get functional and propositional extensionality.

Thorsten

On 19/11/2018, 01:31, "Agda on behalf of James Chapman"
Post by Jon Sterling
Dear Jesper,
DON'T STOP THE PROP!
Personally, I like having Prop as I think it is theoretically and
practically interesting in its own right.
I share Wolfgang's sentiments to an extent but restrict them to the
'.dot' notation (sorry Andreas). In the past I used it primarily out of
desperation when formalizing category theoretic stuff. I dotted the
fields that contained equality proofs in the hope of reducing memory
consumption below the amount of memory my computer had. In this case I
wasn't interested in any changes to the theory and it introduced
limitations such as not being able to substitute (transport) via an
irrelevant equation in a type. Later due to improvements in Agda,
I was happy to remove the dots and return to thinking that I am working in
a more standard type theory without '.dot'.
With Prop I am more interested in things like using the opportunity to
squash (truncate) types down to one element and I would be interested
in being able to turn on impredicative quantification for Prop. Agda
is supposed to be based on UTT after all :)
Having a different universe where different rules apply seems nicer to
me than having a different function space. There is also a nice
separation, if you don't like it don't use it.
On a general note I think one can draw a parallel between being a
programmer and a proof engineer. As a programmer I would like to have
a good optimizing compiler but I still expect that different
implementations of a function can have different run time performance
and I might need to hand optimize (and potentially obfuscate) my
program. I think it is the same with proofs, different approaches
might have different type checking performance and I might need to
optimize/consider the trade offs (inc. readability or writability(is
that a word?)).
If my proof is also a program, I care again about run time performance
as well as type checking performance but both are important.
Regards,
James
On Mon, 29 Oct 2018 at 11:34, Andreas Nuyts
Post by Andreas Nuyts
Dear everyone,
Another dimension (or is it again the compile/run-time dimension?) is
that of type-level vs. value-level annotations.
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.
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.
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 _`.
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.)
Best regards,
Andreas Nuyts
(not the Andreas mentioned in Jesper's emails)
Dear Jon,
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
little inferred compile-time irrelevance (the only thing that comes to
mind is the unit type, which is automatically proof-irrelevant because
of eta).
It seems to me you like a combination of annotated compile-time
irrelevance and inferred run-time irrelevance, is that correct?
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.
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.
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.
-- Jesper
On Mon, Oct 29, 2018 at 1:33 AM Jon Sterling
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
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
- 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
Post by Jesper Cockx
Hi Agda people,
In the comments on issue #3334
<https://github.com/agda/agda/issues/3334#issuecomment-433730080>,
Wolfram
Post by Jesper Cockx
I consider it counterproductive to be able to declare irreleveance,
and
Post by Jesper Cockx
even more counterproductive to have to do it for efficiency reasons,
because that encourages premature optimisations. The compiler
(including
Post by Jesper Cockx
the type checker) should detect it whenever possible, and optimise
it away
Post by Jesper Cockx
as soon as possible.
Often the fact that a certain term is irrelevant is obvious to *you*
as the
Post by Jesper Cockx
Agda programmer but there's no way for Agda to figure this out from
the
Post by Jesper Cockx
code. If it's possible that you will use the term at any point in
the
Post by Jesper Cockx
future, Agda cannot (and should not) erase it. So any automatic
detection
Post by Jesper Cockx
of irrelevance would probably be very disappointing. (The
alternative where
Post by Jesper Cockx
Agda would eagerly erase things without asking and then complaining
later
Post by Jesper Cockx
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
Post by Jesper Cockx
accidentally in a non-erased position, instead of removing the
irrelevance
Post by Jesper Cockx
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
Post by Jesper Cockx
(Andreas' irrelevant functions and irrelevant fields, and more
recently my
Post by Jesper Cockx
implementation of Prop). Maybe inferred proof irrelevance would work
better
Post by Jesper Cockx
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
Post by Jesper Cockx
have Agda infer things for you (and perhaps fail to do so in some
cases)?
Post by Jesper Cockx
I won't promise I will remove Prop and focus all my attention on
inferring
Post by Jesper Cockx
irrelevance even if everyone votes for the latter option, but it
would be
Post by Jesper Cockx
interesting to know going forward what you think.
-- Jesper
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

Loading...