Introduce disjunctive loops
Currently, a loop in a semidet context effectively conjoins all the tests appearing in the body of the loop, a bit like all in Haskell. There should be a version like that that disjoins them, like any in Haskell.
Currently, the library defines:
pub def {test} all(p:{test}(T), xs:_(T)) {
for ?x in xs {
p(x)
}
}
but due to the lack of disjunctive loops, the definition of any looks like this:
pub def {test} any(p:{test}(T), xs:_(T)) {
[?x | ?xs] = xs
(p(x) | any(p, xs))
}
Something like this?
def {test} any(p:{test}(X), xs:list(X)) {
for some ?x in xs {
p(x)
}
}
Looks good! Then maybe we should change for to be for all?
I was thinking for each because it must hold for "each". I think that contrasts nicely with "some".
It could also be for any and for all. I suppose it depends which word we want to promote to a contextual keyword.
Yes, grammatically (in English), for each and for some work well.
Any ideas for a disjunctive version of do loops? Maybe keep do as the det version, and use all and any as semidet versions? Only downside is that makes those keywords, but do all and do any don't read well.
We could do similarly with for: keep as is for the det version, and add for each and for some as the semidet versions. That would also be closer to being backward compatible.
I think by default, people would assume the usual det semantics. So do and for being the det loops makes sense to me.
do some could work for the semi-det do. Though, it is a little unsatisfactory, I feel. Perhaps partial do (and partial for)?
some and any don't imply an ordering of execution. Perhaps something like first could be used (for first ?x in xs, do first) would make the ordering clear?
Yeah, linguistically, do some isn't great, but I think it's better than partial do, because partial doesn't indicate that we're changing the sense of the treatment of partial calls. I do like for first and do first.
So I think the conclusion is to keep the meaning of for and do, but introduce for first and do first as indicating that the loop terminates in success as soon as the loop body succeeds, and in failure if it never does. That has the virtue of being concise, simple, and fully backward compatible. In contrast, for and do terminates in failure as soon as the loop body fails, and in success if it never does.
The awkward thing about do first is that reassigned variables in the loop body revert on failure, so if we want to have that make sense, I think we'll need to have a separate construct in the loop to update variables for loop iterations, and not have those revert when the loop body fails. Maybe something like a special iterate {...} loop body statement, which can be placed anywhere in the loop.
That's a good point on iteration in a do-loop. The iteration can't "progress" if variables get rolled back. We would need to be careful with semi-det fors as they would translate into do loops under-the-hood.
I'm not sure I understand the iterate statement. Is that intended to wrap the parts that get rolled back on failure?
Exactly. The loop body would execute until success or failure or break, then in any case the iterate statement(s) would be executed to prepare for the next iteration. On failure, assignments made by body statements would be reverted, then the iterate statements would execute (and not be rolled back). If the iterate statements fail, the loop terminates. This needs to be carefully thought out.