:- with more than one out-parameter

[RustanLeino]

@samuelgruetter

Problem

If M is a method like

method M(a: A) returns (res: Result<B>)

and Result is a type like:

datatype Result<T> = Success(T) | Failure(string)
{
  // members IsFailure, PropagateFailure, Extract
}

then Dafny allows the method to be called like:

b :- M(a);

There are examples where it would be useful to be able to return additional values. In particular, we have examples where it would be convenient to return ghost values together with the success value. It's awkward to do that today. For example, use of :- requires the method to have exactly one out-parameter, the tuple type is built in and does not have any form like

(B, ghost C)

Therefore, one must declare a new type of pairs, like

datatype ExtendWithGhost<X, Y> = ExtendWithGhost(x: X, ghost y: Y)

and use that in the signature of M:

method M(a: A) returns (res: Result<ExtendWithGhost<B, C>>)

Not only is this construction a bit clumsy, but it also leaves an ExtendWithGhost wrapper around the B value at run time.

Proposed solution

I propose that Dafny allow :- to be used to call methods with more than one out-parameter, provided that the first out-parameter follows the rules of the current :- method calls. (That is, the first out-parameter must be such a Result type.)

Here's what the example above would look like:

method M(a: A) returns (res: Result<B>, ghost c: C)

A call would look like

b, c :- M(a);

which would mean

var tmp;
tmp, c := M(a);
if tmp.IsFailure() {
  callerRes := tmp.PropagateFailure();
  return;
}
b := tmp.Extract();

where callerRes is the name of the first out-parameter of the caller.

Note that the additional out-parameters (here, c) are passed regardless of the success/failure status of the first out-parameter.

Note that the way I defined the meaning above allows the caller itself to have any number of out-parameters, as long as the first one (which I assumed is called callerRes) has a type returned by tmp.PropagateFailure(). In particular, this means that c in the caller can be any l-value (for example, a local variable or any out-parameter of the caller).

In my example, I added one ghost parameter, which is a ghost, because this is scenario we have seen. Dafny could allow any number of additional out-parameters, both ghost and non-ghost.

Alternative solution to the motivating example

Dafny could provide built-in support for tuples with ghost components. Such a type might be written as

TupleType ::= "(" [ TupleComponent ( "," TupleComponent )+ ] ")"
TupleComponent ::= [ "ghost" ] TypeName

Note that TupleType has 0 or 2-or-more components, just like tuples do today.

This new tuple type would compile to a tuple with all ghost components deleted. In the special case that there is only one non-ghost component, the type would compile to that component alone, without any 1-tuple wrapper.

[samuelgruetter]

Interesting! It seems to me that both Result<(B, Ghost)> and (Result<B>, Ghost) have valid use cases, so I'd like to see a solution which works for both, but each of the above solutions only works for one of them.

Regarding the undesired runtime wrapper, have you seen Scala's value classes? They might be nice to have in Dafny too.

[robin-aws]

Just to clarify, I gather the alternative solution would look like this?

method M(a: A) returns (res: Result<(B, ghost C)>)

And the call like this?

var (b, c) :- M(a);

I definitely prefer this over the "the first return value is special" solution - that definitely feels less elegant and general, although I admit I can't put my finger on a concrete example of why it wouldn't be a good idea. I'm still holding out hope that :- can be retroactively interpreted as a special case of Monads in the future, and this would be moving further away from that possibility.

Allowing ghost tuple elements seems to follow naturally from allowing it on datatypes and classes/traits, and optimizing away the wrapper seems like a perfectly reasonable compiler responsibility that would apply there too.

[RustanLeino]

@davidcok and I discussed this one today. I still like the "first return value is special" solution.

David suggested additionally supporting the version where there is no Extract() member. It would work as shown above, but without the b parameter and without the call to Extract(). With this version, program can choose to use a style where the "special first parameter" signals either Okay or an Error(string), for example, and all remaining parameters pass any success (and failure) values.

Whenever there are additional non-ghost parameters, the proposal to compile :- using exceptions in a target language (see dafny-lang/rfcs#1) would still need a try-catch at every level to make sure out-parameters get passed properly.

I propose:

• We implement the "first return value is special" solution above
• We implement (possibly as a separate PR), the extension of that solution to the no-Extract() case
• We ignore the "alternative solution" for now, but we may consider making this into a separate feature request. (It can be used with :-, but is really a feature in its own right.)

To respond to @samuelgruetter : Yes, both can be useful. If we implement "first return value is special" now, we get one of them. And if we add ghosty tuples (i.e., tuples with ghost components) in the future, we'll support the other kind, too.

To respond to @robin-aws : I was going to say "yes" to your syntax question, and I was going to add "just like for non-ghosty tuples today". But then I tried it out and was reminded that such destruction is supported today only if M is a function. Today, if you want to destruct an out-parameter from a method, you first have to read it into another variable and then, separately, do the destruction. So, unless we also a feature to destruct method out-parameters at call sites, you'd have to write:

var r := M(a);
var (b, c) := r;

[davidcok]

Fixed along with #446 in PR #809.