arXiv:1605.01480v2 [] 29 Dec 2017

On Understanding Generics: Towards a Simple
and Accurate Domain-Theoretic Model of
Generic Nominally-Typed OOP
Moez A. AbdelGawad
moez@cs.rice.edu
March 20, 2018
College of Mathematics and Econometrics, Hunan University
Changsha 410082, Hunan, P.R. China
Informatics Research Institute, SRTA-City
New Borg ElArab, Alexandria, Egypt
(Began in 2010, while graduate student at Rice University)

The Gamma function is a metaphorical extension of the factorial function. One property, its
recursion, becomes its most important feature, and serves as the basis for extending it. It’s a
bit like calling an automobile a ‘horseless carriage’, preserving its essence of carrying and
removing the unnecessary horsefulness, or like calling a railroad ferrovia in Italian or
Eisenbahn in German, focusing on the fact that it’s still a road, but one made instead of iron.
~Adapted from a quote by Columbia Physicist Prof. Emanuel Derman

One important value behind developing and presenting N OOP [2, 3, 4, 12,
6, 5, 7, 9, 8], is to provide a more precise foundation on which further OOP
research can be built. N OOP provides a capacity for better mathematical
reasoning about mainstream OO languages.
The development of N OOP was mainly motivated by the lack of a precise
model of OOP despite the prominence and domination of OOP among mainstream programmers, and the realization that extant models of OOP are deeply
flawed, inadequate, or not enough for explaining the typing features of mainstream programming languages, and are thus hindering further development of
these languages.1 A feature of mainstream OOP where such inadequacy and
hindrance of development are clear is ‘generics’.
1 The development of the process of adding “closures” to the Java programming language is
a prime example of how development of mainstream OOP languages is hindered. Also, research
done on Java wildcards has been unable to present a proof that beyond doubt convinces us
of the type safety of Java with wilcards. Also, Smith and Cartwright, in [18], present flaws in

1

Given that genericity is a useful feature for most OO developers, generics
(i.e., generic classes) are supported in most mainstream OO languages. Generics
offer OO developers with more expressive type systems.

1

Generics: A Summary of Developers Perspective

The dictionary definition of the word generic is: ‘Applicable to an entire class or
group (not tied to particulars, or unconstrained)’. For example, if we purchase
some generic dish soap, soap that has no brand name on it, we know that we
are buying dish soap and expect it to help us clean our dishes, but we do not
know what exact brand (if any) will be inside the bottle itself. We can treat it
as dish soap, even though we don’t really have any idea of its exact contents.
Similarly, in OOP, generic classes, usually called generics, provide the programmers to abstract their classes over some types, and thus to define them
“generically”, independent of the particular instantiations of them that class
users later actually use. Generics move the decision as to what actual types to
be used for some of the types used inside the class to the usage-sites of a class
(i.e., are decided by the users of the class) rather than be declared and fixed at
declaration-sites (i.e., decided by class developers).
Generics also offer OO programmers more flexibility, given that different
type parameters of a generic class can be used at different usage sites, even in
the same program. Without generics, such a capability could only be simulated
by a cooperation between class developers and class users, depending on OO
subtyping (which offers so-called ‘subtyping polymorphism’) and using the socalled ‘generic idiom’. Using the generic idiom is not a type-safe alternative to
generics, given that using it involves requiring class users to insert downcasts
by hand. Because they circumvent the type system, programs with downcasts
can be type unsafe (See [14]).
the current Java type system, particularly regarding its polymorphic methods type inference
algorithm.
Even further, at least as of version 1.6.0_16, the standard Java compiler, javac, has
generics-related bugs. For example, the following code correctly compiles with no errors
on the Eclipse Java compiler. The same code, however, generates a ‘Compile exception:
java.lang.NullPointerException’ error message when compiled using javac
class A<T> {}
class B<T> extends A<C<T>> {} // note that C<T> is used inside the supertype of B<T>
class C<T> extends B<T> {}
// note that C<T> extends B<T>
(See Oracle Java compiler bug report [1] for an updated status of this bug in javac).
We believe all such problems are due to the lack of a precise conceptual mathematical model
of mainstream OOP, particularly one that takes nominality in consideration. Even though
the problems we mention are Java-specific problems, we believe similar problems (probably
some of which are undiscovered) do exist in other mainstream OOP languages, given that the
type systems of these languages are much similar to that of Java.

2

2

Modeling Generics

Building on how we modeled nominal OOP in N OOP, and given that generics
is a typing feature of nominal OOP that crucially depends on nominality (as we
will see shortly), it is natural to expect that modeling generics mathematically
builds on top of the typing concepts we developed in N OOP, particularly on
top of N OOP signatures.
In the following, we will see that this expectation is largely true. Compared
to the modeling of nominal OOP in N OOP, the modeling of generics (or, more
accurately, the modeling of ‘generic nominal OOP’) is about allowing type variables to be used inside signatures to stand for (abstract over) other signature
names, making the plain names of signatures “gain some structure” by allowing
them to be “applied” to other signature names, and, finally, to allow any valid
combination of signature names to appear in any place inside a signature where
a “plain” (i.e., N OOP) signature name was allowed before (e.g., field signatures, and method signatures). Combinations of signature names are formed,
syntactically, by “applying” a generic signature name to other combinations of
signature names2 .
Making signatures be generic (abstracting them over other signature names,
using type variables) is sometimes called “generification”. Using generic signatures, we define ground object signatures, which, similar to N OOP object
signatures, are paired with object records to construct generic objects (i.e.,
objects that carry instantiations of generic signatures as their nominal typing
information).
Similar to how we constructed N OOP, we then build a model of generic
nominal OOP, which we call GN OOP. GN OOP includes a domain of generic
objects which we call GO. Domain GO uses ground signatures in the construction of its objects. Otherwise, GO is very similar to domain O of N OOP.
In the next two sections, we formally present generic signatures, and (a rough
sketch for) the formal construction of GN OOP. Construction of GN OOP goes
along the same lines of constructing N OOP.
As we will see in the next two sections, all features of generics, and their
modeling, are centered around the main crucial idea that names of signatures
are not plain but have some structure, indirectly implying, thus, that GN OOP
objects could roughly be viewed as “N OOP objects with structured signature
names” (rather than plain names used in N OOP).

3

Generic Signatures

Before giving the formal definitions for generic signatures, we first present an
informal view of generic signatures to help motivate the later formal definitions.
2 Generic signatures that take no parameters (“zeroary” signatures) are treated as being
non-generic signatures. When used, they can be applied only to the empty sequence of signature names.

3

3.1

Informal View

A signature constructor is a parametrized (“generified”) N OOP signature. A
signature constructor carries almost the same information a N OOP signature
does (i.e., a name, supersignatures, member signatures, ... etc). Like a N OOP
signature, a signature constructor is a syntactic typing entity.
Each signature constructor has a signature constructor name that is a plain
label. Signature constructor names have a very similar purpose in GN OOP to
that of signature names in N OOP signatures. Given its dependency on the use
of names (of signature constructors), generics is also a feature of nominal OO
programming that pivotally depends on nominality.
The main crucial difference between a signature constructor and a N OOP
signature is that, inside a signature constructor, some generic signature names
inside the signature constructor might be “missing” and have instead type variables as place holders (i.e., names are abstracted over by the type variables)3 ,
and, further, structured generic signature names have to be used inside signature
constructors (rather than plain unstructured signature names).
Following the name of a signature constructor, as an extra component in of a
signature, all type variables that might be used inside the signature constructor
are declared (in a sequence of type variables) ahead of the other components
of the signature constructor (no nesting of type variable declarations occurs
except at the top level, akin to a logical ‘prenex form’). The sequence of type
variables is ordered (hence, a sequence) but allows no repetitions (i.e., all type
variables of a signature constructor are distinct/have distinct names). Signature
constructors are thus binding constructs. As such, two signature constructors
are considered equivalent if they are equal modulo the consistent renaming of
type variables throughout the two constructors (“alpha-renaming”).
No type variable can be used/referenced inside a signature constructor without it being declared in the type variables component of the constructor. Like
a function expression in λ-calculus, the signature constructor, via its declared
type variables, is said to abstract over the ground signature names that type
variables, at usage-sites, can be instantiated to. Due to the fact that type variables cannot be “applied” (to other type names), a more accurate, and simpler,
mathematical view of signature constructors is that they are signature schemes,
rather than functions. We adopt this simpler view. We will see, in Section 3.5.3,
how this view (together with type variables being distinct, and being declared
in prenex form) helps us define a very simple notion of name substitution on signatures. All usage and properties of generic signatures in generic OOP depend
on this simple notion of substitution.
Zeroary signature constructors, i.e., ones which take no type parameters,
play the role of providing the base case for almost all inductive definitions or
proofs that involve generic signatures. Given it takes no type parameters (i.e.,
has an empty sequence of type variables), and thus has no missing information,
3 For the sake of familiarity, we keep using the name ‘type variables’ for these variables
that abstract over signature names, although, strictly speaking, they should be called ‘ground
signature name variables (See below).

