sequence comprehensions are ugly

[jonhnet]

I get the desire to recycle the lambda, but the result is much uglier than set/map comprehensions. I have to read:
seq(c.mapCount, i requires 0<=i<c.mapCount => v.maps[i].Keys)
which means I have to talk about the sequence bound twice, with a bunch of unexpected boilerplate in the lambda. It would be much prettier to have a specialized syntax, a la map comprehensions:
seq i | mapCount :: v.maps[i].Keys
... the count parameter information both communicates the sequence length to the comprehension, but also provides the implicit predicate on the uses of i after the qsep.

This particular syntax is a little unfortunate because the thing after the "such-that" bar is a number, not a predicate (since sequences can't have holes in them), which is inconsistent with other syntax. But it's much better than the existing syntax.
Here's an alternative:
seq i len mapCount :: v.maps[i].Keys
In this syntax, 'len' is a reserved word. It avoids overloading the such-that bar with a non-predicate.

[robin-aws]

Couldn't agree more there's room for improvement. What about something like:

seq(c.MapCount) i :: v.maps[i].Keys

[jonhnet]

Oh, I like that syntax quite a bit. The parens suggest that the length is a parameter of the comprehension constructor (and it is!), and then the i :: syntax is the usual way to introduce a bound variable. Lovely.

[robin-aws]

I just realized we could use this for array comprehensions as well, which have the same issue. E.g.:

var identityMatrix = new int[5][5] i, j :: if i == j then 1 else 0;

[RustanLeino]

Thanks for the thoughts about this. In these two places, the language checks the given function to have a sufficiently large range. Your comments above suggest different syntax for that. Another alternative would be to special-case these two places to let Dafny automatically restrict the range, provided the argument is a lambda expression.

For example, the user writes

seq(n, i => f(i))

and Dafny automatically turns this into

seq(n, i requires 0 <= i < n => f(i))

(and analogously for array allocation). The requires 0 <= i < n gets added before any other user-declared requires clauses of the lambda expression.

If the function value is not a lambda expression, no rewrite takes place. For example, if you write

seq(n, (i => F(i))   // note the additional parentheses

or

seq(n, F)

then no automatic rewrite happens.

Would this (a) satisfy the desire for a simplified syntax, and (b) be a shameless language design?

[jonhnet]

It would be an improvement, for sure.

But if you're asking for opinions, it's a lot uglier than the map & set comprehension syntaces. robin-aws's suggestion above looks a lot more consistent with other dafny comprehensions; I vastly prefer it.

[robin-aws]

I may be slightly biased :) but I agree.

I also worry that having the automatic rewrite will make for a very confusing user experience, if they refactor the lambda in a sequence comprehension and it suddenly no longer verifies for no obvious reason. If we want to make a very specific combination of syntax work nicely, we might as well make it a more distinct syntax with its own distinct rules.

[tjhance]

Just popping in to say I just ran into yet another novice user getting tripped up because they didn't know to put the requires clause.

[robin-aws]

@jonhnet / @tjhance / @tchajed - I've just posted a similar but more general alternative proposal for sequence comprehensions here, would absolutely love any thoughts you have!

[davidcok]

I will add my vote: the fact that seq(n, i => f(i)) does not work and needs the extra requires clause is confusing and ugly.
Some fix is sorely needed. The above construction is too common.

[robin-aws]

@davidcok I'm happy to say that we have proper "sequence comprehensions" designed and ready to implement in the near future now. Using that form, the running example here would be something like:

seq m <- v.maps :: m.Keys

[davidcok]

Commented there. seq(n, F) is now what?

[robin-aws]

Replied there :) It's not a complete replacement but can be used most of the time instead.