Do-notation desugaring to monadic Bind #455

osavaryb · 2019-12-09T15:56:27Z

Feature review.

"do { Expression}" allows for monadic bind "<-" to appear.
"x <- e1; e2" desugars to "Bind(e1, x => e2)"
"P x <- e1; e2" desugars to "match e1
P x => e2"

Both MonadicBindExpr and DoNotationExpr are ConcreteSyntaxExpression (i.e. they disappear after the resolving phase)

…refix in next pass

…ll test, then resolve

…it makes sense to switch to a do-notation flag for expression instead

…on, but resolver throw error if they are find outside of do-notation. Still need to fill in the resolving of MonadicBindExpr

…n calc statement (otherwise BinaryExpr may captures the op

…ression

…xpr, will do more testing

robin-aws · 2019-12-09T16:05:59Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: 8b6e83b
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2019-12-09T16:16:10Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: e219a5f
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

… ResolvedExpression is set.

robin-aws · 2019-12-12T15:29:26Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: eb137ff
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

osavaryb · 2019-12-12T15:56:38Z

Some of the test cases are failing at the moment due to "do" being used as a function/method name (some of these fails at the use of the function rather than at declaration). I could try to make it always fail at declaration, or try to fix the parser so that it doesn't get tripped by non-blocks' "do"

RustanLeino · 2019-12-12T23:00:04Z

Thanks for the initiative to add monadic binds to Dafny. I would like to see these, but think they should be more analogous to the :- support that was added to Dafny this year. In particular:

I don't see a need for a do block to go around these monadic binds.
The introduction of the variables in the LHS of the construction should use var, like let expressions.
Instead of a new <- operator for binding, use :-.
Resolve the Bind function as a member of the source expression's type.

So, an expression (which can occur anywhere an expression can occur, not just inside some do block)

var x :- E; Body

where x is a bound variable and E and Body are expressions, has the meaning

E.Bind(x => Body)

To distinguish this construct from the similar :- construct in Dafny today, I propose that the resolve look at the type of E to see:

Does it have a Bind member? If so, treat as monadic bind.
Does it have an IsFailure member? If so, treat as the error-result mechanism.

If neither or both applies, some error should be generated. If it cannot be determined from what's currently known about the type of E during this stage of type inference/checking, then I think an error should be produced.

The resolution of the types for the parameters passed to Bind, IsFailure, PropagateFailure, and Extract can be handled after desugaring according to the two bullets above. However, we can get better error messages if we don't just rely on the desugaring. I have found some of the current error-result error messages unclear, and I would rather that we do more checking before doing the syntactic rewrite.

I'm suggesting the monadic-bind rewrite use just =>, which gives a total arrow. If we ever have a need for a partial arrow (or even a read-effects arrow), then we'd have to invent more syntax.

…ng let-binding depending of the context, as discussed in PR 455

robin-aws · 2019-12-13T20:19:23Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: 38f3c99
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2019-12-13T20:35:02Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: 4de17f6
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-01-06T20:17:03Z

Some thoughts on @RustanLeino's comments.

Rather than introduce another PartialBind method, could we make the signature of Bind always accept a partial function, and just expect that the precondition will often be requires true?

Split Bind up into several functions, akin to the IsFailure, PropagateFailure, and Extract functions that the "exception handling" :- looks for.

This would reduce the power of Monads quite a lot so I don't think it would be a great solution. I can't think of the right set of functions to support classic List Monad, for example, which applies the bound function to each element in the list.

Inline Bind at the usage site of :-, if the definition of Bind is statically known.

This strikes me as fragile, since refactoring in what should be a semantically-equivalent way would break verification very easily.

I'm also starting to think that we shouldn't try to retcon the existing :- syntax as monadic, as tempting as it is. It's a pretty fundamental problem that the block following a :- statement can already be more powerful than the traditional argument to Bind, since it can read and modify the heap. One possibility would be to represent such blocks as already implementing a monadic type, similar to the IO or State type classes from Haskell. For that to work you'd really need monad transformers, though, so that you could stack an additional monad like Option on top of a class method. We'd likely need some more syntax help for mixing monads and "methods" like that.

On a similar subject, will we end up missing a lot of the appeal of monads if we can't express the monad concept as a trait or something similar, rather than just a baked-in implicit interface? It means we can't have user code that implements monad transformers, for example.

RustanLeino · 2020-01-09T22:37:39Z

There are many good comments above and in the discussions linked from the above. Syntactic issues aside, I think we first need to find a good way to deal with the partial expressions that require preconditions above. Should we:

Allow users to provide partial functions as either named functions or as lambda expressions with explicit requires clauses? If so, then we can support both Bind and PartialBind or, as @robin-aws suggested, make Bind always be partial.
Allow users to provide partial functions and, as @samuelgruetter mentioned above, invent an improved syntax for explicitly giving them in the sugared monadic form?
Allow users to provide partial functions and, as @samuelgruetter dream of above, automatically infer these preconditions?
Disallow partial functions altogether?

I think we need to resolve this question to go on. Overall, the inclusion of these monadic constructs seems a bit premature at this time. Do we have any interesting use cases that someone would actually like to write? Then, we could let those inform the design. Alternatively, we could go for a restrictive design (I suggest the one in my first comment in the discussion above), so that we can play with it, and then hope to figure out where to go from there?

Opinions?

…n (which get forwarded to the desugared lambda-expression). Rerun coco, add a test case (from Rustan) in MonadicBind

robin-aws · 2020-01-20T16:22:00Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: ca5671e
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-01-27T16:31:33Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: d798a77
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

RustanLeino

I mention my hesitation about the no-LHS version of :-, but maybe that can be resolved later.
All other comments pertain to code style. Please update the settings in your IDE accordingly.

Source/Dafny/Dafny.atg

Source/Dafny/Resolver.cs

Test/monadic/MonadicBind.dfy

RustanLeino · 2020-02-06T19:53:55Z

Test/monadic/MonadicBind.dfy

@@ -0,0 +1,77 @@
+// RUN: %dafny /compile:0 "%s" > "%t"


I would like to see more tests: some that don't use specifications, some that use reads.
Also, since these are expected to verify, there might as well be some compiling tests (so change to /compile:3 and add a Main).

robin-aws · 2020-02-06T21:42:52Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: 9839e71
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-02-16T19:41:42Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: 93662b6
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-02-16T19:54:05Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: b9d5af5
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-02-16T20:15:37Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: 23fe3f6
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-02-17T22:44:01Z

AWS CodeBuild CI Report

CodeBuild project: Dafny
Commit ID: c7215ee
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

robin-aws · 2020-02-19T19:55:43Z

I still have reservations about edge cases in ambiguity between LetOrFail :- and Monadic :-. I'd like to have a closer look and see if I can break this before it's merged. :)

