Extending wrappers & introducing functors, monads, comonads, and cowrappers

examples/Wrappers.dfy

@@ -10,6 +10,9 @@ include "../src/Wrappers.dfy"
 
 module Demo {
   import opened Wrappers
+  import opened Wrappers.Option
+  import opened Wrappers.Result
+  import opened Wrappers.Outcome
 
   // ------ Demo for Option ----------------------------
   // We use Option when we don't need to pass around a reason for the failure,
@@ -60,7 +63,7 @@ module Demo {
   // Sometimes we want to go from Option to Result:
   method FindName(m: MyMap<string, string>) returns (res: Result<string, string>) {
     // Will return a default error message in case of None:
-    res := m.Get("name").ToResult();
+    res := ToResult(m.Get("name"));
     // We can also match on the option to write a custom error:
     match m.Get("name")
     case Some(n) => res := Success(n);

src/Collections/Arrays/BinarySearch.dfy

@@ -9,7 +9,7 @@ include "../../Wrappers.dfy"
 include "../../Relations.dfy"
 
 module BinarySearch {
-  import opened Wrappers
+  import opened Wrappers.Option
   import opened Relations
 
   method BinarySearch<T>(a: array<T>, key: T, less: (T, T) -> bool) returns (r: Option<nat>)

src/Collections/Maps/Imaps.dfy

@@ -12,7 +12,7 @@
 include "../../Wrappers.dfy"
 
 module {:options "-functionSyntax:4"} Imaps {
-  import opened Wrappers
+  import opened Wrappers.Option
 
   function Get<X, Y>(m: imap<X, Y>, x: X): Option<Y>
   {

src/Collections/Maps/Maps.dfy

@@ -12,7 +12,7 @@
 include "../../Wrappers.dfy"
 
 module {:options "-functionSyntax:4"} Maps {
-  import opened Wrappers
+  import opened Wrappers.Option
 
   function Get<X, Y>(m: map<X, Y>, x: X): Option<Y>
   {

src/Collections/Sequences/Seq.dfy

@@ -20,7 +20,8 @@ include "../../Relations.dfy"
 
 module {:options "-functionSyntax:4"} Seq {
 
-  import opened Wrappers
+  import opened Wrappers.Option
+  import opened Wrappers.Result  
   import opened MergeSort
   import opened Relations
   import Math
@@ -613,7 +614,7 @@ module {:options "-functionSyntax:4"} Seq {
 /* Applies a function to every element of a sequence, returning a Result value (which is a 
    failure-compatible type). Returns either a failure, or, if successful at every element, 
    the transformed sequence.  */
-  function {:opaque} MapWithResult<T, R, E>(f: (T ~> Result<R,E>), xs: seq<T>): (result: Result<seq<R>, E>)
+  function {:opaque} MapWithResult<T, R(!new), E(!new)>(f: (T ~> Result<R,E>), xs: seq<T>): (result: Result<seq<R>, E>)
     requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i])
     ensures result.Success? ==>
       && |result.value| == |xs|

src/Comonad.dfy

@@ -0,0 +1,172 @@
+// RUN: %dafny /compile:0 "%s"
+
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT 
+*******************************************************************************/
+
+include "Functor.dfy"
+include "Cowrappers.dfy"
+
+abstract module {:options "-functionSyntax:4"} Comonad refines Functor {
+  /* Structure  */
+  type F(!new)<T(!new)>
+
+  function Extract<T(!new)>(w: F<T>): T
+
+  function Duplicate<T(!new)>(w: F<T>): F<F<T>>
+
+  /* Naturality */
+  lemma LemmaExtractNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, w: F<S>)
+    requires EquivalenceRelation(eq)
+    ensures eq(f(Extract(w)), Extract(Map(f)(w)))
+
+  lemma LemmaDuplicateNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, w: F<S>)
+    requires EquivalenceRelation(eq)
+    ensures EquivalenceRelation(Equal(eq))
+    ensures Equal(Equal(eq))(Duplicate(Map(f)(w)), Map(Map(f))(Duplicate(w)))
+
+  /* Counitality and Coassociativity */
+  lemma LemmaCoUnitalityExtract<T(!new)>(eq: (T, T) -> bool, w: F<T>)
+    requires EquivalenceRelation(eq)
+    ensures && Equal(eq)(Map(Extract)(Duplicate(w)), w)
+            && Equal(eq)(w, Extract(Duplicate(w)))
+
+  lemma LemmaCoAssociativityDuplicate<T(!new)>(eq: (T, T) -> bool, w: F<T>) 
+    requires && EquivalenceRelation(eq)
+             && EquivalenceRelation(Equal(eq))
+             && EquivalenceRelation(Equal(Equal(eq))) 
+    ensures Equal(Equal(Equal(eq)))(Map(Duplicate)(Duplicate(w)), Duplicate(Duplicate(w)))
+}
+
+abstract module {:options "-functionSyntax:4"} CoreaderRightComonad refines Comonad {
+  import Cowrappers.Coreader
+
+  type X(!new)
+
+  function eql(x: X, y: X): bool
+
+  lemma LemmaEquiv()
+    ensures EquivalenceRelation(eql)
+
+  /* Functor structure */
+  type F(!new)<T(!new)> = Coreader.Coreader<X,T>
+
+  function Map<S(!new),T(!new)>(f: S -> T): F<S> -> F<T> {
+    Coreader.MapRight(f)
+  }
+
+  ghost function Equal<T(!new)>(eq: (T, T) -> bool): (F<T>, F<T>) -> bool {
+    Coreader.Equal(eql, eq)
+  }  
+
+  /* Properties of Equal */
+  lemma LemmaEquivRelLift<T(!new)>(eq: (T, T) -> bool) {
+    LemmaEquiv();
+  }
+
+  /* Properties of Map */
+  lemma LemmaMapFunction<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, g: S -> T) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapFunctorial<S(!new),T(!new),U(!new)>(eq: (U, U) -> bool, f: S -> T, g: T -> U, w: F<S>) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapIdentity<T(!new)>(eq: (T, T) -> bool, id: T -> T) {
+    LemmaEquiv();
+  }
+
+  /* Comonad structure */
+  function Extract<T(!new)>(w: F<T>): T {
+    Coreader.ExtractRight(w)
+  } 
+
+  function Duplicate<T(!new)>(w: F<T>): F<F<T>> {
+    Coreader.DuplicateLeft(w)
+  }
+
+  /* Naturality */
+  lemma LemmaExtractNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, w: F<S>) {
+  }
+
+  lemma LemmaDuplicateNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, w: F<S>) {
+    LemmaEquiv();
+  }
+
+  /* Counitality and Coassociativity */
+  lemma LemmaCoUnitalityExtract<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaCoAssociativityDuplicate<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+    LemmaEquiv();
+  }
+}
+
+abstract module {:options "-functionSyntax:4"} CoreaderLeftComonad refines Comonad {
+  import Cowrappers.Coreader
+
+  type X(!new)
+
+  function eqr(x: X, y: X): bool
+
+  lemma LemmaEquiv()
+    ensures EquivalenceRelation(eqr)
+
+  /* Functor structure */
+  type F(!new)<T(!new)> = Coreader.Coreader<T,X>
+
+  function Map<S(!new),T(!new)>(f: S -> T): F<S> -> F<T> {
+    Coreader.MapLeft(f)
+  }
+
+  ghost function Equal<T(!new)>(eq: (T, T) -> bool): (F<T>, F<T>) -> bool {
+    Coreader.Equal(eq, eqr)
+  }  
+
+  /* Properties of Equal */
+  lemma LemmaEquivRelLift<T(!new)>(eq: (T, T) -> bool) {
+    LemmaEquiv();
+  }
+
+  /* Properties of Map */
+  lemma LemmaMapFunction<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, g: S -> T) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapFunctorial<S(!new),T(!new),U(!new)>(eq: (U, U) -> bool, f: S -> T, g: T -> U, w: F<S>) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapIdentity<T(!new)>(eq: (T, T) -> bool, id: T -> T) {
+    LemmaEquiv();
+  }
+
+  /* Comonad structure */
+  function Extract<T(!new)>(w: F<T>): T {
+    Coreader.ExtractLeft(w)
+  } 
+
+  function Duplicate<T(!new)>(w: F<T>): F<F<T>> {
+    Coreader.DuplicateRight(w)
+  }
+
+  /* Naturality */
+  lemma LemmaExtractNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, w: F<S>) {
+  }
+
+  lemma LemmaDuplicateNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, w: F<S>) {
+    LemmaEquiv();
+  }
+
+  /* Counitality and Coassociativity */
+  lemma LemmaCoUnitalityExtract<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaCoAssociativityDuplicate<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+    LemmaEquiv();
+  }
+}

