Polymorphic types in KeY

Java has a parametrically polymorphic type system since Java 5. (co-)ADTs are typically type-parametric. Should KeY's type system not also support parametric type polymorphism?

There is a 1st attempt already somewhere #3384. Some discussions should be made beforehand anyways.

Requirements for parametric type polymorphism in KeY

1. It should be sufficiently compatible with the Java type system.
2. It should meet the requirements of FOL and ADT reasoning.

For logic and data types

• Thanks to immutability, they are (mostly?) covariant
• Question of constraints on type parameters.
• What if type system is not a lattice (-> like for Java Objects)

Some interesting definitions:

\sorts{
  \generic A
  \generic B
  seq[covariant A]
}

functions {
  seq[max(A,B)] append(seq[A], seq[B]);
  // or
  seq[A] append(seq[A], seq[A]);
  // is this sufficient if seq is covariant?
}

In the contravariant case, is the constant seq[\bot] seqEmpty then of one fixed type or is it a multi-typed constant like seq[A] seqEmpty. In KeY, we did this until now with an explicit (single) type argument like A::seqEmpty. Do we still need this? What about an empty map with two type parameters?

What about the following?

\sorts {
  \generic A;
  seq[covariant A];
  order[contravariant A];
}

\predicates {
  isSorted(seq[A], order[A])
}

Is then isSorted(seqOfInt, orderOnObject) allowed? What is A then?

Requirements in Java

• NOT List<Person> <: List<Object>
• BUT List<? extends Person> <: List<? extends Object>
• similar but contravariant for super
• Invariant originally, but can be made co- and contravariant in each of the type parameter positions
• Probably have a syntactic notation for making an argument co/contravariant.

Concrete syntax in KeY

How should type parameters be notated. Perhaps there are no conflicts, but typical options are already used for other things:

• Suffixes with angled brackets are probably not possible since names like <init>exist.
• Suffxies with squared brackets are already used for sequence access, heap update, array access.
• Curly braces are used for updates.

Scala:

• relevant for comparison: https://docs.scala-lang.org/tour/variances.html
• • or - for co-/contravariance