Skip to content

Polymorphic types in KeY

Jump to bottom
Mattias Ulbrich edited this page Feb 17, 2025 · 4 revisions

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?

The special case of Map

Assume define the ADT Map[A,B] which is meant to model functions from A to B. Let us consider super and sub types of A and B and call them A_sup, A_sub, B_sup, B_sub.

What subtyping is to be expected:

  1. Map[A,B_sub] <: Map[A,B] This relation is disputed the least. Unless maps are required to be surjections, going into the larger type is ok.
  2. Map[A_super, B] <: Map[A,B] If we consider maps as total functions then applicability as a total functions remains if the domain is restricted from A_super to A.
  3. Map[A_sub, B] <: Map[A,B] If we instead consider maps as partial functions, i.e. weakly functional collections of tuples, then it is admissible to widen the domain, not restrict it.

With the two interpretations of Map the respective other view is "wrong". The declaration of type Map hence depends on the modelling and the use case ...

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:

Clone this wiki locally