src/Cowrappers.dfy

@@ -0,0 +1,61 @@
+// RUN: %dafny /compile:0 "%s"
+
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT 
+*******************************************************************************/
+
+module {:options "-functionSyntax:4"} Cowrappers {
+  module {:options "-functionSyntax:4"} Coreader {
+
+  datatype Coreader<+S,+T> = Coreader(left: S, right: T)
+
+  function ExtractRight<S,T>(r: Coreader<S,T>): T {
+    r.right
+  }
+
+  function ExtractLeft<S,T>(r: Coreader<S,T>): S {
+    r.left
+  }
+
+  function DuplicateLeft<S,T>(r: Coreader<S,T>): Coreader<S,Coreader<S,T>> {
+    Coreader(r.left, r)
+  }
+
+  function DuplicateRight<S,T>(r: Coreader<S,T>): Coreader<Coreader<S,T>,T> {
+    Coreader(r, r.right)
+  }
+
+  function ExtendRight<S,T1,T2>(f: Coreader<S,T1> -> T2, r: Coreader<S,T1>): Coreader<S,T2> {
+    Coreader(r.left, f(r))
+  }
+
+  function ExtendLeft<S1,S2,T>(f: Coreader<S1,T> -> S2, r: Coreader<S1,T>): Coreader<S2,T> {
+    Coreader(f(r), r.right)
+  }
+
+  function MapRight<S,T1,T2>(f: T1 -> T2): Coreader<S,T1> -> Coreader<S,T2> {
+    (r: Coreader<S,T1>) => 
+      Coreader(r.left, f(r.right))
+  }
+
+  function MapLeft<S1,S2,T>(f: S1 -> S2): Coreader<S1,T> -> Coreader<S2,T> {
+    (r: Coreader<S1,T>) => 
+      Coreader(f(r.left), r.right)
+  }
+
+  function KleisliCompositionRight<S,T1,T2,T3>(f: Coreader<S,T1> -> T2, g: Coreader<S,T2> -> T3): Coreader<S,T1> -> T3 {
+    r => g(ExtendRight(f, r))
+  }
+
+  function KleisliCompositionLeft<S1,S2,S3,T>(f: Coreader<S1,T> -> S2, g: Coreader<S2,T> -> S3): Coreader<S1,T> -> S3 {
+    r => g(ExtendLeft(f, r))
+  }
+
+  ghost function Equal<S,T>(eql: (S, S) -> bool, eqr: (T, T) -> bool): (Coreader<S,T>, Coreader<S,T>) -> bool {
+    (r1: Coreader<S,T>, r2: Coreader<S,T>) =>
+      eql(r1.left, r2.left) && eqr(r1.right, r2.right)
+  }
+
+  }
+}

