To let or not to let

[JacquesCarette]

Right now, let in Agda generates substitutions (as confirmed by Andreas here amongst other places). The attempted fix for this has stalled even though it is an extremely old issue.

The advice is to favour where over let.

The question is: do we program stdlib to current Agda or some optimistic future Agda that will have a better implementation of let?

Given just how long this has been a wart, I'm of the opinion that being optimistic would be ill-placed (even though I'm actually normally fairly optimistic!)

[gallais]

FTR, these cannot be turned into where definitions because these get lifted to the
toplevel and that is not done in a modality-respecting way. In other words: turning
these into where definitions leads to errors about irrelevant values being used in
a relevant context.

https://github.com/gallais/agda-stdlib/blob/7947cd42ca813dfc9024bc50552c5cd5ea35f221/src/System/Random.agda#L119-L133

[JacquesCarette]

Good point: indeed there are times when we have no choice, because the implementation scheme for where is also sub-optimal.

[jespercockx]

Unfortunately, Agda currently does not have any way to create a local shared closure: let bindings are inlined, while where declarations are lifted to the top level.

[jamesmckinna]

Time to revisit after 2.7.0's introduction of using?

[JacquesCarette]

That would be great - but we'd need to know how using is implemented to see if it's actually a win. Perhaps @jespercockx can enlighten us?

[jespercockx]

I was not the one who implemented it, but I believe using is desugared to an auxiliary function, so I'm afraid it's not really better performance-wise than a where declaration.

I started working on implementing proper let-bindings for Agda's internal syntax during the last Agda meeting (see agda/agda#7253) but it's a lot more complicated that I had anticipated so don't expect anything from it soon.