Skip to content

Alternate names for `List.concat` and `List.append`

Jump to bottom
thorimur edited this page Dec 5, 2023 · 34 revisions

This follows on from ideas in:

Note that Lean's documentation is often inconsistent with its naming: e.g. a function called concat is said to append, a function called append is said to perform concatenation.

Comparison across languages

(m) means "mutates in place"

Language Type x :: xs xs ++ [x] xs ++ ys xss[0] ++ xss[1] ++ ...
Lean List cons x xs concat xs x append xs ys join xss
Lean Fin n -> X cons x xs snoc xs x append xs ys We don't seem to have this. See below.*
Lean Array `xs.insertAt! 0 x xs.push x append xs ys xss.flatten and xss.join (duplication)
Python list xs.insert(0, x) (m) xs.append(x) (m) operator.concat(xs, ys) (though append and extend also work) Various Pythonic ways to do this, no named function.
Python deque xs.appendleft(x) (m) xs.appendright(x) (m) operator.concat(xs, ys) Various Pythonic ways to do this, no named function.
PHP Array array_unshift() array_push() array_merge($xs, $ys) array_merge(...$xss)
Cryptol Sequence (size-dependent) [x] # xs xs # [x] (#) (doc: "append"). join xss
Haskell List (:) snoc (++) (doc: "append") concat
Scala List (::) or, more generically, (+:) (:+) (++) or (:::) or List.concat List.flatten
Scala Array (+:), or (+:=) for (m) (:+), or (:+=) for (m) (++) or Array.concat Array.flatten
Rust Vec<n> Vec::insert, with argument index as 0 Vec::push, docs describe as append. Vec::append Vec::concat
F# List List.insertAt 0 List.insertAt (List.length) List.append List.concat
Common Lisp List cons ? append, nconc (m) (reduce #'append xss)
Mathematica List/any head Prepend Append Join/Catenate/Flatten (variadic) Join/Catenate/Flatten

* This is how we could do join for tuples. But I don't believe we have it currently.

def finJoin : (Fin n → Fin m → α) ≃ (Fin (n * m) → α) :=
(Equiv.curry _ _ _).symm.trans ((finProdFinEquiv).arrowCongr (Equiv.refl _))
Clone this wiki locally