src/FileIO/FileIO.dfy

@@ -18,9 +18,9 @@ include "../Wrappers.dfy"
  * File path symbols including . and .. are allowed.
  */
 module {:options "-functionSyntax:4"} FileIO {
-  import opened Wrappers
+  import opened Wrappers.Result
 
-  export provides ReadBytesFromFile, WriteBytesToFile, Wrappers
+  export provides ReadBytesFromFile, WriteBytesToFile, Result
 
   /*
    * Public API

src/Functions.dfy

@@ -21,4 +21,8 @@ module {:options "-functionSyntax:4"} Functions {
     forall x1, x2 :: f(x1) == f(x2) ==> x1 == x2
   }
 
+  function Composition<X,Y,Z>(f: X -> Y, g: Y -> Z): X -> Z {
+    x => g(f(x))
+  }
+
 }

src/Functor.dfy

@@ -0,0 +1,42 @@
+// RUN: %dafny /compile:0 "%s"
+
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT 
+*******************************************************************************/
+
+include "Functions.dfy"
+include "Relations.dfy"
+
+abstract module {:options "-functionSyntax:4"} Functor {
+  import opened Functions
+  import opened Relations
+
+  /* Structure */
+  type F(!new)<T(!new)>
+
+  function Map<S(!new),T(!new)>(f: S -> T): F<S> -> F<T>
+
+  ghost function Equal<T(!new)>(eq: (T, T) -> bool): (F<T>, F<T>) -> bool
+    requires EquivalenceRelation(eq)
+
+  /* Properties of Equal */
+  lemma LemmaEquivRelLift<T(!new)>(eq: (T, T) -> bool)
+    requires EquivalenceRelation(eq)
+    ensures EquivalenceRelation(Equal(eq))
+
+  /* Properties of Map */
+  lemma LemmaMapFunction<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, g: S -> T)
+    requires EquivalenceRelation(eq) 
+    requires forall x: S :: eq(f(x), g(x))
+    ensures forall w: F<S> :: Equal(eq)(Map(f)(w), Map(g)(w))
+
+  lemma LemmaMapFunctorial<S(!new),T(!new),U(!new)>(eq: (U, U) -> bool, f: S -> T, g: T -> U, w: F<S>)
+    requires EquivalenceRelation(eq)
+    ensures Equal(eq)(Map(Composition(f, g))(w), Composition(Map(f), Map(g))(w))
+
+  lemma LemmaMapIdentity<T(!new)>(eq: (T, T) -> bool, id: T -> T)
+    requires EquivalenceRelation(eq) 
+    requires forall x: T :: eq(id(x), x)
+    ensures forall w: F<T> :: Equal(eq)(Map(id)(w), w)
+}