Confused by the order of the implicit argument insertion

Stream: lean4

[Tim Hunter]

Hello,
I am a bit confused by the (very useful) feature p.foo a b c where p is a structure. According to the documentation:
https://leanprover.github.io/lean4/doc/struct.html
this is translated as MyStructure.foo a b c p. However, it seems that the compiler is currently more lenient in the order of arguments

namespace List

def f2: List α -> Nat -> Nat
| _, x => x

def f3: Nat -> List α -> Nat
| x, _ => x

def g: List α -> List α -> Nat
| _, l => l.length

end List

let l : List Int := [1,2,3]
assert! l.f2 1 = 1
assert! l.f3 1 = 1
-- Can you guess the outcome?
assert! [].g [1] = 1

As a beginner, I try to be careful as a result because the outcome is not always clear to me. Am I missing something?

[Horatiu Cheval]

It’s not about implicitness, but about dot notation. When using dot notation, the argument before the dot is passed to the first argument of the function that matches the namespace (List in your case). So [].g [1] means g [] [1], whose result is clearly 1

[Tim Hunter]

So then, why would the f3 example work? Shouldn't it be translated to List.g l 1, which will then fail? It currently compiles and executes without issue.

[Horatiu Cheval]

l.f3 1 is translated to List.f3 1 l because 1 is not a List. l is sent to the first argument that matches the type List which in this case is the second one

[Tim Hunter]

Ah indeed, reading more carefully the documentation, I now understand: "given an expression p.foo x y z, Lean will insert p at the first argument to foo of type Point". Unlike a language like python for example, it will look at type of the argument during the desugaring.

Since this is the case, are there some best practices? For example, most OO languages would use the first argument but Haskell tends to consider the last argument.

[Horatiu Cheval]

With python do you mean the self argument which normally (or maybe even necessarly, I haven't tried otherwise) is the first argument of a method?

[Horatiu Cheval]

I think in Haskell an important design decision regarding the order of the arguments is to decide what is the most likely situation in which you will want to partially apply your function, and a good order of the arguments will make that considerably easier. I think this still holds true for Lean, because function application follows the same idea. But even if you order the arguments so that that kind of writing is easier for you, you are then still able to use dot notation.

[Horatiu Cheval]

For instance map from the standard library has type List.map (f : α → β) : List α → List β. This allows you to easily write map f for some f in order to succintly state that you want to applyf to lists, but you may still do l.map f if it's more readable in the context. But I don't know whether there are official style guidelines for this

[Horatiu Cheval]

Personally, I think one of the nicest things about dot notation is that it allows you to call functions from namespaces with long names without explicitly writing them or opening them. I.e. if you already have some x : Namespace1.Namespace2.Namespace3 and some function f from the same namespace, you may simply write x.f without worrying about the namespace