dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.89k stars 258 forks source link

Feature request: support for traits as type arguments with variance on datatypes in Java #2013

Closed robin-aws closed 1 year ago

robin-aws commented 2 years ago

Follow-up from #1499, which looks like it was resolved by #1578 (which only added support in C#) accidentally.

robin-aws commented 2 years ago

This came up in the context of using a trait to represent errors when using a Result type, e.g.

trait Exception {}

function method Foo(): Result<int, Exception> {
  // ...
}

Note there is a workaround of defining a more specialized failure-compatible type instead of reusing Result:

datatype ResultWithException<T> = Success(value: T) | Failure(exception: Exception) {
  // ...
}
robin-aws commented 2 years ago

Actually, I should mention there's a simpler workaround.

Traits as type arguments on datatypes are only not supported for Java if the type parameter is declared with covariance or contravariance (e.g. -T or +T). I've adjusted the issue title to reflect this more accurately.

This means using a Result type that doesn't declare variance on its type parameters avoids this issue entirely. The only downside is that you can't assign a more specific instantiation of the type such as Result<MyConcreteClass, SpecificError> to the more generic Result<MyTrait, ErrorTrait> type. In my experience there is no need to ever use the more specific Result type.

Example to help clarify:


trait Vehicle {
}
class Car extends Vehicle {
  constructor() {}
}

trait Error {
}
class FlatTireError extends Error {
  constructor() {}
}

datatype NonVariantResult<T, E> = NVSuccess(value: T) | NVFailure(error: E)
datatype CovariantResult<+T, +E> = CVSuccess(value: T) | CVFailure(error: E)

method Main() {
  var myCar: Car := new Car();
  var error: Error := new FlatTireError();

  var cvSuccess: CovariantResult<Vehicle, Error> := CVSuccess(myCar);
  var cvFailure: CovariantResult<Vehicle, Error> := CVFailure(error);

  // This is just fine
  var nvSuccess: NonVariantResult<Vehicle, Error> := NVSuccess(myCar);
  var nvFailure: NonVariantResult<Vehicle, Error> := NVFailure(error);

  // This is the only pattern that doesn't work without variance
  var nvCarSuccess: NonVariantResult<Car, Error> := NVSuccess(myCar);
  var nvVehicleSuccess: NonVariantResult<Vehicle, Error> := nvCarSuccess; // RHS (...) not assignable to LHS (...)
  var cvCarSuccess: CovariantResult<Car, Error> := CVSuccess(myCar);
  var cvVehicleSuccess: CovariantResult<Vehicle, Error> := cvCarSuccess; // Type checks
}