Download PDFOpen PDF in browser

Towards an Order and Category Theoretic Model of Java Generics (extended version)

EasyChair Preprint no. 3631, version 2

Versions: 12history
18 pagesDate: June 21, 2020


The mathematical modeling of generic type systems of mainstream object-oriented programming languages such as Java, C#, C++, Scala and Kotlin is a challenge. This is mainly due to these languages supporting features such as ‘variance annotations,’ ‘F-bounded type parameters,’ and ‘type erasure.’

In this paper we present an order-theoretic and lattice-theoretic approach to modeling generics in nominally-typed OOP type systems that aims to build a simpler and more intuitive model than the extant “existentials-based” model. The approach also uses some elementary notions in category theory, as a generalization of order and lattice theory.

Our model, as constructed so far, reveals characteristics and relations underlying type systems of generic mainstream OOP languages—such as a Galois connection between subclassing and subtyping—that seem to have not been formalized and made explicit before. The model also suggests how support for generics in these languages may be simultaneously extended and simplified, including proposing features such as ‘interval types,’ ‘doubly F-bounded generics,’ ‘default type arguments,’ and ‘cofree types.’

Keyphrases: adjunctions, Bounded existential types, category theory, cofree type, Coinductive F-bounded existential types, default type, default type argument, existential type, F-algebras, F-bounded existential types, F-bounded polymorphism, F-coalgebras, fixed point, Free and cofree types, Free Type, Galois connections, generic class, generic oop, generic oop type system, generics, Interval Type, interval type argument, Java type erasure, Java Wildcards, mathematical modeling, Nominal Typing, object-oriented programming, OO Inheritance, OO Subtyping, oo type system, oop language, order theory, Ordered sets and lattices, parameterized type, partial products, post fixed point, pre fixed point, Structural-Typing, Subclassing, subtyping relation, valid type argument, Variance Annotations, wildcard type argument

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Moez Abdelgawad},
  title = {Towards an Order and Category Theoretic Model of Java Generics (extended version)},
  howpublished = {EasyChair Preprint no. 3631},

  year = {EasyChair, 2020}}
Download PDFOpen PDF in browser