POPL?

POPL 2011 convenes in Austin next January: we must get a Fortress paper in. The PLRG team has been itching to get something into POPL, and apparently there is outside interest in such work. Eric is convinced that our work on generic overloading — primarily from last summer — is novel enough for a submission, which means we’re in crunch mode for a few months to hammer out the implementation in Fortress and then a generalized theory on paper.

The primary novelty of the work lies in its emphasis on completely generalized overloading. Whereas most OO languages rely on an ad hoc mechanism for determining valid overloadings our system specifies the most permissive overloading possible while increasing the capacity for error checking. Our system is sorta like a functor; give it some information about your system and out come algorithms for checking overloadings. More specifically, given the following components of an OO language:

  • a lattice of types along with the subtype partial order,
  • a relation that specifies the only allowed subtypes of a type (the `comprises` clause), and
  • a relation declaring disjoint types (the `excludes` clause),

our system provides (I think)

  • an algorithm for inference of type arguments to function calls (e.g. `head [\ Int \] (some_int_list)`),
  • a partial order between overloaded signatures representing the “more specific” relation, and
  • an algorithm for checking overloading well-formedness (i.e. the overloading rules).

The type inference algorithm is essentially that of Dan Smith, as presented in his 2008 OOPSLA paper “Java 5 Type Inference is Broken.” The “more specific” relation comes from our work last summer, and the algorithm for checking well-formedness comes from Justin’s undergraduate thesis.