Dafny 4 Suggestion: Adaptors to fix usability of update with failure

[davidcok]

The update-with-failure statement (and related expression) has a significant usability problem, which is that all the uses of such features within a program must use the same generic failure-compatible (FC) type. This is a usability problem for any major project that incorporates source code and libraries from multiple sources.

I can imagine a variety of kinds of FC types that are plausibly used: the Result and Outcome types that are in the library code and variations of those that held more failure data, such as location of error and more specific information about the error than just a message.

The root of the problem is that the PropagateFailure method in a FC type is what converts a failure value in the callee to a failure value in the caller, but the PropagateFailure method is a member of the callee . That is, the callee has to know the the FC types used by all its callers and a caller can only use callees with compatible FC types.

A better approach would be to have the caller have multiple methods that constructed a caller FC value from values of a variety of input FCTs. Dafny would pick a method of the caller FCT that had the right calleeFCT->callerFCT signature and use it to convert the failure value as needed. No PropagateFailure method is needed on the callee side. An identity function could be implicitly an option.

This would look like

datatype Outcome<E> = Pass | Fail(error: E)
  {
    predicate method IsFailure() {
      Fail?
    }
    static function method FromOutcome(f: Outcome<E>): Outcome<E>
      requires f.Fail?
    {
      f
    }
    static function method FromResult<T>(f: Result<T,E>): Outcome<E>
      requires f.Failure?
    {
      Outcome<E>.Fail(f.error)
    }
  }
datatype Result<T,E> = Success(value: T) | Failure(error: E)
  {
    predicate method IsFailure() {
      Failure?
    }
    static function method FromOutcome(f: Outcome<E>): Result<T,E>
      requires f.Fail?
    {
      Result<T,E>.Failure(f.error)
    }
    static function method FromResult<X>(f: Result<X,E>): Result<T,E>
      requires f.Failure?
    {
      Result<T,E>.Failure(f.error)
    }
  }

Even here though the caller has to know how to extract failure information from a callee. And if the FC type of the caller is a library type, only a fixed set of conversions can be built in, even after adjusting the Dafny language to look for more than one conversion. But this would allow a library to accommodate a few known styles of use -- for example both the value-carrying Result and the non-value-carrying Outcome currently in the library.

A more general approach would be to permit a non-ghost conversion function to be indicated at the call site for any conversion that is not handled by the above. That would look something like this:

datatype CalleeFCT = Pass | Fail(error: string, line int)
  {
    predicate method IsFailure() {
      Fail?
    }
    function method PropagateFailure(): CalleeFCT
      requires Fail?
    {
      Fail(this.error, this.line)
    }
  }

datatype CallerFCT = Success | Failure(error: string)
  {
    predicate method IsFailure() {
      Failure?
    }
    function method PropagateFailure(): CallerFCT
      requires Failure?
    {
      Failure(this.error)
    }
  }


method m() returns status: CalleeFCT, value: int {
  return CalleeFCT.Fail("Error!", 9), 42;
}
method mm() returns CallerFCT {
  var k :- {: convertFailure f => CallerFCT.Failure(f.error) } m();
}

The type of the value of the :convertFailure attribute is (C) ~> (C'), where C is the callee FCT at a the call-site and C' is the caller FCT of the enclosing method. The function is only called when IsFailure? is true.

The desugaring of

k :- {: convertFailure F } m();

is

status, k := m();
if (status.IsFailure()) { return F(status), k; }

So I have these recommendations:

• Good Dafny style has FCTs with a FCT that has some field named 'error' that holds a string error message
• The Outcome type in the current libraries return a Outcome from PropagateFailure, so that a program can consistently use Outcome as a non-value-carrying FC type.
• An FC type appropriate for :- is one with an IsFailure? non-ghost function
• When :- is used, the callee's FC value is converted to a caller FC value by
• • the function given in the attribute, if there is one (per the attribute given above, with attribute name TBD)
• • otherwise a function in the caller with a matching signature
• • otherwise use the callee's PropagateFailure function if the signature is appropriate
• • otherwise the identity function if the callee and caller FC types are the same
• • otherwise it is a type error

This is not necessarily a breaking change -- if there are no attributes and no matching caller-side functions, then PropagateFailure would be used. If there already is by coincidence a matching caller-side function, then if it took precedence over PropagateFailure, there would be a change in behavior.

[MikaelMayer]

{:convertFailure f => CallerFCT.Failure(f.error) } m();

I like both of your ideas.

[keyboardDrummer]

The update-with-failure statement (and related expression) has a significant usability problem, which is that all the uses of such features within a program must use the same generic failure-compatible (FC) type.

Don't you mean that all uses of such features within a method or function must use the same generic failure-compatible (FC) type?

Could you add to the description of this issue, a Dafny example where you want to use two FC types in one callable (a method or function), and ideally also how you would currently work around it by splitting the callable up into two, to make it more obvious what the current pain point is?

[davidcok]

Don't you mean that all uses of such features within a method or function must use the same generic failure-compatible (FC) type?

Yes - but then that applies to any chain of calls that pass the FC value up the chain.

[keyboardDrummer]

Don't you mean that all uses of such features within a method or function must use the same generic failure-compatible (FC) type?

Yes - but then that applies to any chain of calls that pass the FC value up the chain.

But when you call a method that returns a FC type, you can convert that value to another FC type, so at any point in the chain you're free to use the FC type you prefer, no?

As mentioned, I think it would be good to have a use-case in the issue description, so it's more obvious what the downsides of the current approach are.

[cpitclaudel]

But when you call a method that returns a FC type, you can convert that value to another FC type, so at any point in the chain you're free to use the FC type you prefer, no?

I think the issue is real but narrow. I thought the same as you @keyboardDrummer , but there's one case where you can't conveniently do this, and it's when you have a method that returns two parameters, one of which is an outcome and the other of which is a regular value. I didn't know that it was possible to call such a method with :- (it looks very similar to Go's error handling style)

Normally when I want to cast a method result I do something like this:

      function method MapFailure<R'>(f: R --> R') : Result<T, R'>
        requires this.Failure? ==> f.requires(this.error)
      {
        match this
          case Success(value) => Success(value)
          case Failure(error) => Failure(f(error))
      }

The problem is that in @davidcok's example you can't do this.

@davidcok in your original message you mention that this is an issue with the update-with-failure statement and the related expression; can you give an example of that issue for expressions? I see the problem with statement, but unless I'm missing something it seems to be specific to methods that return multiple values, and hence shouldn't be an issue with functions, correct?

[keyboardDrummer]

Thanks for the explanation, but even in the multiple return value case, you're still free to use := instead of :- right?

method m() returns status: CalleeFCT, value: int {
  return CalleeFCT.Fail("Error!", 9), 42;
}
method mm() returns CallerFCT {
  var status, k := m();
  if status.IsFailure() then {
    return CallerFCT.Failure(status.error)
  } else {
    return CallerFCT.Success
  }
}

Also, what's the reason to support :- on a RHS with multiple values? Would better support for tuples make that feature obsolete?

[davidcok]

Sorry for the delay in getting back to this. The problem is not only with multiple return values. It is simply this: in the current structure, in using the :- syntax, the caller has to use a FCT determined by the callee's FCT, namely the type returned by PropagateFailure (though the type of the Success value can be generic, but not the type of the Failure value). To give a more concrete example, suppose you have a project that wants to propagate error location information along with an error message. So the project wants to use this FCT

datatype ResultWithErrorInfo<T> = Success(value: T) | Failure(error: string, file: string, line: int)
  {
    predicate method IsFailure() {
      Failure?
    }
    static function method PropagateFailure(): ResultWithErrorInfo <U>
      requires f.Failure?
    {
      Result<U>.Failure(f.error, f.file, f.line)
    }
  }

But then you want to call a library method someone else has written, which uses, say, the Result<int,string> from the library. Using :- won't type check because PropagateFailure does not produce a ResultWithErrorInfo. Instead you have to use := :

method f() returns (result: ResultWithErrorInfo<int>)
//var r :- libraryMethod(...); // illegal -- returns a Result<int>

var r := libraryMethod(...);
if (r.Failure?) { return ResultWithErrorInfo.Failure(r.error, "?", -1); }

That is, you have to do a manual conversion from one failure alternative to another. That is no better than having to remember to check status values after every C function one calls.

There seem to me these options:
a) Require everyone to use one FCT, generic on the type of Success value it carries (if it carries one).
b) Just fall back to the manual approach above whenever the types are different. But then why have :- in the first place?
c) Put the burden of conversion on the caller rather than the callee, allowing multiple source types. I outlined a design of this sort in a previous comment. The burden of conversion belongs with the caller, in my opinion. But even so, the caller FCT can only build in possible callee FCT's that it knows about. But this could be part of an overall solution.
d) Provide language support for specifying a conversion at the call-site, while still using :-. This was my attribute-based proposal. For the above example the code would look like

var r := {:convertFailure f=> ResultWithErrorInfo<int>.Failure(f.error, "?",-1) } libraryMethod(...);

I'm not wedded to using an attribute, and certainly not to the name, but do think that Dafny would be better for large projects if the language supported some sort of FCT conversion, specifiable at the call-site and independent of either the caller or callee FCT.

@keyboardDummer said: But when you call a method that returns a FC type, you can convert that value to another FC type, so at any point in the chain you're free to use the FC type you prefer, no?

