Redundant uses of `with`

[jamesmckinna]

I have recently undertaken a study of all the uses of with in stdlib (there are 650-700 of them, for the sake of a ballpark figure), and discovered some surprising things as a result. Two things (at least) leap out:

• the use of with on boolean subexpressions, in place of if_then_else_ (there are over 100 of these alone, sometimes but not always in the context of more complex pattern-matching analysis);
• the use of with to introduce a name for a recursive call on a function, not subsequently analysed by pattern matching.

The purpose of this issue is to draw attention to such uses, and ask whether they should be replaced/refactored away in favour of 'simpler' definitions. The first seems now to be 'idiomatic' Agda: I'm certainly not arguing per se for uses of if_then_else_, but it is striking that we (seem to) have adopted a style self-consciously not like 'ordinary' functional programming, even when that is available.

A specimen example of the second case is given the following, in Data.List.Properties:

splitAt-defn : ∀ n → splitAt {A = A} n ≗ < take n , drop n >
splitAt-defn zero    xs       = refl
splitAt-defn (suc n) []       = refl
splitAt-defn (suc n) (x ∷ xs) with splitAt n xs | splitAt-defn n xs
... | (ys , zs) | ih = cong (Prod.map (x ∷_) id) ih

whose final defining clause could, much more straightforwardly, be replaced by

splitAt-defn (suc n) (x ∷ xs) = cong (Prod.map (x ∷_) id) (splitAt-defn n xs)

[JacquesCarette]

I think there was an era of doing Agda development where some people were over-enthusiastic users of with, before its fragility was fully known/realized. I think there might have been a bit of a "shiny new thing" effect -- if_then_else is so passé, especially for those who know about boolean blindness.

My opinion:

• if if_then_else would do the job just fine, use it.
• don't abuse with to do simple pattern-matching. Do use with when it causes rather non-trivial new information to get exposed. (Personally, I avoid it in my own code even for that, but that's personal style.)

For the specimen you give, I prefer the cong version. And I'm pretty sure there's a function in Data.Product to avoid the id, while you're at it!

[gallais]

with gets stuck until you abstract over & match on the expression it mentions.
A function with an if_then_else_-based RHS will unfold just fine, potentially making
the goal noisier.

I don't know whether it's an actual problem but it could be why people reached for
with instead of an if.

[JacquesCarette]

I wonder if the recent features (not yet merged) to do more controlled abstraction and unfolding might be a more disciplined way to achieve this.

That people may have done hacks with with to achieve their aims shows this is really a needed feature.

[jamesmckinna]

Re: recent features. I notice that with application f e | r in user-defined code raises a 'NotImplemented' error (AFAIU, it is implemented natively in idris(2)). Any likelihood of it being implemented any time? And if so, would it affect Guillaume's point above about (preventing) unfolding?

[JacquesCarette]

You'd definitely have to ask that on the agda board or the Zulip, the agda devs don't monitor stdlib chat all that closely.

[jamesmckinna]

Yes, and at the Delft AIM (I hope)

[jamesmckinna]

See also my solution to @omelkonian 's agda issue 5833.
Such gymnastics should not be necessary in general, so weeding out (further) redundant uses of with seems a good idea.

[jamesmckinna]

Besides the merged PR, I think this is best kept open, but maybe handled piecemeal going forward?
UPDATED: one of the discussion points from this morning's meeting about the v2.0 release (issue 2063) was that we do not try to handle this issue 'as we go' in other PRs. So I'm going to open a revised companion version of this issue (with a shopping list). and close this one. See #2123