Does Dafny have monadic error handling?

Question

Does Dafny have monadic error handling?

Answer

Yes.

In particular, see the section of the reference manual on Update with Failure statements. The (draft) standard library includes some types needed for error handling.

You can define your own monadic error type by following examples in the RM and the draft library. A simple case is

datatype Outcome<T> =
            | Success(value: T)
            | Failure(error: string)
{
  predicate IsFailure() {
    this.Failure?
  }
  function PropagateFailure<U>(): Outcome<U>
    requires IsFailure()
  {
    Failure(this.error) // this is Outcome<U>.Failure(...)
  }
  function Extract(): T
    requires !IsFailure()
  {
    this.value
  }
}