append and concat

Stream: general

[Yaël Dillies]

The names docs#list.append and docs#list.concat look like they are swapped around. Is this intentional? (I think there already was discussion about this somewhere, but I can't find it)

[Yaël Dillies]

More generally, all instances of docs#has_append look they ought to be called has_concat.

[Adam Topaz]

docs#list.cons

[Eric Wieser]

(I also remember seeing another discussion about this)

[Kyle Miller]

The classic functional programming cute wordplay for appending an element to the end of a list is snoc.

[Kyle Miller]

It's not uncommon to use "appending" or "concatenating" lists interchangeably, so I'd hesitate swapping the names. I think it'd be better to find a better name for list.concat.

[Adam Topaz]

Note that we do have docs#fin.snoc

[Adam Topaz]

We should probably use snoc for lists as well...

[Yaël Dillies]

I disagree. Concatenating always means "putting two things of the same one after each other". Appending can refer to concatenating, but not the other way around.

[Yaël Dillies]

And appending is the counterpart to prepending, which is docs#list.cons.

[Yaël Dillies]

How does it sound renaming append to concat, and concat to snoc?

[Mario Carneiro]

it sounds like a massive name change affecting the whole language

[Adam Topaz]

Not only the whole language (Lean3) but also Lean4

[Yaël Dillies]

Judge it yourself: lean#771

[Yaël Dillies]

Note that most uses should be unaffected as they use the ++ notation.

[Eric Wieser]

I think we should try and find the past discussion before doing anything drastic

[Kyle Miller]

This change also needs buy-in from the Lean 4 developers.

[Mauricio Collares]

I think it's worth splitting this discussion in two, since I guess renaming concat to snoc is comparatively uncontroversial

[Anne Baanen]

(Unfortunately) calling (++) "append" is pretty common in Haskell as well: https://hackage.haskell.org/package/base-4.17.0.0/docs/Data-List.html#v:-43--43-

(++) :: [a] -> [a] -> [a] infixr 5

Append two lists [...]

[Mauricio Collares]

From Haskell I expect append to have type a -> a -> a and concat to have type [a] -> a (as in https://hackage.haskell.org/package/base-4.17.0.0/docs/Data-Monoid.html)

[Anne Baanen]

What Haskell calls concat Lean calls docs#list.join (which fits with monad terminology)

[Ruben Van de Velde]

I have to say I find snoc quite a poor term

[Michael Stoll]

In (Common) Lisp, append joins two lists (non-destructively) and concat joins them destructively (i.e., by modifying the last pointer of the first list).
Magma uses Append to extend a sequence (the datatype similar to lists) by one element (at the end) and cat (an infix operator) to join sequences.

[Johan Commelin]

Another data point: https://www.swi-prolog.org/pldoc/doc_for?object=append/3

append(?List1, ?List2, ?List1AndList2)
    List1AndList2 is the concatenation of List1 and List2

[Bolton Bailey]

My reasoning is etymological. append makes sense to me as [a] -> a -> [a] because prepend would then mean a -> [a] -> [a], and concatenate comes from the latin roots for "to chain together", which makes sense for two objects of the same type. It's a bit surprising to me that Haskell append takes two containers, but I guess that's worth something. In Python, 'append' adds a single element to a list.

[Bolton Bailey]

Also, @Yaël Dillies perhaps where you saw this was this thread (where a relatively new user says that "concatenate is ++", so seems like this does indeed have the potential to confuse people as is).

[Eric Wieser]

That's the thread I was thinking of, thanks!

[Kyle Miller]

For what it's worth, Python's use of the word "append" trips me up pretty much every time I've been away from the language for a while.

If we're using etymologies here, then "append" is "hang after" and "prepend" is "hang before." It's not clear that prepend couldn't mean flip append.

[Kyle Miller]

Ruben Van de Velde said:

I have to say I find snoc quite a poor term

A nicer alternative for this is list.push (though this is not the function you'd want to use to for modeling stacks using list!)

[Kyle Miller]

Then the definition of docs4#Array.push would be in terms of List.push.

[Bolton Bailey]

Kyle Miller said:

If we're using etymologies here, then "append" is "hang after" and "prepend" is "hang before." It's not clear that prepend couldn't mean flip append.

My reasoning is this: If this were the intended definition, there would have been no reason for the term prepend to have arisen as a portmanteau, since there would already have been a way to express the notion: instead of saying "prepend list_b to a" we could just say "append a to list_b".

[Yaël Dillies]

Bolton Bailey said:

My reasoning is etymological. append makes sense to me as [a] -> a -> [a] because prepend would then mean a -> [a] -> [a], and concatenate comes from the latin roots for "to chain together", which makes sense for two objects of the same type. It's a bit surprising to me that Haskell append takes two containers, but I guess that's worth something. In Python, 'append' adds a single element to a list.

Yes that's exactly my reasoning as well.

[Michael Stoll]

Ruben Van de Velde said:

I have to say I find snoc quite a poor term

I agree. I think mathlib is inteded to be useful for mathematicians, and almost no mathematician will know that snoc is even a thing (and so will have problems finding it). I myself wouldn't without having read this conversation.

[Alex J. Best]

Well cons isn't a word I recognize from mathematics either, with terms like this there will always be some learning curve for the language, that seems unavoidable

[Kevin Buzzard]

I'd go so far as to say that list isn't really a word I recognise from mathematics!

[Wrenna Robson]

Just to put my two cents in - that's definitely not what I would have expected concat to mean. append is a bit more ambiguous, to be fair.

[Yaël Dillies]

What should happen here? The current situation seems very weird and it keeps cropping up. See for example #17209

[Kyle Miller]

I personally think nothing should happen. It's not so hard to learn that "append" and "concat" mean what they do in Lean. Every language seems to make mutually incompatible choices, and there is no uniquely correct choice.

[Eric Wieser]

Personally I think the way forward here is:

• Put together a document (gist) indicating the terminology used by as many languages as possible, both for and against the change
• Make an offer to deal with making the change in Lean 4
• Put forth the above two items to Leo to be the final arbiter
• If the change is OK'd for lean4, backport to Lean 3

[Eric Wieser]

Item 1 could go in the docs as a library note even if we don't go forward with the other steps

[Martin Dvořák]

I had no idea list.concat existed. I was writing l ++ [a] instead of list.concat l a all the time. In fact, I have nearly 200 occurrences of terms like l ++ [a] in my project!

[Yaël Dillies]

Do you feel like you didn't know about it because it is misnamed? Would you have thought of looking for list.append?

[Martin Dvořák]

I am not sure. I vaguely remember that, when I was starting with my project, I had trouble remembering that ++ was called list.append which I needed to know in order to write the lemma names by heart. IIRC list.concat was what I expected ++ to be called. Nevertheless, I am now very comfortable with list.append and I would have big trouble getting used to the other name.

[Martin Dvořák]

As for list.concat, I don't think I ever actively searched for a different way to write l ++ [a].

[Martin Dvořák]

I can imagine l.concat a is slightly easier than l ++ [a] but, after I looked up list.concat now, it seems to me that l ++ [a] is better because more lemmata are available without converting it to the other form.