4

a zeroary signature constructor, when its (empty) type variables component is
dropped, corresponds directly to a non-generic N OOP signature. Vice versa,
by adding an empty sequence of type variables to a N OOP signature it directly
corresponds to a zeroary signature constructor. (In summary, thus, each zeroary GN OOP signature constructor corresponds to a N OOP signature, and
each N OOP signature corresponds to a zeroary GN OOP signature constructor. There is a one-to-one correspondence between the two entities). Thus, in
GN OOP, as in [14], ordinary non-generified (i.e., non-generic) signature names
are identified with zero-ary signature constructor names. This is done merely
as a technical convenience.
A signature constructor environment is a finite map (a table) that maps signature constructor names to signature constructors. Like all functions/mappings,
by applying a signature constructor environment to a signature constructor
name, the corresponding signature constructor (the one with the input name)
is obtained.
To construct a generic signature name, for use either inside the supersignatures component, or the member signatures component of a signature constructor, a signature constructor name4 is paired with a (possibly empty) sequence of
‘type variables, or (nested) generic signatures names’. This sequence is called the
sequence of type arguments that are “passed” (as parameters) to the signature
constructor name to construct a generic signature name.
Relative to a certain signature constructor environment, a generic signature
name is well-formed if all signature constructor names inside it are paired with
sequences of type arguments that are the same length as the type variables
components of the signature constructors in the environment corresponding to
the signature constructor names5 .
Generic signature names can be represented as labeled abstract syntax trees.
The signature constructor name used to construct the generic signature name
is the label for the root node of the tree. The subtrees of this node are trees
that each represent an element of the type arguments sequence. Given that
type variables cannot be applied, nodes representing type variables will always
be leaf nodes in the abstract syntax tree representation of a generic signature
name.
Inside a signature constructor, ‘a type variable or a generic signature name’
(usually just called a “type”, or, more accurately, a “type name”) can appear as
the signature name of a field (in a field signature), and as the signature name
of a method parameter or the signature name of a method return value (in a
method signature). A type name can also appear as a supersignature name. To
prevent the possibility of having circular subsigning hierarchies, a plain (also
called “naked”) type variable is not allowed to appear in the supersignatures
4 Whose corresponding signature constructor is then said to be ‘instantiated’, i.e., to be
made an instance of.
5 That is, for a well-formed generic signature name, the number of type arguments must
be equal to the declared number of type parameters. The declared number is based on the
signature constructor information inside a signature constructor environment.

5

component of a signature constructor6 .
In the context of a certain signature constructor environment, well-formed
generic signature names that have no type variables (are “variable-free”) are of
special status, and they deserve some special attention: They are constructed
only out of signature constructor names, nested inside each other via the type arguments component of a generic signature name. A generic signature name that
contains no type variables (i.e., has no missing information) is called a ground
signature name. Inductively, a ground signature name is, thus, constructed
from a signature constructor name of a signature constructor that takes no type
parameters (a zeroary signature constructor) paired to the empty sequence (of
type names, as its type arguments), or is constructed from a signature constructor name of a (generic, non-zeroary) signature constructor paired to a sequence
all of whose members are themselves ground signature names (as the type arguments of the signature constructor name).
Formally, we will see below that ground signature names are finite syntactic
entities, and are members of an inductively defined set. As a subset of generic
signature names, ground signature names also can be represented by labeled
trees. Due to the absence of type variables, all leaves of a tree representation of
a ground signature name are labeled by names of zeroary signature constructors.
In fact, given that we noted above that type variables cannot occur elsewhere in
the tree representing a generic signature name except as leaves, all nodes of the
tree representing a ground signature name are labeled by signature constructors
names only.
Relative to a specific signature constructor environment, well-formed generic
signature names that are not ground signature names are called non-ground signature names. They are generic signature names that do contain type variables.
They can only appear inside signature constructors (in member signatures, or
as supersignatures).
Similar to N OOP object signatures, a generic object signature is a pair of a
ground signature name and a signature constructor environment. Non-ground
signature names are cannot be used to form object signatures.
A signature constructor whose (1) name is substituted by a ground signature name, that (2) has its type variables component removed, and (3) whose
type variables are replaced (substituted) by ground signature names consistently
throughout the signature constructor (i.e., throughout its supersignatures, field
signatures, and method signatures components) is called a ground signature.
Recalling that signature constructors are schemes, ground signatures are instances of signature constructors. Ground signatures have no type variables.
Every zeroary signature can be trivially made into a ground signature.
6 In

[10], it is discussed how MixGen in fact uses naked type variables in the supersignatures
component of a signature to define signatures of “mixins” (as OO components) on top of firstclass OO generics. In the context of mixins, there are in fact easily enforced rules that
prevent circular nominal subtyping hierarchies. [10] presents an algorithm that MixGen uses
to detect, and prevent, such circularity. Since we aim to model generics without mixins (i.e.,
to model “regular generics”) in this report, dealing with such a use of naked type variables is
unnecessary.

6

The instantiation of a signature constructor, with ground signature names as
type arguments, defines a ground signature, whose name is the ground signature
name constructed from the signature constructor name paired with the sequence
of type arguments.
Constructing ground signatures via instantiation of signature constructors
is defined using a simple notion of name substitution. Name substitution substitutes (replaces) type variables inside a signature constructor with ground
signature names.
We can easily see, thus, that in the context of a particular signature constructor environment, a ground signature name ggsn whose first component, say
nm, is the name of a signature constructor sc defines (and is also the name of) a
ground signature, say gs. gs can be obtained from sc and ggsn by substituting
the type variables V inside sc by the type arguments of ggsn (the second component of ggsn, say T N ). When we present formal definitions below, we denote
this substitution/instantiation operation that defines the ground signature gs
corresponding to ggsn by gs = {V 7→ T N }sc, meaning that, if sc has the same
signature constructor name as ggsn, and T N are the type arguments of ggsn,
then gs is defined by substituting the type variables V inside sc by the type
arguments T N of ggsn.
Name substitution plays a very important role in our mathematical (i.e.,
domain-theoretic) modeling of nominal OOP generics.
Given the use of ground signature names to define and name ground signatures, we should note that non-ground signature names do not name any
actual signature names. Instantiation, and name substitution are only defined
for ground signature names. Although, technically speaking, generic signatures
could be defined (as a general notion that embodies signature constructors as
well as ground signatures), they are not needed much in practice7 . This is
why the instantiations of signature constructors that could define these generic
signatures are disallowed.
Because non-ground signature names are names “with some missing information”, in instantiation and name substitution it has to always be guaranteed
that whenever used, non-ground signature names (which may appear inside signature constructors) are used to construct ground signature names first, which
are then the names used to refer to any ground signatures, and that when
constructing ground signature names (to define ground signatures) non-ground
signature names are never passed as type arguments “as is”.
In light of the informal definitions above, we can easily see that generic OOP
depends on names (i.e., nominality) even more than non-generic OOP.
To summarize the above, for generics we have ten name-dependent defini7 See

Section 3.6 for one such important (theoretical/meta-linguistic) need, where, for checking for well-formedness of a signature constructor in a signature constructor environment, we
need to make sure all instantiations of signature constructor satisfy a specific condition related
to the corresponding instantiations of another signature constructor. This condition involves
checking an infinite number of instantiations, which is generally not possible, unless we can
abstract over all these instantiations (using type variables, which is indeed possible in this
case).

7

