Understanding operator dot notation

Stream: lean4

[James Sully]

open System (FilePath)

def runtimeDir : IO FilePath := return "/foo"

def getSockPath1 : IO FilePath := do
  return (← runtimeDir).join "timerd.sock"

def getSockPath2 : IO FilePath :=
  runtimeDir <&> (·.join "timerd.sock")

def getSockPath3 : IO FilePath :=
  runtimeDir <&>.join "timerd.sock"

-- /foo/timerd.sock (expected)
#eval getSockPath1

-- /foo/timerd.sock (expected)
#eval getSockPath2

-- /foo (unexpected)
#eval getSockPath3

I don't really have a good mental model of how operators interact with "method syntax". Why does getSockPath3 have the result it does?

[Sebastian Ullrich]

I don't really have a good mental model of how operators interact with "method syntax".

They don't. What you wrote is equivalent to runtimeDir <&> (.join "timerd.sock"), which is equivalent to runtimeDir <&> (FilePath.join "timerd.sock"), which prepends a path to an absolute path, which discards the first path

[James Sully]

Ah so it's only for |>

[James Sully]

That makes sense, thank you