Why is there a generic parameter in Constructor<R> class in Z3 Java API?

[ruijiefang]

Hello,

I'm recently looking at Z3's Java API, and found the definition of a datatype constructor class a bit confusing --- at https://github.com/Z3Prover/z3/blob/master/src/api/java/Constructor.java#L25, there is a generic parameter R, but this parameter seems unused throughout the Constructor class, and there is no obvious lower bound / upper bound on this generic parameter. Is this truly unused, or is this supposed to mean something?

[NikolajBjorner]

@ThomasHaas

[ThomasHaas]

Those changes were made by @addisoncrump in 3bca1fb. I guess he was a little too eager when adding generic types to the API :).

I agree that the type parameter there does not seem to do anything.

[ruijiefang]

Just curious, what is to be gained in general by adding generics? Java's runtime type erasure has made Expr<T> more difficult to use compared to just an Expr, and even if the runtime type info is somehow managed behind the scenes, the API caller still needs to do book-keeping somehow or resort to using asInstanceOf more frequently. And is it just me, or do other people find the use of <?> in the method signatures a little bit aesthetically troubling? :-).

[addisoncrump]

Not going to lie, I wrote this code many years ago and will need to look back over it. I think it was for local type checking, but you are correct: this only really helps when you are checking the types because of erasure.