signature of `modify` functions

Stream: batteries

[Kim Morrison]

We have a variety of modify functions on collections, which take the form modify (c : Coll X) (f : X -> X) (i : Idx), except that there is inconsistency in the order of arguments: does the function come first (List.modify), or does the index come first (Batteries.HashMap.modify, Array.modify)?

Arguments either way?

I feel like it is slightly more likely the the partially applied modify f is useful rather than modify i. On the other hand it is probably more churn/harder to reach consistency to move the function first everywhere.

[François G. Dorais]

My gut tells me function first but I just realized I have no good argument for that.

[Joachim Breitner]

I guess there is no good answer. Partial application prefers function first, but lean's syntax encourages function arguments last (for parentheses-less fun that possibly spans multiple lines). So either is probably fine.

One could make the argument that function first is more versatile: works well partially applied, but in can get the other form with c.modify (i := …) fun x => ….

In any case I think it's important that the collection comes last, so that you can nicely nest calls to modify in each other.

[Mario Carneiro]

collection comes first is a fairly strong convention at this point

[Mario Carneiro]

I agree that having the index before function makes things easier in the large function case (which is a pretty common situation)

[Mario Carneiro]

We generally don't optimize for partial applications at all, because we have a section syntax and dot notation. Plus I would argue that overuse of partial application and especially higher order combinators is what leads to the classic (and unreadable) pointfree haskell style

[Joachim Breitner]

Fair points. I'm certainly prone to lean towards classic Haskell :-)

[Jannis Limperg]

My approach (inconsistently applied in Aesop) is:

• Collection last because the partially applied form modify f i or modify i f can be useful while modify c f or modify c i is never useful (could be written as c.modify instead).
• Function argument second to last because in the fully applied form it's usually nicer to write c.modify i λ <long expression> than c.modify (λ <long expression>) i, especially if the function spans over multiple lines. c.modify (i := i) f is an okay workaround, but the common case is the fully applied form, so we should optimise for that.

[Kim Morrison]

Jannis's case is pretty good! However, as Mario says above, collection first is pretty well established at this point (although with many exceptions). We can start changing that, but I'd want everyone who's spoken so far to be in favour. :-)

[Joachim Breitner]

Is it generally useful (even though a bit counter-intuitive) to put the namespace-relevant parameter near the end, on the grounds that if by using dot notation, you can effectively pull it to the front when explicitly applying it, and thus dot notation vs plain function application now gives you two useful partial applications of a single function.

[Yaël Dillies]

Yes, I have been using Joachim's argument above to justify a lot of my function argument order choices

[Mac Malone]

For my two cents, I fully agree with Jannis's analysis.

Also, I supsect the promienence of "collection first" in core is a result of Joachim's insight that putting the namespace-relevant parameter last is naturally counter-intuitive. It is natural when writing a definition for e.g. List to start with the thought that the first thing one needs is the List in question.