Using Category Theory in Modeling Generics in OOP (Outline)

TL;DR

This paper explores how category theory tools like adjunctions, monads, and operads can be applied to model generics in object-oriented programming languages, offering a new theoretical perspective.

Contribution

It introduces a category-theoretic framework for modeling generics in OOP, extending previous order-theoretic approaches with advanced categorical concepts.

Findings

Category theory tools effectively model generics in OOP.

The approach provides a unified theoretical framework.

Potential for improved understanding of generics semantics.

Abstract

Modeling generics in object-oriented programming languages such as Java and C# is a challenge. Recently we proposed a new order-theoretic approach to modeling generics. Given the strong relation between order theory and category theory, in this extended abstract we present how also some tools from category theory, such as adjunctions, monads and operads, are used in our approach to modeling generics.

Equations

$$E(t)\le c⟺t<:FT(c),$$

$$\mathtt{LinkedList}\le \mathtt{List}⟺\mathtt{LinkedList}<\mathtt{T}><:\mathtt{List}<?>$$

$$t<:FT\left(E\left(t\right)\right)\text{ and }c=E\left(FT\left(c\right)\right)$$

$$\mathtt{LinkedList}\le \mathtt{List}⟺\mathtt{LinkedList}<\mathtt{T}><:\mathtt{List}<?>$$

$$t<:FT\left(E\left(t\right)\right)\text{ and }c=E\left(FT\left(c\right)\right)$$

Full text

Introduction

Support for generic classes and generic interfaces (called generics) was added to Java to enhance the expressiveness of its type system [20, 21, 13, 17, 29, 23]. Generics are supported in other mainstream nominally-typed object-oriented programming (OOP) languages, such as C# [1], Scala [24], C++ [2], and Kotlin [3], for the same purpose. However, in spite of much research, the simple and accurate mathematical modeling of generics in nominally-typed OOP languages remains a challenge, mainly due to the roughness of some features of generics such as variance annotations (e.g., Java wildcards), $F$-bounded generics, and (Java) erasure [31, 30, 15, 14, 27, 28].

In a recent paper [12] we outlined a new approach, based on order theory, for modeling generics in OOP languages. In the order-theoretic approach to modeling generics we use concepts such as products of posets, intervals over posets, and pre-/post-fixed points. Details of different parts of this approach are presented in [9, 8, 10, 6, 11].

Most concepts in order theory have more general counterparts in category theory [19, 25, 26]. These include Galois connections which, in category theory, are generalized to adjunctions, and closure and kernel operators which are generalized to monads and comonads. As such, in the order-theoretic approach to modeling generics we also make use of some concepts from category theory. Further, some useful tools in category theory, such as operads, either have trivial or no clear counterparts in order theory. In this abstract we present a brief summary of how, in particular, we use adjunctions, monads (together with algebras and coalgebras), and operads in our approach to model generics in object-oriented programming.

The Java Erasure Adjunction and Free Types

All nominally-typed OOP languages, such as Java, C#, C++, Scala and Kotlin, are class-based. Class-based OOP languages that are statically-typed have two fundamental ordering relations: the subclassing (also called inheritance) relation between classes, and the subtyping relation between reference types11endnote: 1To shorten this extended abstract, some technical details are left out (and online preprints that include these details are cited), while some other details (that are not available online) and some of the lesser-significant text is moved to these endnotes. These endnotes are included here as an appendix mainly for ACT’19 reviewers to make a more in-depth assessment of the approach we present in this abstract. As such, these endnotes are not intended for inclusion in the final version of the abstract, and can be included only in a full preprint version available online (e.g., on arXiv). ,22endnote: 2In our work interfaces and traits are treated as abstract classes. The term ‘classes’ here thus refers to classes and similar (reference-)type-constructing constructs in OOP such as interfaces and traits. Also, reference types are sometimes called object types, class types, just types, or (when generics are supported) *generic types or parameterized types. . In the order-theoretic approach to modeling generics, the subtyping relation in nominally-typed OOP is constructed iteratively, solely from the subclassing relation, using novel order-theoretic *operators developed particularly for this purpose [9, 8, 10].

