List.drop vs String.drop

Stream: lean4

[Horațiu Cheval]

Is there a design consideration behind the fact that docs#String.drop takes the string as the first argument, while docs#List.drop takes the list as the second one (and the same for take etc)? Of course, it's irrelevant when using dot notation, but it can lead to some minor inconveniences without (e.g. switching from String to List Char in a large codebase)

[Mario Carneiro]

I believe the preference is to take the main argument first

[Mario Carneiro]

which differs from the haskell convention to put the main argument last

[Horațiu Cheval]

Yes, though many list functions seem to go against this preference

[Kyle Miller]

I think a motivation for number first is that List.drop n is an operator that drops n elements, like how List.map f is an operator that maps f over the elements, and so on.

[Mario Carneiro]

that's the reason haskell does it, but I think it's not a strong argument in lean because (·.drop n) also does this

[Mac Malone]

Mario Carneiro said:

that's the reason haskell does it, but I think it's not a strong argument in lean because (·.drop n) also does this

However, (·.drop n)only works if the expected type is know to be a List operator. If not, the List.drop n style is the necessary form. I have encoutered this problem a number of times in the wild (for types other than List).