In the past, there have been requests to include monadic constructs into Dafny (see e.g. https://github.com/dafny-lang/dafny/pull/455). The main issue with providing native support has been that monads don't fit as naturally into a partly imperative language as Dafny, as they do for purely functional languages. Here, I propose that instead of further embedding monads into the language itself, we simply provide a comprehensive standard library. The PR makes the following contributions:
Extends Wrapper.dfy with more wrappers and more functions for existing wrappers
Introduces a new file Cowrapper.dfy with currently one example, the Coreader cowrapper.
Axiomatises functors in Functors.dfy, monads in Monads.dfy, and comonads in Comonads.dfy
Shows that the examples in Wrapper.dfy are instances of monads, and the examples in Cowrapper.dfy are instances of comonads
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
In the past, there have been requests to include monadic constructs into Dafny (see e.g. https://github.com/dafny-lang/dafny/pull/455). The main issue with providing native support has been that monads don't fit as naturally into a partly imperative language as Dafny, as they do for purely functional languages. Here, I propose that instead of further embedding monads into the language itself, we simply provide a comprehensive standard library. The PR makes the following contributions:
Wrapper.dfywith more wrappers and more functions for existing wrappersCowrapper.dfywith currently one example, the Coreader cowrapper.Functors.dfy, monads inMonads.dfy, and comonads inComonads.dfyWrapper.dfyare instances of monads, and the examples inCowrapper.dfyare instances of comonadsBy submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.