Maintaining a clear distinction between the subclassing and subtyping relations also enables recognizing and defining an adjunction between the two relations, when the two ordered sets corresponding to the two relations are viewed as categories rather than posets. We call this adjunction the Java Erasure Adjunction (JEA).33endnote: 3Although JEA involves category-theoretic concepts such as adjoints and free types, but the basis of the adjunction is order-theoretic. Also, while erasure is discussed frequently in relation to Java (to support migration-compatibility), but erasure is not specific to Java and, as a mapping between classes and types, it is applicable to any generic OOP language. As such, the JEA may also be called the Erasure Galois Connection (EGC). The left adjoint of JEA is* *Java erasure, which “erases” type arguments of a parameterized type [21], and as such maps a parameterized type to a class. The right adjoint of the JEA adjunction is the newly-named notion of a free type corresponding to a class, which maps any class to the type expressing the “most general wildcard instantiation” of the class (e.g., in Java, a generic class C with one type parameter has the parameterized type C<?> as its corresponding free type).

As for any adjunction, to properly define an adjunction the two maps of JEA have to work in tandem to satisfy a preservation condition. In particular, if $E$ is the erasure functor and $FT$ is the free type functor, and if $\leq$ denotes the subclassing relation and $<:$ denotes the subtyping relation, then for $E$ and $FT$ to define an adjunction we must have

[TABLE]

for all types $t$ and classes $c$.

In words, this condition says that the erasure $E(t)$ of a parameterized type $t$ is a subclass of class $c$ if and only if $t$ is a subtype of the free type $FT(c)$ corresponding to class $c$. This is a true statement in generics,44endnote: 4Consider, for example, the statement (in Java)

$\mathtt{LinkedList\leq List\Longleftrightarrow LinkedList\negthickspace<\negthickspace T\negthickspace>\;<:\;List\negthickspace<?\negthickspace>}$

