Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
robin-aws opened this issue Apr 13, 2022 · 2 comments · Fixed by #3072
Closed
Assignees
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: java Dafny's Java transpiler and its runtime

Comments

@robin-aws
Copy link
Member

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

@fabiomadge fabiomadge added lang: java Dafny's Java transpiler and its runtime kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny labels Apr 13, 2022
@robin-aws
Copy link
Member Author

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 robin-aws changed the title Feature request: support for traits as type parameters on datatypes in Java Feature request: support for traits as type arguments with variance on datatypes in Java Jul 12, 2022
@robin-aws
Copy link
Member Author

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
}

@RustanLeino RustanLeino self-assigned this Nov 18, 2022
RustanLeino added a commit to RustanLeino/dafny that referenced this issue Nov 18, 2022
RustanLeino added a commit that referenced this issue Nov 29, 2022
… in Java (#3072)

This PR removes that pesky "not supported" error for Java where it
wouldn't allow a `trait` to be passed in as a variant type parameter of
a (co)datatype.

Fixes #2013

The solution is pretty simple. Basically, it just emits casts when
needed. To be accepted by Java's static type checker, these casts first
upcast to `Object` and then downcast to the desired type. Since the JVM
doesn't keep track of type parameters, it'll never know what hit it. (In
particular, this means that we don't need the expensive `DowncastClone`
mechanism that we're using for C# to satisfy .NET's more informed
runtime.)

To make it work, this PR also makes more precise the `IsTargetSupertype`
method for Java. In particular, to check if `A<X, Y>` is a supertype of
`B<U, V, W>`, first keep converting the latter up the `trait` parents of
`B` until it gets to `A` (if ever). This is already done for all the
compilers. Call the result `A<X', Y'>`. For the other compilers, one
would now start to see if the parameters `X, Y` are target supertypes of
`X', Y'` with variance in mind (for example, if the first type parameter
is contravariant, we would actually check if `X'` is a supertype of
`X`). For Java, however, we continue with variance in mind only if `A`
is a collection type (because those already have run-time support for
variance, using Java's bounded existential types). For non-collection
types, we instead check if `X, Y` are target-type equal to `X', Y'`. If
they are not, the compiler calls `EmitDowncast`. (To read these in the
code, look at `EmitDowncastIfNecessary` in `SinglePassCompiler.cs`.)

We could have used simple casts like this for collection types, too. But
since I already have those, I left those alone.


<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Co-authored-by: Fabio Madge <fabio@madge.me>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: java Dafny's Java transpiler and its runtime
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants