best practices: iteration over array items with indices

Stream: general

[Michael Rothgang]

What's the most idiomatic way of iterating over all array items with their corresponding index? Something akin to Python's enumerate(array, 1).
One way is the following, but I can't help wondering if there's something better.

  let mut index := 0
  for item in array do
    -- work with index and item
    index := index + 1

[Eric Taucher]

Take a look at the Lean tutorial Functional Programming in Lean, in particular the section titled Proving Termination.

Yes you may have to read the entire tutorial to understand the noted section but if you plan to create programs with Lean it is worth the effort even if it takes a few days or more.

[Damiano Testa]

I think that you might get some suggestions from this topic.

[Michael Rothgang]

Thanks to both of you! I'm going with

  for h : idx in [:array.size] do
    let item := array[idx]
    -- work with index and item

[Jz Pan]

docs#Array.zipWithIndex

for (item, index) in array.zipWithIndex do
  ...

(untested)

[Eric Wieser]

Strangely, docs#List.enum puts the pairs in the opposite order

[Kim Morrison]

It is possibly not too late to fix that. I'm starting soon on making the List/Array APIs more consistent. Besides the churn, does anyone see a downside of flipping List.enum?

[Kim Morrison]

(I recall finding the current order slightly unergonomic recently, but can't remember where.)

[Yakov Pechersky]

The nice thing about the current order is that you get an obvious lex order on the elements of the attach subtype

[Eric Wieser]

enum also matches the order of Python's enumerate

[Kim Morrison]

Perhaps the only reason for the disparity is that it is hard to say "indexWithZip" because of English word order. :-)

[Eric Wieser]

Taking a step back: is array.zipWithIndex actually an efficient way to do this looping? In python, enumerate returns an iterator, not an list - presumably allocating an Array of pairs is wasteful here?

[Thomas Zhu]

What about the best practice for tracking indices in a general for-in loop, such as over MLList?

[Jz Pan]

Eric Wieser said:

Taking a step back: is array.zipWithIndex actually an efficient way to do this looping?

Since array.zipWithIndex is constexpr (C++ sense), the best bet is that a very good optimize compiler will reorder loop operations.

In python, enumerate returns an iterator, not an list - presumably allocating an Array of pairs is wasteful here?

Perhaps we should add a array.forWithIndexM.

[Kim Morrison]

I think we could even provide a ForIn instance that returns pairs.