Monadic array init

Stream: lean4

[James Sully]

def Array.initM [Monad m] {n : Nat} (fn : Fin n → m α) : m (Array α) := do
  let mut arr := Array.mkEmpty n
  for i_in_range : i in [:n] do
    have ok : i < n := Membership.get_elem_helper i_in_range rfl
    arr := arr.push (← fn ⟨i, ok⟩)
  return arr

It would be nice to have something this in the standard library. What do you think?

[James Sully]

we have Array.ofFn.{u} {α : Type u} {n : Nat} (f : Fin n → α) : Array α. To be consistent maybe the monadic version should be called ofFnM?

[James Sully]

Technically it should be Applicative I think, but I'm not sure how to write that. I think I'd need Traversable, but that's in mathlib.

[James Sully]

One thing I'm confused about is why n is implicit in ofFn? It seems like in most cases it wouldn't be possible to infer it, and Array.ofFn 10 f seems more ergonomic than Array.ofFn (n := 10) f

[James Gallicchio]

James Sully said:

It would be nice to have something this in the standard library. What do you think?

I'd like to add it to the LeanColls Seq class and put that implementation in the Seq Array instance, if that's alright with you?

[James Sully]

feel free!