Design Proposal: Support for enumeration

[robin-aws]

(Apologies for the fuzzy description, hopefully this can be refined as we think through the implications)

The recently-added for loop construct only supports iterating over integer values. There is frequently a strong need in Dafny code to define enumerations of values in more flexible or runtime-efficient ways than seq<T> values, such as streams of values, and to perform actions or transformations on each value in sequence (or perhaps even in parallel whenever Dafny supports concurrency :).

There are two parts to this: how to define an enumeration (and I'm using that term to avoid conflict with the existing iterator construct, which is one possible way to define an enumeration but not the only one) and what features we offer to operate on enumerations, such as foreach loops.

Strongly coupled to #413, which talks about having string correctly and efficiently model Unicode encodings: if your abstract string value is a sequence of Unicode scalar values but your runtime representation is, say, UTF-8 bytes, then you really want your code to iterate over “characters” instead of doing random access indexing.

@seebees' standard library PR (dafny-lang/libraries#29) is partially inspired by this need, and could also benefit from more built in support for enumerations.

[robin-aws]

Note for myself: it's also possible this would help users achieve successful verification when working with iteration. That's because a while loop carries a lot less implicit information than a foreach loop of some kind would.

If an enumeration has something like a ghost var of the elements it enumerates, it's likely that Dafny could have axioms for how a foreach is equivalent to a recursive function applied to those elements, and hence make it a lot easier to prove your foreach satisfies a specification using such a function.

[robin-aws]

Another related issue: #424 - it's likely what we want is a built-in way to get an "enumerator" value for a given set<T> (where one such set value is m.Keys when m is a map<K, V>).

[robin-aws]

See also previous RFC and PR that added for loops.

[keyboardDrummer]

What prevents you from enumerating over a collection using a higher order ForEach function that takes a collection and a function to execute for each element?

[robin-aws]

Great question - that's certainly possible now, but a lot more limited than a hypothetical foreach control structure with a block statement body.

The standard library already has higher-order functions like Map (https://github.com/dafny-lang/libraries/blob/master/src/Collections/Sequences/Seq.dfy#L574), which lets you map a pure function over a sequence:

var oneThroughFive := [1, 2, 3, 4, 5];
var sixThroughTen := Map(oneThroughFive, x => x + 5);

But the second argument to Map has to be a pure T ~> R function: it can be partial (i.e. with a requires clause) and read the heap (i.e. with a reads clause), but it has to be defined by an expression rather than a statement, and can't have side effects. So it's not even possible to do this:

var oneThroughFive := [1, 2, 3, 4, 5];
Map(oneThroughFive, x => {   // Invalid syntax - has to be an expression
    print x;
});

However, this is exactly one possible solution I'm strongly considering: supporting "anonymous methods" and "method references" as first class values, so you COULD write ForEach as a library method rather than (or more likely in addition to) having it baked into the language. It's probably one of the more expensive and complex solutions, but also extremely powerful. I also like it because it will likely be extremely useful whenever Dafny supports asynchronous/concurrent execution, because you can naturally use the same construct as the argument to something like ParallelForEach.