Yes you can always make the call using :=and do a manual conversion. The design question is then whether the frequency of FCT mismatch is high enough to warrant some language feature to accommodate. As I see it, Dafny has so far been used for small tutorial and academic/educational issues and some largish projects that control all their own code. So the problem I describe has not arisen. But I anticipate it will arise as soon as large projects start that try to incorporate library code from multiple sources.

@cpitclaudel : Yes I did gloss over let-or-fail expressions. In the case of V; E where V might return a failure, that failure value and the value of E have to be the same type, something like either Result or ResultWithErrorInfo, which type is clearly determined by the callee; as there is no immediate return from the method it does not have to match the caller's FCT. So the problem I describe only arises if that expression is assigned somewhere with a :-. So you are correct: there is not an issue with expressions, just with :- when that expression is assigned to something.

@cpitclaudel : The problem is not just with multiple out parameters, as I described above. The problem is when the construction of a Failure value in the caller differs from the construction used in the callee's PropagateFailure method.

@keyboardDrummer said: Also, what's the reason to support :- on a RHS with multiple values? Would better support for tuples make that feature obsolete?

If Dafny is going to support := with multiple outputs, then it should support :- with multiple outputs. But I agree that tuples could be used in either case -- and that is how multiple outputs are compiled to languages that don't support multiple outputs.

---

I actually prefer to keep the error status separate from the return value, and so I much prefer the library's Outcome to Result (though I prefer the name Status to Outcome). That is I prefer writing

method div(x: int, y: int) returns (r: Status, q: int) {
  if ( y == 0) return Fail("zero divisor"), 0;
  return Pass, x/y;
}

And it works consistently with multiple outputs. But that is a style and preference question that is not the point here.

[cpitclaudel]

Just focusing on the issue with expressions:

@cpitclaudel : Yes I did gloss over let-or-fail expressions. In the case of V; E where V might return a failure, that failure value and the value of E have to be the same type, something like either Result or ResultWithErrorInfo, which type is clearly determined by the callee;

See above with MapFailure: you can chain calls on the expression that returns an error, and this is in fact what I do in my code. I use :- extensively, with different error types, and it works just fine for that, AFAICT:

var x :- SomeComputation(…).MapFailure(f => SomeOtherFailure(f));

So the problem I describe only arises if that expression is assigned somewhere with a :-. So you are correct: there is not an issue with expressions, just with :- when that expression is assigned to something.

Not quite, again, because you can chain the cast. You suggest doing it with an attribute, but for expressions it can be done with a member function instead.

I actually prefer to keep the error status separate from the return value, and so I much prefer the library's Outcome to Result (though I prefer the name Status to Outcome). That is I prefer writing

The example you gave with div is pure and deterministic; given that, I don't think you really have a problem for this specific example: you can make it a function method and use the MapFailure pattern above.

And it works consistently with multiple outputs. But that is a style and preference question that is not the point here.

I think it is? I agree that :- doesn't work for the style you describe (methods with multiple returns), but it works just fine with functions returning results.

One last note:

var r := libraryMethod(...);
if (r.Failure?) { return ResultWithErrorInfo.Failure(r.error, "?", -1); }

I write this like the following:

var r := libraryMethod(...);
var r :- r.MapFailure(…);
…

For me what this suggests is that we really want to be able to chain functions after methods; then you could write this:

var r :- libraryMethod(...).MapFailure(…);

But: I agree that this doesn't solve the multi-return case any way.

Finally @keyboardDrummer:

Also, what's the reason to support :- on a RHS with multiple values? Would better support for tuples make that feature obsolete?

Potentially performance? Dafny code using tuples is pretty slow in C# at least.

[davidcok]

My overall point was that there needs to be a way to convert one failure type to another at the call-site. I'm not wedded to any particular solution. Your use of MapFailure does precisely that, though as you point out it does not work with multiple returns. Your example does take a function as an argument, so it is not restricted to known FCTs. I see these issues:

• the multiple return problem
• requires chaining a function call on a method call
• requires that FCTs define a MapFailure method (that takes a function), which we could recommend.

Actually, if PropagateFailure took a function argument and there was a syntactic way to say to use a particular function, that would be an implicitly applied MapFailure, which would meet my overall goals in the context of the current language.

[davidcok]

The revision of the Dafny library adds functions to convert among FC-types. This may be sufficient for most use cases. The one that is not covered is a method returning an FC-type where the calling method has a different FC-type. For this, currently, one needs to capture the callee's FC-value (with :=) and then do a conversion manually.

We might want to put in some syntax that makes this more concise, but we can wait to see if there is any user use case driving such syntax. It will only arise if users are using source code from multiple sources that use differnt FC-types that then need to be converted among.