monadic `join` for `Vec`

[jamesmckinna]

This issue follows on from #2065 and #2079 , and concerns design choices for join vs. _>>=_, but is/might only be specific to the Monad instance(s) for Vec:

-- Diagonal

diagonal : Vec (Vec A n) n → Vec A n
diagonal [] = []
diagonal (xs ∷ xss) = head xs ∷ diagonal (map tail xss)

module DiagonalBind where
  infixl 1 _>>=_

  _>>=_ : Vec A n → (A → Vec B n) → Vec B n
  xs >>= f = diagonal (map f xs)

  join : Vec (Vec A n) n → Vec A n
  join = _>>= id

The first observation is that since map id is the identity, the definition of join should/could simply be reduced, in place, to

join = diagonal

So, the question is/might be: why go to the trouble of giving it a generic definition (which #2079 at present deprecates in favour of a generic join defined now in Effect.Monad), when the already-defined, and more efficient one, would be 'better'?

The second is that DiagonalBind._>>=_ might (?) better be given a direct recursive definition

  _>>=_ : Vec A n → (A → Vec B n) → Vec B n
  []     >>= f = []
  x ∷ xs >>= f = head (f x) ∷ (xs >>= tail ∘ f)

such that join being then defined generically as _>>= id would make sense... but now, mutatis mutandis, we could instead define diagonal as:

diagonal =  _>>= id where open DiagonalBind

or, if the inlining of id is regarded as problematic, as:

diagonal [] = []
diagonal (xs ∷ xss) = head xs ∷ (xss >>= tail) where open DiagonalBind

Would any of these observations yield actual improvements, though?

[jamesmckinna]

Have now propagated the first idea through #2079.
The second seems to have some 'interesting' questions about optimisation, in terms of when the various tails of xss in diagonal xss, resp. xs >>= f might be computed, so I have left things as they are for now.