tions. These are:
1. Signature constructors (which have names), signature constructor names,
and signature constructor environments (mappings from names to constructors),
2. Type variables (which, incidentally, are also mere names, but ones not
related to nominality of OOP),
3. Generic signature names (which are signature constructor names paired
with sequences of type names),
4. Type names (which are type variables or generic signature names. Note
the circular dependency on generic signature names),
5. Name substitution (which instantiates a generic signature name to a ground
signature name, and a signature constructor to a ground signature),
6. Ground signature names, and ground signatures (which result from instantiation/name substitution), and
7. Generic object signatures (which are ground signature names paired with
signature constructor environments).
Dependency on names (and nominality) allows named entities to be referenced and used before they are fully-defined (i.e., they allow circularity/mutualrecursiveness). It should be noted that generic signature entities have even a
heavier dose of circularity than non-generic ones8 .
Below we formally present all generic OOP definitions we informally discussed above.

3.2

Signature Constructors

Formally, corresponding to signature equations for N OOP, for GN OOP signature constructors we have
SC =

N × X∗ × GN∗ × (L × GNX)∗ × (L × GNX∗ × GNX)∗

(3.1)

where SC is the set of signature constructors, X is a non-empty set of type
variables9 as plain names, and where sets N, T, L and the set constructors ×
and ∗ have the same meaning as in N OOP signature equations.
8 Note, for example, that some of the definitions above mutually-recursively depend on each
other. We have signature constructors (which have signature constructor names) using generic
signature names, which, in turn, recursively use signature constructor names (a counterpart
to this sort circularity exists for non-generic signatures, via the use of signature names). Also,
generic signature names use type names, which, in turn, are type variables or, recursively,
generic signature names (Due to the absence of type variables, this sort of circularity has no
counterpart in non-generic signatures)
9 Or, more accurately, type variable names, or most accurately, ground signature name
variable names (given that “type” variables actually get instantiated only to ground signature
names).

8

X∗ is the set of (finite) sequences of type variables. As a component inside a
signature constructor, a member of X∗ is the sequence of type variables whose
members can be used inside this signature constructor. Ordering of elements
in an element (a sequence) of X∗ does matter (type arguments are matched
with type variables based on the order of each in their respective sequences).
Repetitions is not allowed allowed in elements of X∗ . Similar to all sequences,
elements of a sequence V ∈ X∗ can be referenced by their indices, e.g., Vi ,
where Vi ∈ X. # is a function whose value is the length of a sequence (e.g.,
the expression #(V ) gives the size of V ). Given that repetition is not allowed,
a sequence can also be viewed as a function from its members to their indices
(natural numbers). Thus, for example, for Y ∈ X, V (Y ) gives the index of type
variable Y in the sequence V of type variables10 . As a function, V is undefined
for indices equal to or larger than its size, nor for variable names that do not
exist in its range.
For generic signature names, we formally have
GN = N × GNX∗

(3.2)

where, for ‘a generic signature name or a type variable’ (which, inaccurately, is
sometimes also called a type, or a type name), we have
GNX = GN + X

(3.3)

(Note the mutual dependency between GN and GNX, and that only members of
N, not X, can be paired with members of GNX∗ ).
3.2.1

BNF Rules for Generic Signatures

Similar to BNF rules for N OOP signatures, the BNF rules (which allow us to
name components of generic signatures) corresponding to the definitions above
are:
sc::= (nm,[X], [gnm], [gfs], [gms])
signature constructors
gfs::= (a, gnmx)
generic field signatures
gms::= (b,[gnmx] → gnmx)
generic method signatures
gnm::= (nm,[gnmx])
generic signature names
type variables or generic
gnmx::= (0,X)|(1,gnm)
signature names
For members of gnmx when they are in printed form, the pairing with 0 and
1 is usually unnecessary, given that type variables and generic signature names
are usually syntactically distinguishable.11 The pairing is, thus, usually elided
when a member of gnmx is spelled out in this thesis.
10 Thus, if we have a sequence of signature names, say T N , assuming V is a sequence of
type variables of the same length as T N , the expression T N V (Y ) gives the signature name

in T N corresponding to a type variable Y in V . We use this notation below to define name
substitution.
11 Note that even if sets X and N where the same set (e.g., plain strings), if a non-algebraic
notation (e.g., ‘(x,y)’ for pairing) is used for expressing generic signature names (as is the case
in most mainstream generic OO languages), type variables (members of X) are syntactically

9

3.3

Ground Signature Names

A proper subset of generic signature names (i.e., a subset of set GN) that is
of special interest (see Section 3.5 for more details) is one whose members are
generic signature names that have no occurrences of type variables inside them.
We call (members of) this subset ground signature names. Ground signature
names could, more simply, be viewed as “structured signature names”, as opposed to the plain signature names used in constructing N OOP.
Thus, formally, for the set GGN of ground signature names, we have
GGN = N × GGN∗

(3.4)

(where the empty sequence of ground signature names provides the base case
for the definition).
Each member of GGN is a member of GN, but not necessarily vice versa
(Members of the difference set, GN\GGN, are the non-ground signature names,
which necessarily contain type variable occurrences).
The BNF rule corresponding to the definition of ground signature names is:
ggnm::= (nm,[ggnm])
ground signature names

3.4

Signature Constructor Environments and Generic Object Signatures

Similar to N OOP signature environments, signature constructor environments
(SCEs, members of a set SCE, for short) are finite functions from N (signature
constructor names) to SC (signature constructors), i.e., SCEs are particular
subsets of N × SC12 .
Within the context of a particular signature constructor environment sce, a
generic signature name (including ground signature names) gnm = (nm,[gnmx])
is well-formed if and only if (1) sce(nm) is defined (nm is in the domain of sce),
(2) #(tvars(sce(nm))) = #(gnmx), and (3) all nested generic signature names
in gnmx are also well-formed in sce, where tvars is a projection function that
extracts the type variables component of a signature constructor.
distinguishable, using a context-free grammar, from generic signature names (members of
GN). That is because type variables are not paired with a sequence of type arguments, since
they cannot be “applied” and thus do not take type arguments (signature constructors are,
thus, not “higher-order”), and also because, strictly speaking, signature constructors must
be applied to a sequence of type arguments (even zeroary signature constructors have to be
applied to the empty sequence of type arguments). Raw types (see Section 5.1.1) and/or
making the empty sequence of type arguments optional affects the easy distinction between
the two entities, but the distinction is still possible using context-dependent information (e.g.,
when a signature constructor is used in a signature constructor environment, which provides
the names of all signature constructors that could be referenced inside a signature constructor,
and by, possibly, giving either N or X a higher priority [Java, for example, gives higher priority
to set X]).
12 Incidentally, we might have used ⊸ (the finite records constructor) to function also as a
set constructor (making it ignore any ordering and repetitions of members of its input sets [the
defining sets] and output sets [the defined sets]). If so, then we would have SCE = N ⊸ SC.
We prefer, in this thesis, however, to limit the use of ⊸ to the construction of semantic
domains only.

10

Similar to N OOP object signatures, generic object signatures are pairs of
a ground signature name ggnm and a well-formed (See Section 3.6) signature
constructor environment sce (where ggnm, by definition, is well-formed in sce).
Generic object signatures are, thus, well-formed members of GGN × SCE. Note
that ground signature names, not the more general generic signature names, are
used to define generic object signatures.
Similar to a N OOP signature, the informal “meaning” of a generic object
signature is that its first component, the ground signature name, should be
“interpreted” in the context of its second component, the signature constructor environment (In particular, signature constructor names referenced by the
ground signature name are meant to refer to names of signature constructors in
the signature constructor environment).

3.5

Ground Signatures

Ground signatures provide a connection (and a “middle ground”) between N OOP
signatures and GN OOP signatures. Ground signatures are signature constructors that (1) use ground signature names as their names13 , (2) have no type
variables component, and (3) have type variables occurrences inside supersignatures, and member signatures substituted with ground signature names. Ground
signatures could, equivalently, be viewed as N OOP signatures with structured
signature names.
The equivalence of the two views of ground signatures is why they are considered a “middle ground” between (non-generic) N OOP signatures and (generic)
GN OOP signatures.
Formally, we have GGS, the set of ground signatures, defined as
GGS = GGN × GGN∗ × (L × GGN)∗ × (L × GGN∗ × GGN)∗

(3.5)

