[Agda] Cost of ``open ... public using (...)''?
kahl at cas.mcmaster.ca
Tue Jan 29 04:59:33 CET 2013
| Nisse, Andreas, Peter II: Optimizing Agda (positivity graph)
| We: Trying to make "open M x using (y)" not create useless things.
| Fr: Gave up on this for now.
I have observed significant cost of
open M x public using (y)
, and I am working around this regularly (at some cost to
the niceness of my code), but I don't think that I have ever seen
this performance impact without ``public''.
(I just did a quick test: ``using'' in a pure import context (i.e., no ``public'')
actually saved a tiny bit on allocation and MUT time.)
My main question is: Does the problem with ``using public'' only affect ``using'',
or also ``hiding''?
(``hiding'' is much more of a hassle to work around, especially with large modules...)
Apart from that, I am also curious: What is behind this effect anyways?
Is there an issue on the issue tracker associated with it?
(I could not identify anything from what I found for ``using'' or ``open using''.)
P.S.: This page seems to be strangely disconnected from the AIM it belonged to...
More information about the Agda