Result monad

[stefan-aws]

I propose we remove https://github.com/dafny-lang/libraries/blob/master/src/Wrappers.dfy and create a separate file for each of the existing wrappers, and for any wrapper we add in the future. (Perhaps it would be good to group them in one folder.) In particular, I suggest that we extend the existing code for the result monad such that it contains at least the code below. Please ignore the include of Wrappers.dfy for now. I am particularly impressed that Dafny proves all monad laws by itself.

include "Wrappers.dfy"

module {:options "-functionSyntax:4"} Result {

  import opened Wrappers 

  datatype Result<+S,+E> = | Success(value: S) | Failure(error: E)

  function Success<S,E>(v: S): Result<S,E> {
    Result.Success(v)
  }

  function Failure<S,E>(e: E): Result<S,E> {
    Result.Failure(e)
  }

  predicate IsSuccess<S,E>(r: Result<S,E>) {
    r.Success?
  }  

  predicate IsFailure<S,E>(r: Result<S,E>) {
    r.Failure?
  }  

  function GetValue<S,E>(r: Result<S,E>): S 
    requires r.Success?
  {
    r.value
  }

  function GetValueDefault<S,E>(r: Result<S,E>, default: S): S {
    match r 
    case Success(v) => v
    case Failure(_) => default
  }

  function GetError<S,E>(r: Result<S,E>): E 
    requires r.Failure?
  {
    r.error
  }

  function Bind<S1,S2,E>(r: Result<S1,E>, f: S1 -> Result<S2,E>): Result<S2,E> {
    match r
    case Success(v) => f(v)
    case Failure(e) => Result<S2,E>.Failure(e)
  }

  function Join<S,E>(rr: Result<Result<S,E>,E>): Result<S,E> {
    match rr
    case Success(v) => v
    case Failure(e) => Result<S,E>.Failure(e)
  }

  function Map<S1,S2,E>(f: S1 -> S2): Result<S1,E> -> Result<S2,E> {
    (r: Result<S1,E>) =>
      match r 
      case Success(v) => Result<S2,E>.Success(f(v))
      case Failure(e) => Result<S2,E>.Failure(e)
  }

  function MapError<S,E1,E2>(f: E1 -> E2): Result<S,E1> -> Result<S,E2> {
    (r: Result<S,E1>) =>
      match r 
      case Success(v) => Result<S,E2>.Success(v)
      case Failure(e) => Result<S,E2>.Failure(f(e))
  }  

  function Fold<S,E,T>(f: S -> T, g: E -> T): Result<S,E> -> T {
    (r: Result<S,E>) =>
      match r 
      case Success(v) => f(v)
      case Failure(e) => g(e)
  }

  function Composition<S1,S2,S3,E>(f: S1 -> Result<S2,E>, g: S2 -> Result<S3,E>): S1 -> Result<S3,E> {
    x => Bind(f(x), g)
  }

  function ToSeq<S,E>(r: Result<S,E>): seq<S> {
    match r
    case Success(v) => [v]
    case Failure(_) => []
  }

  function ToSet<S,E>(r: Result<S,E>): set<S> {
    match r
    case Success(v) => {v}
    case Failure(_) => {}   
  }

  function ToOption<S,E>(r: Result<S,E>): Option<S> {
    match r
    case Success(v) => Some(v)
    case Failure(_) => None()
  }

  lemma LemmaUnitalityJoin<S,E>(r: Result<S,E>)
    ensures Join(Map(Success<S,E>)(r)) == r == Join(Success<Result<S,E>,E>(r))
  {
  }

  lemma LemmaAssociativityJoin<S,E>(rrr: Result<Result<Result<S,E>,E>,E>) 
    ensures Join(Map(Join<S,E>)(rrr)) == Join(Join<Result<S,E>,E>(rrr))
  {
  }  

  lemma LemmaLeftUnitalityBind<S1,S2,E>(v: S1, f: S1 -> Result<S2,E>)
    ensures Bind(Success(v), f) == f(v)
  {
  }

  lemma LemmaRightUnitalityBind<S,E>(r: Result<S,E>)
    ensures Bind(r, Success) == r
  {
  }

  lemma LemmaAssociativityBind<S1,S2,S3,E>(r: Result<S1,E>, f: S1 -> Result<S2,E>, g: S2 -> Result<S3,E>)
    ensures Bind(Bind(r, f), g) == Bind(r, Composition(f, g))
  {
  }

}

[davidcok]

1. Why do you propose separate files? In my review of the library, I'm considering proposing fewer files, so there need to be fewer includes.

2. Why are you proposing functions that simply replace constructors or discriminators?

3. I note that some of the new functions have type parameters that are not used. I'm not sure those will work.