[TYPES] An order-theoretic approach to OO generics

[moez at cs.rice.edu]

Dear all,




Here's my ACT 2019 poster.  It summarizes the order-theoretic (and category-theoretic) approach to modeling generics.




https://app.box.com/s/o3xv02sbic4uswh2700wlt46bbjjgnke




Regards,


-Moez







From: moez at cs.rice.edu


Sent: Thursday, June 27, 11:28


Subject: An order-theoretic approach to OO generics


To: Types List






Dear TYPEers,




The progress of OOP languages such as Java, C#, Scala, and C++ has been hindered by the complexity of their type systems.




Features of generics in OOP languages such as:




(1) variance annotations (of which Java wildcards are an instance),




(2) (Java) erasure, where type arguments of a parameterized type get dropped/ignored, and




(3) F-bounded polymorphism/generics, where a type variable occurs in its own bound, such as in the Java class declaration 


class Enum<T extends Enum<T>>{},




are particularly notable for their contribution to the complexity of OO type systems (as a check of the latest versions of language specifications - or of the Java generics FAQ - reveals, these three particular features make the specification of type systems of these languages overly unwieldy and complex). This complexity makes the full understanding of the type systems of these mainstream OO languages amenable only to the most advanced of OO software developers.




Building on the simplicity and intuitiveness of graph theory, order theory, and *basic* category theory, in recent work I've tried to build a simple model of generics in nominally-typed OOP languages (such as the ones mentioned above) using an approach that is mainly and mostly order-theoretic in its essence and nature.




I presented the details of this approach in multiple research articles that I posted to arXiv. To summarize the approach though,  recently I presented an abridged outline of the whole approach (as developed so far) in an article available at:




http://arxiv.org/abs/1906.11197




I am posting about this outline article to the TYPES mailing list because, first, I'd like to thank all those (mathematicians, PL researchers, language designers, and OO software developers) who gave me their precious feedback on the approach while its development was in its infancy.  That includes thanking in particular David Spivak, Robert Cartwright, John Greiner, Daniel Smith, Larry Paulson, Nathan Carter, and Kariem ElKoush, as well as plenty of the anonymous reviewers of conferences and workshops I submitted some of my work to.  Any shortcomings or errors found in the approach as developed so far or in its presentation should be blamed on me and no one else.




And, since the approach has matured a bit, I am now seeking further feedback on the approach from the wider community.




Next, given the limited financial and human resources available to me, I am also seeking collaborations with interested and qualified members of the community, which can help in speeding up the development of the approach and in finalizing it sooner.




Finally, if you happen to read the outline paper then please make sure that (even if you can provide me with no material support) you do not keep your opinions about the approach to yourself.  All kinds of feedback on the approach --- including constructive, well-justified and respectful criticism --- are more than welcome.




Cheers,


-Moez




PS: Pending finding funding for my trip, I plan to be in Oxford in mid July to attend ACT 2019 and to present a poster there on this work, under the title 'Modeling OO Generics: An Order- and Category-Theoretic Approach'.  Assuming I make it to Oxford, those attending ACT 2019 and interested in a chat should feel free to drop by.