where, in Equation (1)1, type variable $t$ is instantiated to the generic type LinkedList<T> for all type arguments $\mathtt{T}$ (e.g., String or Integer or ? extends Number) and class variable $c$ is instantiated to class List. This statement asserts that class LinkedList in Java is a subclass of List if and only if all instantiations of LinkedList are subtypes of the free type List<?>—which is a true statement in Java. ,55endnote: 5*Digressive Note*:* *The preservation condition expressed by Equation ([1](#S0.E1))[1](#S0.E1) is equivalent to the statement stating that, for any two classes C and D, if D is a subclass of (*i.e.*, inherits from) C then all parameterized types that are instantiations of D, and their subtypes, are subtypes of the free type C<?> corresponding to class C and vice versa, i.e., if all instantiations of some class D and their subtypes are subtypes of the free type C<?> corresponding to some class C, then D *is *a subclass of C. As stated here, this statement is familiar to OO developers using nominally-typed OO programming languages such as Java, C#, C++, Scala and Kotlin. It is a true statement in these languages due to the nominality of subtyping in these languages. Subclassing (a.k.a., inheritance), a relation characteristic of class-based OOP, is always specified between classes in OO programs using class names. Nominal subtyping asserts a bidirectional correspondence between the subtyping relation and the inherently nominal subclassing relation. In the case of non-generic OOP, the correspondence between subtyping and subclassing is expressed, succinctly, by stating that ‘inheritance is subtyping’.. In the case of generic OOP, the correspondence is succinctly expressed by stating that ‘inheritance is the source of subtyping’. The latter is a compact expression of Equation (1). Focusing on generic nominally-typed OOP, the ‘inheritance is the source of subtyping’ statement and Equation (1) state, first (in the left-to-right direction), that subclassing does result in (i.e., is a source of) subtyping between reference types, and, secondly (in the right-to-left direction), that subclassing is the *only *source of subtyping between reference types (i.e., that besides subclassing there are no other sources for subtyping). making erasure and free types in OO programming languages two adjoints of an adjunction—the JEA adjunction.66endnote: 6It should be noted that in Java and other similar OO languages a parameterized type is always a subtype of the free type corresponding to the class resulting from the erasure of the parameterized type, and a class is always the same as that resulting from the erasure of the free type corresponding to the class. In symbols, in OO generics we have

$t<:FT\left(E\left(t\right)\right)\textrm{ and }c=E\left(FT\left(c\right)\right)$

for all types $t$ and classes $c$. For example, in Java we have List<String> <: List<?> and, more generally, we have List<T> <: List<?> = $FT$(List) = $FT$($E$(List<T>)) for all types T. Also, for all classes C we have C as the erasure of the corresponding free type C<?>, *e.g.*, we have LinkedList = $E$(LinkedList<?>) = $E$($FT$(LinkedList)) and List = $E$(List<?>) = $E$($FT$(List)). Following order-theoretic parlance [18, Ch. 7], a reference type is called a closed type if it does not get changed (i.e., is fixed) by erasure followed by free type construction. Similarly, a class is called a closed class if it is not affected by free type construction followed by erasure. As such, relative to JEA, in the OO subtyping relation only the free types are closed types, while in the subclassing relation all classes are closed classes. In order theory parlance, the compositions $FT\circ E$ (from the subtyping relation to itself) and $E\circ FT$ (from the subclassing relation to itself) of the adjoints of JEA are called closure operators, and closed elements are fixed points of these closure operators [18, Ch. 7]. These observations regarding JEA and closure operators hint at the well-known correspondence between adjunctions and monads in category theory. (See the discussion in the main text for another use of monads in modeling generics.)

It should be noted that the notion of a free type in OOP is similar to the notion of a ‘free monoid’ corresponding to a set and of a ‘free category’ (a ‘quiver’) corresponding to a graph. More details on JEA and on free types are available in [4] and [11].

Monads, Inductive/Coinductive Types, and Co-free Types

Monads and comonads in category theory generalize closure and kernel operators in order theory [19, 25]. As such, the discussion of (co)inductive types in the order-theoretic approach to modeling Java generics [7, 11]—a discussion that can be expressed using closure and kernel operators [18]—can also be generalized to involve categories (as “generalized posets”), using monads and comonads. Generalizing the discussion of induction/coinduction to categories has the immediate benefit of enabling a discussion of inductive and coinductive types while not requiring the subtyping relation to be a complete lattice, nor requiring the existence of exact fixed points in the relation. (We further discuss this point in [7, 11].)

Using order-theory, inductive types and coinductive types in OOP (which are relevant to $F$-bounded generics77endnote: 7An example of $F$-bounded generics is class Enum in Java. The declaration of class Enum looks as follows:    class Enum<T extends Enum<T>> {...}. Class Enum is an instance of an $F$-bounded generic class because its type parameter T is upper-bounded by a parameterized type that uses a type variable—namely T itself—as a type argument (Parameter T is thus not bounded by a constant type, but rather by a function/functor over types—hence the name ‘$F$-bounded’111By allowing the bound of an $F$-bounded type variable to depend on any type variable, not just on the bound type variable, we are sticking to the original definition of $F$-bounded polymorphism (which posits that ‘the bound type variable may occur within the bound’ [16]) rather than to the definition that is seemingly used in more recent literature, e.g., in [22] (which posits that a type variable is $F$-bounded if and only if the variable does occur, recursively, in its own bound).). As such, the type parameter T of class Enum ranges over all $F$-subtypes of class Enum (the second occurrence of Enum in the declaration), i.e., over all Enum-subtypes. (The $F$-subtypes of class Enum are also called the coinductive or post-fixed types of Enum, or Enum*-coinductive* or Enum*-postfixed* types). In summary, valid type arguments to class Enum are only Enum-subtypes (i.e., of all the admittable parameterized types constructed using class Enum the valid ones are only those instantiations of Enum with Enum-subtypes. For a discussion of admittable type arguments versus valid ones, of admittable parameterized types—such as Enum<Object>—versus valid ones, and of admittable subtyping relations versus valid ones, see [6].) ) are modeled using pre-fixed points and post-fixed points. When using monads from category theory, the discussion of inductive and coinductive types can be expressed, rather, using the category-theoretic notions of $F$-algebras and $F$-coalgebras. In particular, if $F$ is a generic class, then all the parameterized types Ty such that Ty is a subtype of F<Ty> are called the $F$-subtypes of class $F$, while, dually, all the parameterized types Ty such that F<Ty> is a subtype of Ty are called the $F$-supertypes of $F$. Using monads enables easily seeing that $F$-subtypes of a generic class $F$ in an OO program directly correspond to coalgebras of $F$, while its $F$-supertypes correspond to algebras of $F$.

Using monads further allows easily seeing that free types, as the greatest $F$-subtypes, are final coalgebras in the Java subtyping category, and that, on the other hand, initial algebras rarely exist in the Java subtyping relation since, unlike for free types, Java does not define a general notion of types that correspond to least $F$-supertypes. The discussion of final coalgebras and initial algebras motivates us to suggest adding to Java and similar OOP languages the notion of co-free types as the least $F$-supertypes (i.e., as initial algebras) in the OO subtyping relation. Co-free types, as indicated by their name, function as duals of free types. We envision the main use of co-free types to be as lower bounds of type variables and of interval type arguments.88endnote: 8In particular, for each generic class C, we suggest the notation C<!> for the corresponding co-free type. In Java the cofree type C<!> has as instances only the trivial object null. The cofree type C<!> has as supertypes all parameterized types that are instantiations of class C (and their supertypes), and has as subtypes only the cofree types corresponding to all subclasses of C. We predict the main use of cofree types to be as lower bounds of type variables (in doubly $F$-bounded generics [6]) and of interval type arguments (in interval types [10]). Currently in Java, rather confusingly, when a free type such as C<?> is used as the lower bound of a wildcard type argument* *(*e.g.*, as in ? super C<?>) the free type has a meaning—one similar to that of co-free types—that is intuitively *different *than the meaning of the free type when it is used as the upper bound of a wildcard type argument (e.g., as in ? extends C<?>)—which hints at the need for co-free types. More details on the uses of lower bounds in OO generics can be found in [10, 6].

JSO: An Operad for Constructing the Generic Subtyping Relation

Operads are a tool in category theory that can be used to model self-similar phenomena [26]. As such, operads can be used to construct the subtyping relation in generic OOP. Noting the self-similarity of the Java subtyping relation allowed us, in our order-theoretic approach to modeling generics, to express the construction process of the subtyping relation iteratively [5, 8]. In [5], in particular, we presented an outline for defining $JSO$ (the Java Subtyping Operad) as an operad that models this iterative construction process. We expect the full development of *JSO *to be a significant step in the construction of a comprehensive category-theoretic model of OO generics.

Discussion

Based on the substantial progress we made in developing an order-theoretic and category-theoretic approach to modeling generics, the concepts and tools of order theory and category theory seem to us as being perfectly suited for modeling generics in nominally-typed OOP languages.

As such we believe order theory and category theory hold the keys to overcoming the challenges met when modeling generics, and thus also to developing a simple, yet accurate model of generics in mainstream object-oriented programming languages such as Java, C#, C++, Scala and Kotlin.99endnote: 9Collaboration Plea: Given the limited human and financial resources available to him, the author would like to invite interested and qualified parties (such as individual mathematicians and PL researchers, PL and theoretical computer science research groups, software-development companies and corporations, research funding agencies, and other interested parties) to join him in speeding up the development of the order-/category-theoretic approach to modeling OO generics.