which is the same as the N OOP signature equation but uses ground signature
names (members of GGN) in place of plain signature names (members of N),
implying names of ground signatures have an inherent, desirable structure, and
are not plain names as those of N OOP signatures.
The fact that ground signatures provide a middle ground (expressed mathematically in the equations for S, SC and GGS) is behind the statement that
“generics saves developers typing [as in writing] time” (which has the implication of decreasing the chances for coding errors, as well), and that “generics does
not let developers do something fundamentally different than what they were
able to do without generics (but with significantly more code written)”14 .15
13 That

is, their names are members of GGN, rather than members of N.
as a refactoring technique, generics has the implication of decreasing the size of
the code that OO developers would have to maintain if they were to “encode” generics into a
non-generic OO language, e.g., using the so-called “generics idiom”.
15 Given that sets N and GGN have the same cardinality, ℵ , a one-to-one correspondence
0
(mapping) between the two sets can be used to define a one-to-one correspondence between
ground signatures and (non-generic) signatures (of N OOP), and, accordingly, to define a
mapping from ground object signatures (see below) to (non-generic) object signatures. An
14 However,

11

The BNF rule corresponding to the definition above is:
ggs::= (ggnm, [ggnm], [ggfs], [ggms])
ground signatures
ggfs::= (a, ggnm)
ground field signatures
ggms::= (b,[ggnm] → ggnm)
ground method signatures
3.5.1

Are Ground Signature Environments and Ground Object Signatures Needed?

Given the definition of ground signatures, as the result of instantiating the
type variables inside a signature constructor, it may be tempting to extend this
connection between generic and non-generic signatures to consider defining what
could be called ‘ground signature environments’, which could, it may be thought,
also provide a “middle ground” between signature constructor environments and
N OOP signature environments, and could also be, it may be further thought,
“N OOP signature environments with structured signature names”.
While defining more ground signature entities is possible mathematically, we
should note that a hypothetical ground signature environment corresponding
to a particular signature constructor environment could be an infinite function
(from ground signature names to ground signatures), unlike a N OOP signature
environment, which must be a finite function.
An example that demonstrates that a signature constructor environment can
get translated to an infinite ground signature environment is the case where inside the signature constructor environment there is a signature constructor that
has inside it a generic signature name in which the main signature constructor
name is used to construct type arguments that are then passed again to the
main signature constructor name (thus making rewriting/name substitution expansive. See [13]). Trying to instantiate this signature constructor to produce a
ground signature, and, recursively, have ground signature names inside it produce ground signatures that should be in the co-domain of the ground signature
environment will cause an infinite number of different instantiations, and thus
the domain and co-domain (or, range) of the ground signature environment will
also be infinite sets.16
In any one generic nominal OOP program, up to any (finite) moment in
time, however, only a finite number of instantiations of a signature constructor
example of functions that map ground signature names to non-generic signatures names, and
vice versa, are the so-called “name mangling” functions, such as the one used in the NextGen
implementation of Java Generics (See [11]).
16 A sample valid Java code that demonstrates a case where rewriting, if done, would be
infinite, is the following code:
class C<T> {
C<C<T>> m(){ return new C<C<T>>(); } // note the expansive return type
}
This example is similar to the recursive generics example in [11] (called recursive polymorphism in that paper), but this example, unlike the one in [11], demonstrates the use of an
expansive type in the return type of a method, rather than only inside its body (if used only
inside the body of a method, a recursively polymorphic type may not necessarily affect the
typing (i.e., signature) of the method).

12

could take place, and thus the whole set (of ground signatures) resulting from
all possible instantiations is not needed (or is “lazily” needed). This situation is
much like an inductively defined data type (of, say, lists, or natural numbers),
which has a finite set of data constructors that are then used to construct values
of that data type17 . In fact, we could explicitly formalize ground signature
names, relative to a fixed finite subset of N, as being elements of such a data
type. Given its irrelevance to the goal of modeling generics, however, except for
this brief note we do not present any further discussion of such a possibility in
this thesis.
‘Ground object signatures’ could also be defined, by pairing ground signature
names and (the undefined) ground signature environments. Given the impracticality of the latter, the former become impractical too, so we do not define
them here.
3.5.2

The Import of Ground Signatures and Their Names

The reason behind defining ground signature names is that they are the names
paired with signature constructor environments (SCEs) to construct generic
object signatures. Generic object signatures, in turn, are paired with object
records to construct the domain of (generic) objects, GO, in GN OOP (See
Section 4).
By using a more structured name for object signatures (i.e., ground signature names), when compared to non-generic OOP, generics could be viewed
as basically offering a “structuring” of the namespace of signature names, and
them providing access to a (finitely-constructed) infinite set of these signatures.
Signature constructors, via generic signature names, then, enable abstracting
over subsets of these ground signatures (subsets whose members share common
signature constructor names). Signature constructors could, thus, be considered
as functions from ground signature names to ground signatures, or, given their
syntactic nature, as signature schemes rather than functions as we pointed out
earlier. A signature constructor is an “abbreviation” for (abstracts over) an
infinite set of structurally-similar ground signatures. By instantiating a signature constructor, we obtain an instance of the set of ground signatures that the
signature constructor abbreviates (is a scheme for).
Thus, by having structured signature names, generics adds expressiveness
to an OOP language by allowing multiple (ground) signatures with the same
signature constructor name to be usable, in a type safe manner, in a single OO
program.
17 In our case, i.e., for the “data type” of ground signature names, names of zeroary signature
constructors provide the base elements of the data type, while the names of non-zeroary
signature constructors will be used (with the more basic elements) to inductively construct
the compound elements of the data type.

13

3.5.3

Constructing Ground Signatures: Using Name Substitution to
Instantiate Signature Constructors

This section presents the formal definition of the name substitution function.
As explained above, name substitution uses ground signature names to map
generic signature names to ground signature names, by replacing type variable
occurrences inside the generic signature names with ground signature names,
and, in turn, mapping a signature constructor to a ground signatures (i.e.,
to an instance of the set of ground signatures that the signature constructor
abstracts over).
Given two special properties of how type variables are used in generics,
generic name substitution has a simple definition (unlike the definition of substitution for β-reduction in λ-calculus, for example). These two special properties
are:
1. Type variables are declared all at once, at the “outer level”, with nesting
of type variables not being allowed except at that level (type variables
later in a sequence of type variables are in the scope of type variables
declared earlier in the sequence).
2. Type variables are required to have distinct names, and thus variable name
clashes (and the use of shadowing, or overriding, or so) between type
variables names are not possible (This property, together with the first
property, allows substitution to be defined in a straightforward manner
without concern for “capturing” or shadowing).
Formally, we use the following notation to denote the operation of substituting
type variables V in a signature constructor sc with type arguments T N
{V 7→ T N}sc
We first define name substitution on generic signature names, then extend this
definition to define name substitution for signature constructors. For type variables V ∈ X∗ , and T N ∈ GGN, we have
(
T N V (Y ) Y ∈ V
{V 7→ T N}Y =
Y
Y ∈
/V
(In fact, the second case, Y ∈
/ V , should not occur. The substitution in this case
should be undefined 18 ). For a generic signature name gnmx = (nm, [gnmx]),
we have
{V 7→ T N }gnmx = (nm, [{V 7→ T N }gnmx])
This definition extends naturally to signature constructors as follows:
18 And an error should be reported, meaning, for example, that the name substitution is not
the result of a proper signature constructor instantiation, or that the signature constructor is
not well-formed.

14

For a signature constructor sc = (nm, [V ], ssn, gf ss, gmss]), we have
{V 7→ T N }sc =

(nm, [V ], {V 7→ T N }ssn, {V 7→ T N }gf ss, {V 7→ T N }gmss)

(note that we require the sequence V of the substituted variables to be the same
as the type variables of sc, and also note that the substitution can be performed
without need for a signature environment)
where for a generic member (field or method) signature ms = (c, gcs), {V 7→
T N }ms = (c, {V 7→ T N }gcs), and where for a name substitution on sequences
of elements [e], of size n, we have
{V 7→ T N}[e] = [{V 7→ T N }e0 , · · · , {V 7→ T N }ei , · · · , {V 7→ T N }en−1 ]
For instantiating a signature constructor to define a ground signature, we can
thus, finally, now define
GenT oGnd(sc, T N ) = drop_tvars({tvars(sc) 7→ T N }sc)
where tvars returns the third (type variables) component of a signature constructor, and drop_tvars is a function that takes a sextuplet and returns a quintuplet without the third component of the input (drops it), and, by extension
to generic object signatures, for a generic object signature gos = (ggnm, sce)
we define a ground signature ggs where
GenT oGnd(gos) =

