Feature request: member methods on type aliases

[cpitclaudel]

One obstacle to reusing existing library types in client code is that Dafny currently does not support defining member functions on type aliases. Here is what I would like to be able to write:

// Library
datatype Result<+T, +Q> = Success(t: T) | Failure(q: Q)

// App
datatype AppExn = ErrorA | ErrorB(s: string)

type AppResult<+T> = Result<T, AppExn> {
  predicate method isErrorA<T>() { // HERE: A member method
    this == Failure(ErrorA)
  }
}

// Client
function method APICall() : AppResult<int>
method t() {
  var i := APICall();
  if i.isErrorA() { print "A!\n"; } // HERE: Member syntax for i.isErrorA()
  else if i.Failure? { print "!!\n"; }
  else { print i.t, "\n"; }
}

Here is the working Dafny code that I have to write instead:

// Library
datatype Result<+T, +Q> = Success(t: T) | Failure(q: Q)

// App
datatype AppExn = ErrorA | ErrorB(s: string)
type AppResult<+T> = Result<T, AppExn>

predicate method isErrorA<T>(this_: AppResult<T>) { // HERE: Not a member function
  this_ == Failure(ErrorA)
}

// Client
function method APICall() : AppResult<int>
method t() {
  var i := APICall();
  if isErrorA(i) { print "A!\n"; } // HERE: Regular function code
  else if i.Failure? { print "!!\n"; }
  else { print i.t, "\n"; }
}

The status quo makes it harder to reuse existing types from Dafny's standard library, because newly defined methods look "second-class" (they don't get member syntax)

Could we allow member methods on type aliases?

[robin-aws]

This has been on my mind as I worked on prototype standard library code for enumeration too (https://github.com/dafny-lang/libraries/pull/37). It's a really common pattern in multiple languages to support chaining operations on values (e.g. something like myList.stream().filter(x => x < 5).map(x => x + 2).collect(toList()) in Java), and this feature would be one possible way to support that style without needing to define all possible transformations directly on the type in question.

[cpitclaudel]

I think you'd need a bit more than this feature for this, because this issue assumes that there's a new type alias that you're add methods to. In contrast, I think you want to add member methods to existing types, which C# calls "extension methods"?

I agree that general-purpose extension methods would take care of the problem above nicely. For your issue of streaming APIs, though, do you want extension methods or do you want a trait? Presumably you want to attach a consistent spec to all .map implementations?