Type-safe assignments and valuations

[mtf90]

During my work on cleaning up type definitions (cf. #75) I found that many assignments lack proper type checking. In fact, you can easily assign a String value to an Integer register or parameter. While one could add additional type-equality checks, these would only detect errors at runtime. I was wondering whether it is desirable to have compile-time type checking as well? Essentially, this would make SymbolicDataValues (incl. sub-classes) parameterized in their DataType<T>.

This would not get rid of runtime checks completely because you can always create types such as DataType<Integer>("id", Integer.class) and DataType<Integer>("pin", Integer.class) which are type-compatible but unequal. However, it would at least allow for more type specificity, because users could decide to create explicit Id and Pin classes for this purpose.

Furthermore, the current assignment structure would have to change. You cannot enforce (nested) type constraints on keys and values if, e.g., a VarMapping is a Map<SymbolicDataValue<?>, SymbolicDataValue<?>> (otherwise you would not allow assignments of different-typed registers). So rather than a Map<X, Y> the assignments would need to be encoded as a Collection<Assignment<?>> where Assignment<T> enforces the same type T on the target and the source (there would be specific sub-classes for registers, parameters, valuations, etc.).

Currently, this isn't that much of a problem, because in most cases guards, etc. only check for equality which works on arbitrary Objects. However, already the AtomicGuardExpression could be cleaned up if the SMALLER/BIGGER guards could enforce a <T extends Comparable<T>> bound. Especially looking forward to more complex guards (cf. #73 (comment)), proper typing support could be very beneficial.

I'm in favor of this refactoring because I like to utilize the strong typing capabilities of the language. The compiler is a friend that helps you to prevent errors. However, since this would induce quite a lot of refactoring, I'd like to hear other opinions first. Especially if you have other solutions to this problem, feel free to present/discuss them here.

[fhowar]

This is ok for me. Can you prepare a pull request with a proposal?

[mtf90]

It is a little bit complicated to isolate this feature in a single pull request because it is part of the more complex, ongoing RAlib re-integration. However, I want to give a short update of the current state as I have been working again on this issue for the last couple of days.

Initially, I advocated for a Collection<Assignment<?>>-based approach to strongly bind the common type parameter of SymbolicDataValues and actual DataValues (or even other SymbolicDataValues in case of Mappings). However, during execution (i.e., updating a Register mapping) and especially for the evaluation of GuardExpressions you often need a direct, key-based lookup mechanism. Iterating through collections of assignments seems very inconvenient and non-performant for this. Therefore, I looked into solutions that could keep the current Map-based semantics but there are some challenges.

The rigorous approach

In order to enforce the same type for the arguments of the assignment/valuation, you need method-level type variables. For example, a RegisterValuation could look like this:

public <T> void put(Register<T> reg, DataValue<T> val) {
    // ...
}

public <T> DataValue<T> get(Register<T> reg) {
    // ...
}

Here, the main problem is that these methods cannot override the respective put/get methods of the Map interface. For the put method, Java would even require higher-kinded generics (as in public <T> void put(K<T> reg, V<T> val)). Implementing all the refinements via independent classes adds some boilerplate code with which I would even be fine if it would mean that user-land could benefit from this type-safety.

However, the second drawback is that it would require a lot of refactoring of existing code because you would now need to maintain proper type information. Currently, this is already a challenge in the XML serializer which constructs Registers/Constants/etc. first and then sets their values. I'm unsure whether all the learning-related code (e.g., SDTs) or working with these concepts in general would become more inconvenient due to this.

And after all, this approach would still require runtime checks because you wouldn't be able to distinguish between an integer-based id type and integer-based pin type at compile level anyway.

The laissez-faire approach

Someone who doubles down on the last point could also argue that since (thorough) type checking only happens at runtime anyway, we may ditch the type information completely and only deal with it when necessary (e.g., via explicit casting). While I can understand this point of view, I would argue that type information generally help to write cleaner and less error-prone code and can even be more convenient if used in the right places. So I would definitely try to provide type information where reasonable.

The compromise approach

A potential compromise would be to introduce type information only for data retrieval, i.e.,

public <T> DataValue<T> get(Register<T> reg) {
    // ...
}

This method would not override the Map#get method

public V get(Object reg) {
    // ...
}

(with V extends DataValue<?>) but exist alongside of it. Since we typically have type-specific keys at the call-site, one would automatically link against the type-specific variant, greatly profiting from the type information. See, e.g., a potential ComparableGuard:

public class ComparableGuard<T extends Comparable<T>, L extends SymbolicDataValue<T>, R extends SymbolicDataValue<T>> implements GuardExpression {

    private final L left;
    private final R right;

    public ComparableGuard(L left, R right) {
        this.left = left;
        this.right = right;
    }

    @Override
    public boolean isSatisfied(Valuation<?, ?> val) {
        DataValue<T> lv = val.get(left);
        DataValue<T> rv = val.get(right);

        return lv.getValue().compareTo(rv.getValue()) < 0;
    }

    // ...
}

At the same time, type management can be ignored when constructing mappings or valuations which should minimize the impact on existing code. For some user-facing parts it may also be possible to provide convenient (and type-safe) utility functions, e.g., a constructor

public <T1, T2> Assignment(Register<T1> reg1, SymbolicDataValue<T1> val1, Register<T2> reg2, SymbolicDataValue<T2> val2) {
  // ...
}

for constructing assignments directly, etc.

Overall, I think I'm happiest with the last approach. However, I have to think about and experiment with it a little bit more. I'm happy to hear other opinions (and solutions) as well since there are things that I might not see.

[mtf90]

Just a small update: The compromise approach works relatively well with valuations since the return type is always DataValue<T>. However, problems occur when using mappings. Since a VarMapping<K, V> should get a V, writing something like

public <T> SymbolicDataValue<T> get(SymbolicDataValue<T> key) {
    return (SymbolicDataValue<T>) super.get(key);
}

loses this information, i.e., a VarMapping<Register<?>, Register<?>> would only return a SymbolicDataValue<T> instead of a Register<T>. This can be compensated for relatively easy by introducing a type-specific refinement such as

public class RegMapping<K extends SymbolicDataValue<?>> extends VarMapping<K, Register<?>> {
    @Override
    public <T> Register<T> get(SymbolicDataValue<T> key) {
        return (Register<T>) super.get(key);
    }
}

which can be used instead of a normal VarMapping. In my opinion, the additional overhead of providing these type-specific refinements (for Parameter<T>s, etc. as well) is manageable.

Switching to these type-aware mappings (that also check types during insertion) also uncovered 4 test failures in the remaining RALib code. I still have to check whether these are expected errors (e.g., guard checks) or actual bugs.

Furthermore, I would continue to look into removing more raw types in the learning code (e.g., some Theory-related code) to see whether all the type information nicely play together or new problems arise.