GenT oGnd(sce(f st(ggnm)), snd(ggnm))

where f st and snd return the first and second component of a pair, respectively (and thus for the ground signature name ggnm they return the signature
constructor name used to construct ggnm, and the type arguments to that
constructor name, respectively).
Claim 1. It is relatively clear that for a generic object signature gos, GenT oGnd(gos)
is a ground signature with ground signature name f st(gos).
For a generic object signature gos, one may also try defining a ground signature environment that, if paired with the ground signature name of gos, would
define a ground object signature. This definition would have to produce infinite
ground signature environments for some generic object signatures, i.e., ones
containing signature constructors with ‘recursive generics’ in their signature
constructor component.
It should be noted that the GenT oGnd function loses some information, and
is thus not a reversible function. More concretely, this means that while a generic
object signature can be mapped to a unique ground signature, it is not possible
to reverse the work of GenT oGnd by mapping the resulting ground signature
back to a unique generic object signature, and thus it cannot be mapped back to
the same generic object signature that produced it. Intuitively, this is impossible
because there are multiple ways to “generify” a non-generic ground signature
(i.e., many ways to make a non-generic signature be generic). Because of such
an information loss, GenT oGnd is called an erasure function.
15

3.6

Well-formed Generic Signatures

Similar to what we have for N OOP, only well-formed generic signatures are
used in constructing GN OOP. Well-formed generic signatures satisfy seven
constraints.
(1-4) The first four well-formedness constraints for N OOP are almost the
same for generic signature constructors and signature constructor environments,
with the only difference being that names (members of set N) now refer to
signature constructors not to signatures.
(5) We also require, for a signature constructor to be well-formed, that all
generic signature names inside it to be well-formed (See Section 3.4), and for
type variables inside the signature constructor to be members of its type variables component.
(6) The generic counterpart of the (No cycles in supersignatures) condition
requires that when the supersignatures hierarchy of a signature constructor
is recursively followed, via signature constructor names inside the signature
constructors, and via the bindings of these in the signature environment, each
signature constructor in the co-domain of a well-formed signature constructor
environment has to have no cycles in its list of supersignatures (i.e., it has no
‘infinite ascending chains’ of “super” signature constructors). The names of the
supersignature constructor names are obtained from the first component (the
“head”) of the generic supersignature names.
(7) The generic counterpart of the (Signatures inherit signatures of members
in supersignatures) condition is the most interesting well-formedness condition.
Like for N OOP, members in well-formed signature constructors that are inherited from (have the same name in) supersignature constructors are required
to have the same signature they have in the supersignature constructors when
the supersignature constructors are instantiated with the (generic) signature
names declared in the subsignature. This condition can be checked by making
a name substitution (See Section 3.5.3) on the supersignature constructor using
the generic signature name parameters used in the supersignatures component
of the subsignature constructor. The signatures of members of the generic signature resulting from the substitution will be checked for being exact matches
with signature of the corresponding members in the subsignature constructor.
By using a generic signature name (which abstracts over all possible instantiation of the signature construction) in the substitution, it is made sure that all
instantiations of the subsignature constructor satisfy the “member signatures
matching” condition of the corresponding instantiation of the supersignature
constructor. If signatures of all members of a signature constructor match the
signatures of members the constructor shares with all its supersignature constructors, the signature constructor is well-formed.

3.7

Equality of Generic Signatures and Extension of SCEs

Equality of well-formed generic signature entities is defined not much differently
from the definition of equality of N OOP signatures, except that the exact names

16

of type variables in signature constructors are irrelevant, and thus equality is defined modulo “alpha-renaming” of type variables. Otherwise, equality is defined
component-wise using equality of components of generic signatures as syntactic
elements (just like for N OOP signatures).
Given that well-formed signature constructor environments are “minimal”,
by well-formedness conditions, extensions of signature constructor environments
are defined exactly in a similar manner to their definition for N OOP signature
environments. A signature constructor environment sce1 extends a signature
constructor environment sce2 if, modulo alpha-renaming of type variables, all
members of sce1 (name/signature constructor pairs) are members of sce1 (and
thus sce1 is a superset of sce2 ).

3.8

Inheritance and Subsigning of Generic Signatures

In a signature constructor environment sce, a signature constructor sc has a supersignatures component, ss, that specifies for each instantiation of sc, which defines a ground signature gss, what ground signatures are the ground supersignatures of that instantiation. Ground supersignatures are decided by the supersignatures component of gss. When the substitution is, transitively, done throughout the supersignatures hierarchy (which is of finite size, by well-formedness
rules), all ground supersignatures of gss can be obtained. In agreement with
nominal subtyping, a pair of ground signatures (gss1 , gss2 ) is in the subsigning
relation if and only if the ground signature name of gss2 is a member of the set
of names of the ground supersignatures of gss1 .
The supersignatures component of a signature constructor is thus considered
to define a pointwise subsigning relation, between ground signature instantiations of the signature constructor and instantiations of its explicitly declared
supersignature constructors..
Thus, for two well-formed ground object signatures gos1 = (ggnm1 , sce1 )
and gos2 = (ggnm2 , sce2 ), we have
gos2 E gos1 ⇔ sce2 ◭ sce1 ∧ (ggnm2 = ggnm1 ∨ ggnm1 ∈ gss(sce2 , ggnm2 ))
(3.6)
where gss is a projection function that computes the set of all ground supersignatures names of a given ground signature name (ggnm2 ) in a given signature constructor environment (sce2 ) by, transitively, going throughout the
supersignature hierarchy. gss uses name substitution to obtain these ground
supersignatures names.

4

GN OOP: A Domain Theoretic Model of Generic
OOP

Construction of GN OOP mostly resembles the construction of N OOP. The
main difference between generic objects of GN OOP and non-generic objects of
N OOP is the use of generic object signatures in constructing generic objects
17

in place of the (non-generic) object signatures used in constructing N OOP
objects.
Given its great similarity to N OOP construction, we only skim through the
construction of GN OOP (in the next two subsections). We then discuss the
properties of GN OOP in Section 4.3.

4.1

GN OOP Domain Equation

The domain equation used to construct GN OOP is the same as the N OOP
domain equation, with a domain GO, of generic objects, replacing domain O,
and using the (flat) domain of generic object signatures, SGO , in place of domain
SO of N OOP object signatures. The domain L and domain constructors ×,
⊸, →, ∗ retain their same meanings.
GO = SGO × (L ⊸ GO) × (L ⊸ (GO∗ → GO))

(4.1)

Similar to the construction of COOP [2, 3, 5], a model that represents the ‘core’
of GN OOP could be constructed, using the domain equation
GO = L ⊸ (GO → GO) + B

(4.2)

but the model constructed using this domain equation would be precisely the
same as COOP, because COOP uses no signatures, and so does Equation (4.2).
Thus, like it does for N OOP, COOP functions as a simple, structural core of
GN OOP as well.

4.2

GN OOP Construction

The construction method of GN OOP is the same method used for constructing
N OOP, where the construction proceeds in iterations, guided by the structure
of the right-hand-side of domain equation (4.1) (which has precisely the same
structure as that of the right-hand-side of the domain equation of N OOP).
Similar to filtering of pre-N OOP to define N OOP, GN OOP filtering is responsible for ensuring generic object records are matched with concrete generic
object signatures where member signatures in the generic object signatures
match those in the object records (note that generic object signatures define
ground signatures, whose member signatures are used to decide the matching).

4.3

Properties of GN OOP

Similar to our investigation of some main properties of N OOP, and using terminology used there, we also interpret generic object signatures of GN OOP as
denoting nominal object types, where we will have
GS[gos] = {go ∈ GO|∃goss ∈ SGO , gr ∈ GR.(goss E gos) ∧ (go ⊑ (goss, gr))}
(4.3)
18

