flip vs swap

Stream: mathlib4

[Violeta Hernández]

We have docs#flip and docs#Function.swap and these seem to be entirely identical (save for the latter being dependently typed). Should one be deprecated for the other?

[Eric Wieser]

The latter also works with dot notation

[Kyle Miller]

@Eric Wieser It "works" with dot notation, but not in the way you would expect.

[Eric Wieser]

In that the effect is surprising, or the mechanism is?

[Kyle Miller]

The effect

[Eric Wieser]

Oh no, it fills in the type argument!

[Aaron Liu]

import Mathlib

example (a b : Nat) (c : Nat → Nat → Type)
    (f : (a : Nat) → (b : Nat) → c a b) : c b a :=
  c.swap f a b

[Aaron Liu]

Is this a quirk of Function. or does this happen with all dot notation?

[Eric Wieser]

I think all dot notation fills in the first argument with the right type, rather than the first explicit argument

[Eric Wieser]

I believe Kyle had an RFC for marking which argument should participate

[Kyle Miller]

My very first Lean RFC is about this too: lean4#1629

[Kyle Miller]

(The motivation for this "first argument, even if it's implicit" behavior is that it makes dot notation consistent when you are using it on a typeclass instance, where the typeclass appears as an instance implicit argument.)

[Eric Wieser]

"first explicit argument if there is one, followed by first implicit otherwise" would seemingly work for that case too

[Eric Wieser]

It's quite uncommon for a typeclass to appear in both positions

[Kyle Miller]

Here's my current RFC about it: lean4#6489

The first RFC suggests looking for a self parameter, and the new one suggests looking for a dotParam-annotated parameter.

[Kyle Miller]

Eric Wieser said:

"first explicit argument if there is one, followed by first implicit otherwise" would seemingly work for that case too

An annoying complication is that somehow we have to interleave finding CoeFun instances. I suppose for Function it would be fairly rare for there to be a CoeFun instance, and there's no confusion between trying for a CoeFun instance and making use of an implicit function-type argument.

[Kyle Miller]

For "there's only one way to do it" purposes, dotParam seems like the right choice to me.

However, I'm feeling tempted to let self be used for this too. The main argument against self is that it tempts people to use it rather than a more descriptive parameter name.

[Kyle Miller]

Anyway, regarding the original question, I believe there are a number of examples where there's the dependently-typed version and the simply-typed version, and you sort of need both since the former is more complicated to elaborate and might fail so you want the second, but also you do want the more complicated one since not everything is simply typed.

[Eric Wieser]

I guess we could try making the one in core dependently-typed and see what breaks?

[Kyle Miller]

I'm wondering if it's a good use of time though. Usually we don't use these functions for plain functions, and at least in core we don't tend to write in point-free style.

[Kyle Miller]

Haskell programmers learning Lean might gravite toward flip, and I'd hate to see dependent type issues making their programming style not work for them.

[Eric Wieser]

I'm wondering if it's a good use of time though.

Well, if it works everywhere then that's perhaps an argument for dropping it; and if it doesn't, it gives us something to put in the docstring of Function.swap explaining why it can't replace flip

[Eric Wieser]

I'm not proposing trying to fix all downstream breakages, only check if there are any!