SequencesExt!Fold[Left|Right] over domain of sequence

[lemmy]

I've encountered situations where I needed to fold (either left or right) over the indices of a sequence. In other words, the operation involves both the current element and its index within the input sequence. Currently, to overcome this limitation, we must resort to folding over a sequence that represents the domain of the original sequence:

    FoldLeft(LAMBDA acc, idx: 
                IF log[idx].something = "foobar" /\ idx < someBound
                THEN {log[idx]} \cup acc
                ELSE acc,
                {}, [ i \in DOMAIN log |-> i])

Preferred:

    FoldLeftDomain(LAMBDA acc, idx: 
                IF log[idx].something = "foobar" /\ idx < someBound
                THEN {log[idx]} \cup acc
                ELSE acc,
                {}, log)

A more elegant, though backward-incompatible, approach could involve increasing the arity of op to include acc, e, and idx:

    FoldLeft(LAMBDA acc, e, idx: 
                IF e.something = "foobar" /\ idx < someBound
                THEN {e} \cup acc
                ELSE acc,
                {}, log)

Thoughts?

[muenchnerkindl]

Makes sense, given that from the index you can recover the element of the sequence at that index. Your FoldLeftDomain can be defined as

FoldLeftDomain(op(_, _), base, seq) == 
MapThenFoldSet(LAMBDA x,y : op(y,x), base,
                 LAMBDA i : i,
                 LAMBDA S : Max(S),
                 DOMAIN seq)

(and similarly for FoldRight). Not sure if making op a ternary operation is such a good idea, as it introduces the invariant e = seq[idx], which may be non-obvious. Are you suggesting replacing the current operators FoldLeft and FoldRight?

[lemmy]

microsoft/CCF#6053