where GR is the generic object records counterpart of domain R of N OOP
object records.
Similar to what we did for N OOP, it is easy, using essentially the proof we
developed for N OOP (only slightly appropriately adjusted for GN OOP), to
prove that generic nominal types denoted by generic object signatures are weak
ideals in domain GO.
Similar to what we did for N OOP, based on the definition of the interpretation of a GN OOP generic object signatures and the definition of the interpretation of a N OOP non-generic signature being very similar, we also use
essentially the same proof we developed for N OOP to prove that in GN OOP
the inheritance and generic nominal OO subtyping are completely reconcile
(i.e., that adding generics to a non-generic nominal OO language preserves the
reconciliation).
Formally, thus, similar to the ‘inheritance is subtyping’ theorem for N OOP,
for GN OOP we also have that
gos1 E gos2 ⇔ GS(gos1 ) ⊆ GS(gos2 )

(4.4)

That is, one fully instantiated class type is a subtype of another fully instantiated type only if its fully instantiated signature subsigns the former (the ⇐
direction in 4.4). If subsigning holds, then the instantiated supertype signature
name must appear in the chain of instantiated supertypes for the subtype. Then
signature matching implies that the weak ideal of the subtype is contained in
the weak ideal of the supertype (the ⇒ direction in 4.4).

5

Modeling More Generic OOP Features

Although the modeling and analysis of more features of generic OOP is mostly
considered future work and beyond the scope of this thesis, we here present
a necessarily-incomplete basis for such future work and we present some main
ideas we intend to build on and develop in the near future.
First, given that Java implements a somewhat-limited notion of generics on
a virtual machine that has no notion of generics (the JVM [16]), using a technique and concept called erasure 19 , we would like to make a full assessment of
this technique, by building a model for erased generics. Building on concepts we
presented in earlier sections of this report, we present in Section 5.1 the basis on
which we can build such a model of erased generics (which is called EGN OOP).
We will see that erased generics (generics implemented via erasure) provides an
approximation20 for full generics, since it basically ‘saves programmers from
using the “generic idiom” but does not give them the full power of generics’, including support for generic type-dependent runtime operations (such as creating
objects of type variable types [i.e., type specified using naked type variables]).
Next, in Section 5.2, we will discuss how to incorporate bounding type variables, so that rather than allowing a signature constructor to be instantiated
19 Generics,
20 Not

as implemented in Java is sometimes, thus, called “second-class generics”.
in a domain-theoretic sense!

19

using any ground signature name (which has been the case so far), some subtyping constraints about possible type argument instantiations is made on type
variables, and these constraints are guaranteed to be satisfied for passed-in type
arguments.
‘Raw types’ is not only an artifact of erasure, but also arise in Java from
the need for supporting “migration compatibility”, where erased and non-erased
code need to co-exist. We discuss raw types in Section 5.1.1.
Wildcards, as a main motivation behind developing N OOP and GN OOP,
try to increase the expressiveness of generics. Wildcards lessen the mismatch between subtyping polymorphism and generics, by allowing unknown types (with,
or without known upper and lower bounds) to be passed as type arguments
to signature constructors. Using generics terminology of Section 3, wildcards
allow the naming and the referencing of more ground signatures. Wildcards are
discussed in Section 5.3.
In Section 6, we briefly discuss how polymorphic methods could be modeled.
Even though not a must, polymorphic methods are supported in virtually all
OO languages that support generics. Generics allows abstracting full objects
(i.e., all their members) over type arguments, while polymorphic methods allow
abstracting individual methods of objects over type arguments.
While the discussions in the sections on modeling erasure and polymorphic
methods are more technical, the discussions are less technical in the rest of the
sections on modeling other generic OOP features.
We start the discussion of more generic OOP features by discussing erasure.

5.1

Erasure and Erased Generic OOP (The “Generics Idiom”)

Erasure as a technique using in some mainstream OO languages, most notably
Java, for supporting generics when first-class generics is not possible to support.
Erased generics thus only approximates full generics (when information is lost
due to erasure, an operation the depends on the erased information is disallowed, or a warning is produced). Erasure produces code that a non-generic
OO developer “would have written (using the ‘generic idiom’)” if they had no
generics. This is the essential intuition behind erased generics in Java. The
definitions accurately capture this intuition.
The generics idiom, and erased generics accordingly, crucially depend on
the existence of a type (a signature constructor) at the top of the subtyping
hierarchy (typically Object).21 The generics idiom, and erased generics, also
depend on the observation that in the full-generics semantics all instantiations
of a signature constructor have the same members, only with different member
signatures22 .
21 This is why Java Generics does not support generics using primitive types, because Java
primitive types of Java are outside the object subtyping hierarchy, and are not subtype of
Object.
22 The Java compiler tries to compensate for the difference in members signatures by using
type cast operations that are never guaranteed to fail.

20

Using our modeling of generics presented in earlier sections, in an OO language where all object types have a common supertype (and without type variables having bounds—see §5.2), erasure is equivalent to instantiating a signature
constructor with one type then using the signature constructor name to refer to
this particular instantiation (rather than the ground signature name).
The erasure of a ground signature name ggnm = (nm, [ggnm])
GndT oN onGen(ggnm) = nm
(That is, the erasure of the ground signature name ggnm is simply the name of
the signature constructor used to construct ggnm23 ).
If we abbreviate the GndT oN onGen function to ⌈·⌉, then the erasure of a
ground signature ggs = (ggnm, [ggnm], [ggfs], [ggms])24 is
⌈ggs⌉ = (⌈ggnm⌉ , [⌈ggnm⌉], [⌈ggf s⌉], [⌈ggms⌉])
For a signature constructor environment sce = {. . . , (nm, sc), . . .}, its erasure is
⌈sce⌉ = {(nm, ngs)|(nm, sc) ∈ sce ∧ ngs = ⌈GenT oGnd(sc, Object)⌉}
(check Section 3.5.3 for the definition of the GenT oGnd function).
That is, the definition of erasure for signature constructor environments
converts a signature constructor in the environment to a ground signature by
instantiating it with a sequence of type arguments whose elements all having
the same value: namely, signature constructor name Object (which we assume
is the type at the top of the subtyping hierarchy).
Equivalently, without making a detour via ground signatures, we could state
that ngs is the result of taking out the type variables component of sc, replacing each plain (i.e., naked) type variable by Object, and dropping the type
arguments of all generic signature names (i.e., we only keep the outer signature
constructor name). Given that plain type variables are not allowed in the supersignatures component of sc, this shows that the supersignatures component of
the result signature will use the same signature constructors of the supersignatures component of sc (This property plays an important role in preserving the
inheritance and subtyping properties of the resulting erased-generic entities.)
For a generic object signature gos = (ggnm, sce), its erasure, egos is
egos = (⌈ggnm⌉ , ⌈sce⌉)
Theorem 1. If a GN OOP generic object signature gos is well-formed, its
erasure, egos, is a well-formed non-generic N OOP object signature.
23 Erasure of ggnm is a reminiscent reminder of the mathematical ceiling function, ⌈.⌉,
which computes the smallest integer greater than or equal to a floating point number.
24 Erasure of a ground signature is like first converting the floating number 3.2 to the floating
number 3.0 (corresponding to instantiating with Object), then referring to that new floating
number using (the symbol for) the integer 3 (by dropping type arguments of generic signature
names).

21

Proof. By induction on the structure of gos, and by noticing that ⌈·⌉ produces
N OOP signature name for given GN OOP ground signature name, produces
N OOP signatures for GN OOP signature constructors, and produces N OOP
signature environments for GN OOP signature constructor environments.
A domain of erased-generics objects constructed using these erased-generics
object signatures, based on N OOP domain equations (or GN OOP domain
equations, for this matter), will produce a domain, EGO, isomorphic to the
domain O of N OOP of non-generic objects. It is this domain that is used
to interpret generics in Java. The erasure of generic information (i.e., its unavailability at runtime) limits the operations a Java developer can perform on
generic types (at compile time) to ones that will be type sound even without
such information (dynamic dispatch is type safe, while new and ‘cast’ operations
cannot be performed on plain type variables).
5.1.1

Java Raw Types

‘Raw types’ refers to using non-structured plain signature constructor names as
generic signature names, simultaneously while using (structured) generic signature names. Raw types are an artifact of Java erasure that are only motivated
by attempting to maintain “migration compatibility”. Migration compatibility allows Java developers to simultaneously use generic and non-generic code,
while motivating them to use generics. The Java type system gives unmodified
non-generic code a generic interpretation. Raw types are best understood as
generic signature names that are “missing type parametrization information”25 .
We relegate further analysis of raw types to future work.

5.2

Bounded Type Variables

