Zulip Chat Archive

Stream: general

Topic: good name?

Yury G. Kudryashov (Jul 23 2020 at 22:41):

What would be a good name for the following function?

def noname [monoid M] (l : list α) (f : α → α → M) : M := (l.zip_with f l.tail).prod

Yury G. Kudryashov (Jul 23 2020 at 22:42):

I'm mostly interested in the additive version of this with f = dist or f = edist.

Jalex Stark (Jul 23 2020 at 22:42):

is it a add_comm_monoid? then you could use finset sum / prod, which i think has more lemmas than list sum / prod

Yury G. Kudryashov (Jul 23 2020 at 22:45):

For l = a₀ :: a₁ :: a₃ :: a₄ we have noname l f = f a₀ a₁ * f a₁ a₂ * f a₃ a₄.

Yury G. Kudryashov (Jul 23 2020 at 22:46):

I think it's easier to express this using list, not finset.

Yury G. Kudryashov (Jul 23 2020 at 22:46):

My question is how to call this.

Jalex Stark (Jul 23 2020 at 22:46):

ah, thanks, I had not understood the definition before

Floris van Doorn (Jul 23 2020 at 22:47):

maybe something like sequential_prod or map_prod_sequential

Jalex Stark (Jul 23 2020 at 22:47):

in math i might call it a product over f at consecutive pairwise elements

Floris van Doorn (Jul 23 2020 at 22:48):

(I'm a little surprised that zip_with is not called map2)

Jalex Stark (Jul 23 2020 at 22:48):

i think zip_with is a haskell name and map2 is a mathlib name?

Jalex Stark (Jul 23 2020 at 22:51):

pandas would call this something like l.rolling(2).agg(f).prod()

Floris van Doorn (Jul 23 2020 at 22:52):

Jalex Stark said:

i think zip_with is a haskell name and map2 is a mathlib name?

I wouldn't call it a mathlib name, since the only time map2occurs in the library is nonempty.map2 (contributed by me).
I probably got the naming scheme from Coq: https://coq.github.io/doc/master/api/coq/Util/List/index.html#val-map2 (if something exists for a unary function, appending a 2 means the corresponding thing for a binary function)

Jannis Limperg (Jul 23 2020 at 23:15):

list.map₂ is from core.

Jalex Stark (Jul 23 2020 at 23:20):

and has the same type signature as list.zip_with

Jalex Stark (Jul 23 2020 at 23:21):

they have slightly different implementations but I think they compute the same function

Jannis Limperg (Jul 23 2020 at 23:22):

Yeah, it's the same function with two implementations in the same file. Never change, Lean.

Floris van Doorn (Jul 23 2020 at 23:23):

they're both from core, defined in the same file :O

Jalex Stark (Jul 23 2020 at 23:23):

we don't have to remove it if we add the right simp lemma :P

Last updated: Dec 20 2023 at 11:08 UTC