feat: Functional constructs for methods#29
feat: Functional constructs for methods#29seebees wants to merge 2 commits intodafny-lang:masterfrom
Conversation
Being able to express logic with map and filter simplifies the expression of an implementation. However doing this iteration in a method requires a loop. Loop invariants are hard.
seebees
force-pushed
the
map-with-result
branch
from
5883ab4 to
51f5954
Compare
robin-aws
left a comment
robin-aws
left a comment
There was a problem hiding this comment.
I really like the general idea here. Added some initial thoughts and I'm going to play with it a bit myself in the meantime.
| predicate Ensures(a: A, r: R) | ||
| } | ||
|
|
||
| trait {:termination false} NothingToRequire<A> |
There was a problem hiding this comment.
Perhaps TotalAction instead, to align with -> being a "total" function?
Once you add Reads you'll want that to be just {} here too. You could then have a PartialAction which reads nothing but CAN require something.
| { | ||
| method Invoke(a: A) | ||
| returns (r: R) | ||
| requires Requires(a) |
There was a problem hiding this comment.
I think you mentioned you were aware already offline, but we'll need a function Reads(a: A): set<object> too.
There was a problem hiding this comment.
Yup. And I think we can have some nice helpers so people can mix in and not have so much typing :)
There was a problem hiding this comment.
What about having a "modifies" first ?
| s: seq<A> | ||
| ) | ||
| returns (res: seq<R>) | ||
| requires forall i | i in s :: action.Requires(i) |
There was a problem hiding this comment.
(Just food for thought as I THINK we can address this later) - I wonder if we could make this less restrictive, so later elements could depend on earlier ones. Something like:
requires |s| > 0 ==> action.Requires(s[0])
requires forall i | 1 <= i < |s| ::
(exists r | action.Ensures(s[i - 1], r) ==> action.Requires(s[i]))
There was a problem hiding this comment.
This looks a bit suspicious. Should it be parenthesized differently?
requires forall i | 1 <= i < |s| ::
((exists r | action.Ensures(s[i - 1], r)) ==> action.Requires(s[i]))
Which is then equivalent to
requires forall i | 1 <= i < |s| ::
(forall r :: action.Ensures(s[i - 1], r) ==> action.Requires(s[i]))
?
| var maybeR := action.Invoke(s[i]); | ||
| if maybeR.Failure? { | ||
| return Failure(maybeR.error); | ||
| } |
There was a problem hiding this comment.
Worth a comment about how you're having to work around the issue with :- here?
| ensures | ||
| res.Success? | ||
| ==> | ||
| exists a | a in s :: action.Ensures(a, Success(res.value)) |
There was a problem hiding this comment.
Don't you want to make this stronger and say it's the FIRST such element?
There was a problem hiding this comment.
Yes, I do! But I did not know how.
There was a problem hiding this comment.
exists i | 0 <= i < |s| :: action.Ensures(s[i], Success(res.value)) && forall j | 0 <= j < i ==> exist f | action.Ensures(s[i], Failure(f))
Maybe there is a better way?
| return rs, parts; | ||
| } | ||
|
|
||
| method FlatMapWithResult<A, R, E>( |
There was a problem hiding this comment.
It's definitely bothering me that we need this and can't just use Flatten(MapWithResult(action, s)) but I know you warned me it's not that simple. Let me play around with it a bit. :)
There was a problem hiding this comment.
You should. It may be that with #28 many things are easier.
The difficulty was crossing the flatten boundary.
I will also note, that there may be a runtime efficiency "thing" in here.
If one or the other of these is easier to fold into a lazy seq creation,
then we should go with that one :)
4 participants
Being able to express logic with map and filter
simplifies the expression of an implementation.
However doing this iteration in a method requires a loop.
Loop invariants are hard.
@robin-aws here is the implementation we have been talking about.
Obviously we need examples before we could merge,
but this can start a discussion about if/how such constructs could be used or simplified.