For more expressive and more precise typing, type variables in generic OOP are
usually provided with type bounds. An upper type bound on a type variable tells
that all instantiations of the type variable will be guaranteed to be subtypes
of the provided bound. A lower type bound of a type variable tells that the
provided bound will be guaranteed to be a subtype of all instantiations of the
type variable. Bounds on type variables of generic classes make use of the
naturally-supported subtyping relation in OOP. In this section, and thus in
25 Raw types are much like ‘unbounded wildcard types, or erased types, with automaticallyinserted type casts that are not guaranteed to succeed’ (See Section 5.3 for a brief discussion of
Java wildcards). Just like a Java program with downcasts, or “stupid casts” is not guaranteed
to be free of type errors (see [14]), also a Java program with raw types (which are used as
generic types) is not guaranteed (or cannot be decidably guaranteed) to be free of type errors.
A Java program with raw types that are always used as non-generic types, as is the case
in pre-generics Java (i.e., Java 4.0-), can be decidably guaranteed to be free of type errors.
Generification helps the type system decide type safety. Generification can somewhat be
viewed as providing the type checker with the “non-decidable” portion of the analysis it does
while type checking. Otherwise generification would be an automatable process (Generification
is believed to be an undecidable problem).

22

this thesis, we only discusse upper type bounds of generic type variables, and
relegate a discussion of lower type bounds to future work.
An upper type bound of a type variable allows a class designer to assume
that certain members do exist in objects of any valid instantiation of the type
variable, and, because of nominality associating a behavioral contract with type
names, to also assume that all instantiations of the type variable stick to the
behavioral contract associated with the name of the type bound.26
Formally, adding upperbounds (upper type bounds) to type variables, amounts
to a small addition to signature constructors, where the type variables component is not a sequence of type variables (names from set X), but a sequence of
pairs of type variables and bounds, where bounds are members of the set GN27 .
We thus define
UBX = X × GN
and we could now redefine signature constructors
SC =

N × UBX∗ × GN∗ × (L × GNX)∗ × (L × GNX∗ × GNX)∗

(5.1)

Other than this small change, all other definitions we had in Section 3 remain
exactly the same. Type variable bounds, however, add few more definitions and
concepts.
5.2.1

Valid Signature Constructor Instantiations and Valid Ground
Signature Names

The main change done to our modeling of generics by having upper bounds is
that it introduces, on top of the notion of well-formed signature constructor
instantiations (which we have seen in Section 3), the notion of valid signature
constructor instantiations. Rather than using generic object signatures that
are only well-formed, valid generic object signatures (which use valid signature
constructor instantiations) are now used to construct the domain of generic
objects GO of GN OOP to model objects of generic OOP where type variables
have bounds. The addition of type variable bounds thus affects values in the
domain.
A valid signature constructor instantiation is a well-formed generic object
signature whose type arguments do satisfy the upper bound constraints on the
corresponding type variables they instantiate. A type argument must be a subsign of the upper bound of the corresponding type variable. This condition
cannot be considered a well-formedness condition. As we have seen in Section 3.6, and Section 3.8, subsigning is defined for well-formed signature constructor instantiations, by implicitly assuming they are instantiated with valid
26 For example, a class that provides (i.e., whose instances provide) a generic sorting “service”, needs to be sure that whatever elements (objects) it orders do actually support ordering.
The type of these elements will be provided to the “sorter” generically, as a type variable,
but will be required, via an upperbound, to provide “proof” that its elements (of the type) do
support ordering, e.g., by having a compare() or leq() (less-than-or-equal) method.
27 Not the set GNX. We do not allow type variables to bound type variables, but only
to appear as type arguments in the bounds. Even though the consequences of lifting this
restriction could be interesting to investigate, we do not do so here.

23

type arguments (all instantiations were valid at the time, and thus there was
no need for an explicit validity check). Checking validity of an instantiation depends on the subsigning relation being defined. If validity were to be considered
part of well-formedness then a circularity would ensue between the definition
of subsigning and well-formedness. Luckily, this circularity can be resolved by
introducing the notion of validity, which is defined after the subsigning relation
is defined, which, in turn, is defined after well-formedness is defined. Subsigning
(between two instantiations) is thus defined assuming that the instantiations are
valid. A decision made regarding subsigning does not later change if the either
of the instantiations is discovered to be invalid28 .29
Within the context of a signature constructor environment, thus, a valid
ground signature name is a well-formed ground signature name with the additional condition that when the arguments are substituted (via name substitution) in the upper bounds of the signature constructors the required subsigning
constraints will hold in the subsigning relation.
Formally, in the context of a signature constructor environment sce, ggn =
(nm, [ggn]) if ggn are valid ground signature names30 , and if and only if when
we define
xub = tvars(sce(nm))
we have
ggn E {xub 7→ ggn}ub(xub)
where tvars is a function that projects a signature constructor to its type variables component (now a member of UBX), ub returns the second component
(the upper bound) of a pair (subsigning between pairs of ground signature constructor names is extended to sequences of pairs in the obvious way [i.e., by
conjunction]). Note the use of ggn on both sides of the E relation, where it is
used as the substitutant on the r.h.s of E.
To construct a domain corresponding to these new instantiations, the only
change in the construction is to redefine domain of signatures used to construct
GN OOP to be the flat domain of valid generic object signatures (which use
valid ground signature names).
Given that we allow type variables to appear as arguments in their bounds,
substituting type arguments in their bounds then checking if those same arguments subsign these instantiated bounds, allows for a form of generics called
28 This

is the key observation behind not needing to redefine subsigning for valid instantiations, and then redefine valid instantions and so on ad infinitum.
29 This split between well-formedness (as a more syntactic condition) and validity (as a more
semantic condition), however, does introduce the annoying, but inevitable, notion of “wellformed yet invalid” ground signature names. An example from Java is the ground signature
name Enum<Object>, which is a well-formed instantiation of the generic Enum signature, but is
invalid because Object is not a subsign of the bound on Enum’s type variable (in the case of this
particular instantiation, the bound on the type variable of class Enum, given its declaration
in the Java class library, would , a little bit confusingly, be Enum<Object> itself. In Java,
Object is not a subsignature of any other signature but itself [its supersignatures component
is empty]).
30 Note that instantiations of zeroary signature constructors (only one such “instantiations”
is possible) are all valid.

24

F-bounded generics (corresponding to the notion of F-bounded polymorphism,
of structural OOP). F-bounded generics, arguably, provides more flexibility to
generic nominal OOP by allowing better typing of so-called “binary methods”.
Even though we have many interesting ideas related to them, we relegate further
analysis of F-bounded generics, of so-called self-referential F-bounded generics
(like in class Enum of Java), and of the generics-based solution to the problem
of binary methods to future work.
5.2.2

Type Variable Bounds and Erasure

Upper type bounds on type variables offer a chance to do a little better regarding
the information lost when interpreting generics using erasure (See Section 5.1).
Due to the possible use, inside a class, of the members of the bound, having a
better erasure precludes the use of “guaranteed-to-not-fail” type casts to make
such accesses (method calls, or field accesses).
In this case , because it is more precise (more informative) than type Object,
the erasure of the upper bound of a type variable is itself used, rather than type
Object, as the erasure of the type variable when the type variable occurs naked
inside a signature constructor.

5.3

Java Wildcards and Variance Annotations

‘Variance annotations’ is a feature of OOP generics that helps resolve the mismatch between subtyping polymorphism and generics, and to combine the power
of the two type-abstraction features.
Because of supporting mutation (which we do not model in N OOP nor
GN OOP), a type like LinkedList<Integer> and LinkedList<Number> are
unrelated by subtyping, even though type Integer is a subtype of type Number.
Variance annotations is a feature that tries to resolve this mismatch. There are
two styles for specifying variance annotations: declaration-site variance annotations, and usage-site variance annotations. Declaration-site variance annotations attach “annotations” to type variables of generic classes that limit how
type variables can be used in the class (eg, as type of arguments to methods,
or as return types of methods). Declaration-site variance annotations are used
in languages such as Scala and C#. Usage-site variance annotations attach
annotations to type arguments of generic class instantiations that limit how
type variables used in the signature of methods of instantiations of a generic
class are viewed outside (See [15] for a more detailed discussion of variance
annotations). Java wildcards are the Java incarnation of usage-site variance
annotations (See [19]).
Given the dependence of variance annotations on the nominal subtyping
relation of OO languages, any accurate analysis of OO variance annotations
should depend on having a precise model of nominal subtyping. Thus, having
GN OOP should help better reasoning about wildcards.
In this section we do not dig into modeling wildcards, but having GN OOP
at hand enables us to consider more precisely what could be involved if a full