samuelgruetter · 2020-02-20T05:31:20Z

Test/monadic/MonadicBind.dfy

+
+class Cell {
+  var data: int
+}


What is class Cell used for?

samuelgruetter · 2020-02-20T05:32:26Z

Test/monadic/MonadicBind.dfy

+      case Cons(x, _) => Some(x)
+}
+
+function method G(list: List): Option {


You're using List and Option without giving a type argument. I'd also test it with List<A> and Option<A>.

samuelgruetter · 2020-02-20T05:38:14Z

Test/monadic/MonadicBind.dfy

+  var cdr :- Tail(list);
+   var cddr :- Tail(cdr);
+  Head(cddr)
+}


All the examples involving generics go from a List<T> to List<T>, where T remains the same. I'd also test an example where the function you pass to Bind goes from List<T> to List<U>, where T and U are different, and also one where it goes from Foo<T> to Bar<U>, just to see how this interacts with type inference.

samuelgruetter · 2020-02-20T05:40:44Z

Test/monadic/MonadicBind.dfy

+  {
+    if this == None then None else f(get)
+  }
+}


You're intending to implement quite a generic feature, so it would be nice to not only test it for the Option monad, but also for some other monad, maybe for the State monad? Or what other monads are people intending to use in Dafny?

+1 - this also needs to test the case where a type defines both Bind and IsFailure/PropagateFailure/Extract, since the syntax is ambiguous there

RustanLeino · 2021-01-27T22:52:18Z

Upon further consideration, we will not include this feature in the language at this time. There are some issues to be resolved around how to write verifying code with the functions that are being generated.

Olivier Savary Belanger added 17 commits December 2, 2019 14:51

First pass at adding monadic notation, regenerated p/s. Will remove p…

8ee5040

…refix in next pass

Second pass for parser with IsDoBind lookahead and removed suffix. Wi…

cd3bed0

…ll test, then resolve

Fill in printer for unresolved do notation, will start resolving

391fab7

Parsing let-binding eagerly in Do-notation, will think a bit more if …

521c900

…it makes sense to switch to a do-notation flag for expression instead

Change atg, monadic binds are now accepted by parsers in any expressi…

7c9a971

…on, but resolver throw error if they are find outside of do-notation. Still need to fill in the resolving of MonadicBindExpr

Progress on resolving monadic bind (variable case)

8f9e151

Resolving var case, type checking not quite there yet

6cc21c5

Raised donotation to top level expression to make it work correctly i…

b5d29d7

