Array.join vs Array.flatten

Stream: batteries

[Eric Wieser]

docs#Array.join looks the same as docs#Array.flatten to me:

/--
`O(|join L|)`. `join L` concatenates all the arrays in `L` into one array.
* `join #[#[a], #[], #[b, c], #[d, e, f]] = #[a, b, c, d, e, f]`
-/
@[inline] def join (l : Array (Array α)) : Array α := l.foldl (· ++ ·) #[]

/-- Joins array of array into a single array.

`flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` = `#[a₁, a₂, ⋯, b₁, b₂, ⋯]`
-/
def flatten (as : Array (Array α)) : Array α :=
  as.foldl (init := empty) fun r a => r ++ a

Which name should be kept?

[Eric Wieser]

(mentioned previously here)

[Kyle Miller]

join is perhaps the more common name for this monadic operation, though it appears Scala might call it flatten.

My vote would be for join.

If we wanted Lean to be friendly in a Ruby sense, I know there is an aliasing mechanism where we could make Array.flatten be an alias for Array.join — so it would elaborate as Array.join — but I'm not sure that's exposed in any command (the Lean 3 export command would let you rename identifiers, but Lean 4's doesn't). I also seem to remember there being some inconsistencies with how aliases are handled, but having more aliases could help exercise this feature.

[Eric Wieser]

Join matches List.join too, which is nice; though to make things more confusing, .flatten was upstreamed to core

[Joe Hendrix]

I think Array.join should be the exclusive one kept and upstreamed to core. I don't see any reason that can't be done prior to the next release.

[Joe Hendrix]

We could make Array.flatten a deprecated abbreviation for Array.join.

[Mario Carneiro]

I think join is a bit of a monad-brained name, it is not as natural from procedural programming languages. From the name alone I think someone would guess that it is the ++ operation

[Mario Carneiro]

(I have also thought the same about List.bind, which would probably be called something more like flatMap in a javascriptish language)

[Kim Morrison]

(When I first came to Lean it took me a while to stop writing flatMap, which was one of the most common tokens in the Scala code I used to write...)

[François G. Dorais]

(Aside: is flatMap in Scala join or bind?)

[Ruben Van de Velde]

flatMap is the monad operation, so I guess bind

[Mario Carneiro]

bind

[François G. Dorais]

I don't see any issue with having both so long as one is an alias pointing to the other. That way a quick hover will reveal they are synonyms.

Of course, it's debatable which should be the root. My preference is for the generic name (join) to be an alias for the specialized name (flatten).

[James Gallicchio]

François G. Dorais said:

(Aside: is flatMap in Scala join or bind?)

Scala's join is flatten, which nicely emphasizes their relationship. flatMap is map followed by flatten.

[Kyle Miller]

For what it's worth, I think the monad word "join" comes from generalizing the example of List.join to all monads.

[Kyle Miller]

I'm not sure what's it's most often called the the math literature, but it's the "multiplication" law of the monad, denoted by $\mu$. Just mentioning this to say that neither "join" nor "flatten" is the general word, at least as the math is concerned.

[Mario Carneiro]

I always assumed it was the other way around. It would be great to track down the history of the naming of Monad.join and List.join in haskell

[Kim Morrison]

Doesn't Haskell use concat for List.join?

[Mario Carneiro]

According to https://en.wikipedia.org/wiki/Monad_(functional_programming)#History , the first use of monads in FP is by Moggi (1989 / 1991), but he is using the standard mathematical notations only (i.e. greek letters) and does not name the operations AFAICT; and the next reference is to monads in Haskell when they were overhauling their IO system in 1993 and that paper uses bindIO for the first time but not join

[Mario Carneiro]

there is no explanation of why the name "bind" is chosen, it may predate the paper

[Mario Carneiro]

there is also no mention of "Monad" as a typeclass, I think this may also predate typeclasses

[Mario Carneiro]

lol @ https://wiki.haskell.org/Monad_tutorials_timeline

[Mario Carneiro]

Scott Morrison said:

Doesn't Haskell use concat for List.join?

Indeed Haskell's list type has concat and concatMap, although of course you can also use bind and join coming from the Monad implementation. In Haskell I think the names tend to be different on specialized types because they don't have dot-notation for disambiguation (you can also use qualified imports but this is usually not used for things in Base)

[James Sully]

Some people might incorrectly expect [[[1]]].flatten = [1]

[Eric Wieser]

That view is probably quickly dispelled when they realize that #[#[1, 2], 3] is a type error.