Semantic subtyping is an approach for defining sound and
complete procedures to decide subtyping for expressive types,
including union and intersection types; although it has been
exploited especially in functional languages for XML based
programming, recently it has been partially investigated in
the context of object-oriented languages, and a sound and
complete subtyping algorithm has been proposed for record
types, but restricted to immutable fields, with union and
recursive types interpreted coinductively to support cyclic
objects.
In this work we address the problem of studying semantic
subtyping for imperative object-oriented languages, where
fields can be mutable; in particular, we add read/write field
annotations to record types, and, besides union, we consider
intersection types as well, while maintaining coinductive
interpretation of recursive types. In this way, we get a richer
notion of type with a flexible subtyping relation, able to
express a variety of type invariants useful for enforcing static
guarantees for mutable objects.
The addition of these features radically changes the defi-
nition of subtyping, and, hence, the corresponding decision
procedure, and surprisingly invalidates some subtyping laws
that hold in the functional setting.
We propose an intuitive model where mutable record val-
ues contain type information to specify the values that can be
correctly stored in fields. Such a model, and the correspond-
ing subtyping rules, require particular care to avoid circularity
between coinductive judgments and their negations which,
by duality, have to be interpreted inductively.
A sound and complete subtyping algorithm is provided,
together with a prototype implementation.