…n calc statement (otherwise BinaryExpr may captures the op

CI before making DoNotationExpr and MonadicBindExpr ConcreteSyntaxExp…

5216f9d

…ression

Made MonadicBindExpr and DoNotationExpr subclasses of ConcreteSyntaxE…

6d395dd

…xpr, will do more testing

Fill in resolution for pattern on the lhs of a monadic bind

6f05c5e

Clean up resolver, add documentation for monadic bind syntax

f560013

Rerun madoko

b4226ce

pre commit

e89ea2d

Merge remote-tracking branch 'upstream/master'

8be2753

Merge branch 'master' into monadic-syntax

8b6e83b

rerun madoko

e219a5f

Fix cloner: DoNotationExpr should be cloned as unresolved, even after…

eb137ff

… ResolvedExpression is set.

osavaryb mentioned this pull request Dec 12, 2019

Ordered, nested matching of datatypes and constants #458

Merged

Olivier Savary Belanger added 2 commits December 13, 2019 15:12

Remove DoNotation and MonadicBind from grammar, rerun coco

8004b32

Trying to resolve :- (LetOrFail) as Monadic Bind or as failure-handli…

38f3c99

…ng let-binding depending of the context, as discussed in PR 455

Had forgotten to include the Printer in previous commit

4de17f6

..

b211751

Added support for requires and reads clause in monadic-bind expressio…

ca5671e

…n (which get forwarded to the desugared lambda-expression). Rerun coco, add a test case (from Rustan) in MonadicBind

Olivier Savary Belanger added 2 commits January 27, 2020 10:09

Merge remote-tracking branch 'upstream/master'

4fa651b

Rerun coco after merging with master

d798a77

RustanLeino requested changes Feb 6, 2020

View reviewed changes

Coding style cleanup

9839e71

Olivier Savary Belanger added 2 commits February 9, 2020 13:22

Spacing

93662b6

Added Main to test, made :- with No-Lhs optional

b9d5af5

Fix MonadicBind.dfy.expect

23fe3f6

Update Resolver.cs

c7215ee

RustanLeino approved these changes Feb 19, 2020

View reviewed changes

robin-aws self-requested a review February 19, 2020 19:55

samuelgruetter reviewed Feb 20, 2020

View reviewed changes

Test/monadic/MonadicBind.dfy

class Cell {

var data: int

}

Copy link

Collaborator

samuelgruetter Feb 20, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is class Cell used for?

samuelgruetter reviewed Feb 20, 2020

View reviewed changes

RustanLeino added the status: implemented Candidate feature available for experimentation label Jun 26, 2020

RustanLeino closed this Jan 27, 2021

robin-aws mentioned this pull request Aug 6, 2021

Dafny Standard Library dafny-lang/libraries#7

Merged

stefan-aws mentioned this pull request Feb 6, 2023

Extending wrappers & introducing functors, monads, comonads, and cowrappers dafny-lang/libraries#80

Draft

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Do-notation desugaring to monadic Bind #455

Do-notation desugaring to monadic Bind #455

osavaryb commented Dec 9, 2019

robin-aws commented Dec 9, 2019

robin-aws commented Dec 9, 2019

robin-aws commented Dec 12, 2019

osavaryb commented Dec 12, 2019

RustanLeino commented Dec 12, 2019

robin-aws commented Dec 13, 2019

robin-aws commented Dec 13, 2019

robin-aws commented Jan 6, 2020

RustanLeino commented Jan 9, 2020

robin-aws commented Jan 20, 2020

robin-aws commented Jan 27, 2020

RustanLeino left a comment

RustanLeino Feb 6, 2020

robin-aws commented Feb 6, 2020

robin-aws commented Feb 16, 2020

robin-aws commented Feb 16, 2020

robin-aws commented Feb 16, 2020

robin-aws commented Feb 17, 2020

robin-aws commented Feb 19, 2020

samuelgruetter Feb 20, 2020

samuelgruetter Feb 20, 2020

samuelgruetter Feb 20, 2020

samuelgruetter Feb 20, 2020

robin-aws Feb 23, 2020

RustanLeino commented Jan 27, 2021

Do-notation desugaring to monadic Bind #455

Do-notation desugaring to monadic Bind #455

Conversation

osavaryb commented Dec 9, 2019

robin-aws commented Dec 9, 2019

AWS CodeBuild CI Report

robin-aws commented Dec 9, 2019

AWS CodeBuild CI Report

robin-aws commented Dec 12, 2019

AWS CodeBuild CI Report

osavaryb commented Dec 12, 2019

RustanLeino commented Dec 12, 2019

robin-aws commented Dec 13, 2019

AWS CodeBuild CI Report

robin-aws commented Dec 13, 2019

AWS CodeBuild CI Report

robin-aws commented Jan 6, 2020

RustanLeino commented Jan 9, 2020

robin-aws commented Jan 20, 2020

AWS CodeBuild CI Report

robin-aws commented Jan 27, 2020

AWS CodeBuild CI Report

RustanLeino left a comment

Choose a reason for hiding this comment

RustanLeino Feb 6, 2020

Choose a reason for hiding this comment

robin-aws commented Feb 6, 2020

AWS CodeBuild CI Report

robin-aws commented Feb 16, 2020

AWS CodeBuild CI Report

robin-aws commented Feb 16, 2020

AWS CodeBuild CI Report

robin-aws commented Feb 16, 2020

AWS CodeBuild CI Report

robin-aws commented Feb 17, 2020

AWS CodeBuild CI Report

robin-aws commented Feb 19, 2020

samuelgruetter Feb 20, 2020

Choose a reason for hiding this comment

samuelgruetter Feb 20, 2020

Choose a reason for hiding this comment

samuelgruetter Feb 20, 2020

Choose a reason for hiding this comment

samuelgruetter Feb 20, 2020

Choose a reason for hiding this comment

robin-aws Feb 23, 2020

Choose a reason for hiding this comment

RustanLeino commented Jan 27, 2021