25

model of wildcards is developed.
Our most critical observation is that with wildcards (or variance annotations,
more generally), infinite chains of supertypes could now occur in the subtyping
relation of signature constructor instantiations. Given the declaration of class
Enum in Java, and with a typical class declaration that has the heading class C
extends Enum<C>, consider, for example, the chain of Java types C, which has
Enum<C> as a supertype (given the declaration of class C), which, by subtyping
rules for wildcard types, has supertype Enum<? extends C>, which in turn
has Enum<? extends Enum<C>> as a supertype, which has Enum<? extends
Enum<? extends C>>> as a supertype, which has Enum<? extends Enum<?
extends Enum<C>>>> as a supertype, ... and so on.
It is our opinion that having infinite supertype chains makes the semantics
of full wildcards problematic, pending a detailed development of an elaborate
model of wildcards. We do not see, however, a simpler way to handle full
wildcards.

6

Polymorphic Methods

Polymorphic methods are usually associated with generics, but, despite some
similarity, polymorphic methods are not an artifact of generics (generic classes)
per se. Type variables of a generic class are shared by all methods. Polymorphic methods provide method-specific type variables. The declared type
variables of a polymorphic method can be used in the signature and the code
of that polymorphic method only. Polymorphic methods give more power and
expressiveness to OO type systems.
Just like signature constructor type variables, method type variables allow
a method signature to be abstracted over a set of signature names, allowing the
same method to be used with different signature name instantiations.
In this section we give few core formal definitions for formally modeling
polymorphic methods.
For signature constructors, we add an extra method type variables component Y∗ to sixth component of signature constructors (i.e., their method signatures component), and we use a separate set, GNY, for types that can be used
in method signatures.
SC =

N × X∗ × GN∗ × (L × GNX)∗ × (L × Y∗ × GNY∗ × GNY)∗
GN = N × GNX∗
GNX = GN + X

where for method signatures, we have
GNM = N × GNY∗
GNY = GNM + X + Y

26

(as expected, method type variables cannot be used except in the types of the
method that declares them, not in other parts of the signature constructor,
whether that is other methods, fields, or the supersignatures of the signature
constructor). Note that because of the X variant of GNY the type variables of
a signature constructor can be used inside a method signature.
We leave the rest of research work needed to model polymorphic methods
to future work. We expect it not to be too difficult since polymorphic methods
merely involve an additional level of schematic abstraction and application.

7

Concluding Remarks

N OOP enables proper mathematical reasoning about mainstream OO languages. Developing GN OOP based on N OOP has made ‘understanding generics’ an “application” demonstrating the utility of N OOP (i.e., of modeling nominal typing in particular). Reasoning about generics is not possible using earlier
models of OOP. Because of them being structurally-typed and structurallysubtyped, earlier models of OOP, in fact, do not allow us to evaluate any interesting properties of nominal OO languages because the typing systems are
fundamentally incompatible.
Even without using GN OOP to reason about many generic OOP features,
one immediate value of developing it is it dispelling a misconception that by
supporting generics the type system of Java and similar languages is ‘a complex
hybrid of nominal and structural type systems’ (See [17, p.254]). Looking at
GN OOP, it is clear that all OO typing features of Java, generic ones and ones
unrelated to generics, are purely nominal. We believe the misconception that
Java has become ‘a hybrid’ may have been due to confusing the ‘structure’
that generics does add to signature/type names (which is indeed important
in GN OOP) and the ‘structure’ of objects and classes (i.e., the set of object
members and their signatures) which is the relevant structure that structural
type systems refer to and are interested in.

8

Approach Extension

The author is also currently considering extending the above approach to generics and simplifying it. The extended approach is based on what is tentatively
called ‘nominal intervals’ and ‘single-nested generics’. A nominal interval is a
type variable name with both upper and lower bounds. In this approach, basically every type (including wildcard types) written inside a class is “captured”
(not certain yet if that’s the right term) into a synthetic type variable (a nominal interval) of the class. For single-nested generics, because of the capturing in
synthetic type variables, a type argument (like any type inside the class now)
can always be a type variable (a nominal interval), not a generic type. In this
simplified approach, class names/type names/signature constructor names will
appear only in bounds of type variables (interval bounds).

27

For this approach, the equations for generic signatures will be along lines of
the following (Y is now the set of synthetic and original type variable names):
GN = N × Y∗
GNY = GN + Y
(Note single-nesting of generic types. No mutual dependency between GN and
GNY as that between GN and GNX above)
YB = Y × GN × GN
(Note nominal intervals. All type variables will have lower and upper bounds,
in addition to a name. Can be extended to YB = Y × GNY × GNY?)
SC =

N × YB∗ × GN∗ × (L × Y)∗ × (L × Y∗ × Y)∗

(Note: all types of fields and methods are now replaced by references to type
variables/nominal intervals).
We expect this approach to allow better modeling of Java wildcards and
Java erasure.

References
[1] Moez A. AbdelGawad. Generic supertype not allowed to use generic
subtype (http://bugs.sun.com/bugdatabase, bug id=7009524), December
2010. 2
[2] Moez A. AbdelGawad. NOOP: A Mathematical Model of Object-Oriented
Programming. PhD thesis, Rice University, 2012. 1, 18
[3] Moez A. AbdelGawad. NOOP: A Nominal Mathematical Model Of ObjectOriented Programming. Scholar’s Press, 2013. 1, 18
[4] Moez A. AbdelGawad. A domain-theoretic model of nominally-typed
object-oriented programming. Journal of Electronic Notes in Theoretical
Computer Science (ENTCS), DOI: 10.1016/j.entcs.2014.01.002. Also presented at The 6th International Symposium on Domain Theory and Its
Applications (ISDT’13), 301:3–19, 2014. 1
[5] Moez A. AbdelGawad. Domain theory for modeling oop: A summary.
Technical report, arXiv.org:1406.7497 [], 2014. 1, 18
[6] Moez A. AbdelGawad. Domains for OOP semantics (extended abstract).
Technical report, The International Workshop on Domain Theory and Applications (Domains XI), Paris, France, 2014. 1

28

[7] Moez A. AbdelGawad. A comparison of NOOP to structural domaintheoretic models of object-oriented programming.
Technical report,
arXiv:1603.08648 [], 2016. 1
[8] Moez A. AbdelGawad. In nominally-typed OOP, objects are not merely
records and inheritance Is subtyping. Under preparation for journal publication, 2016. 1
[9] Moez A. AbdelGawad. Why nominal-typing matters in OOP. In Submitted
for publication in Onward! Essays, 2016. 1
[10] Eric Allen, Jonathan Bannet, and Robert Cartwright. A first-class approach to genericity. In OOPSLA’03, 2003. 6
[11] Eric Allen, Robert Cartwright, and Brian Stoler. Efficient implementation
of run-time generic types for Java. In IFIP WG2.1 Working Conference on
Generic Programming, 2002. 12
[12] Robert Cartwright and Moez A. AbdelGawad. Inheritance Is subtyping
(extended abstract). In The 25th Nordic Workshop on Programming Theory
(NWPT), Tallinn, Estonia, 2013. 1
[13] Douglas R. Hofstadter. Gödel, Escher, Bach: an Eternal Golden Braid.
Basic Books, second edition, 1999. 12
[14] Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight
Java: A minimal core calculus for Java and GJ. ACM Transactions on
Programming Languages and Systems, 23(3):396–450, May 2001. 2, 5, 22
[15] Atsushi Igarashi and Mirko Viroli. On variance-based subtyping for parametric types. In In ECOOP, pages 441–469. Springer-Verlag, 2002. 25
[16] Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification,
2nd Edition (Updated with Java 5.0 Changes). Second edition, 1999, 2005.
19
[17] Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.
27
[18] Dan Smith and Robert Cartwright. Java type inference is broken: Can we
fix it? OOPSLA, pages 505–524, 2008. 1
[19] Mads Torgersen, Christian Plesner Hansen, Erik Ernst, Peter von der Ahé,
Gilad Bracha, and Neal Gafter. Adding wildcards to the Java programming
language. In SAC, 2004. 25

29

