Home

Type-checking Modular Multiple Dispatch with Parametric Polymorphism and Multiple Inheritance

Type-checking Modular Multiple Dispatch with Parametric Polymorphism and Multiple Inheritance. Eric Allen, Justin Hilburn, Scott Kilpatrick, Sukyoung Ryu, David Chase, Victor Luchangco, and Guy L. Steele Jr. Submitted for publication, December 2010.

Multiple dynamic dispatch poses many problems for a statically typed language with nominal subtyping and multiple inheritance. In particular, there is a tension between modularity and extensibility when trying to ensure at compile time that each function call dispatches to a unique most specific definition at run time. We have previously shown how requiring that each set of overloaded definitions forms a meet semi-lattice allows one to statically ensure the absence of ambiguous calls while maintaining modularity and extensibility.

In this paper, we extend the rules for ensuring safe overloaded functions to a type system with parametric polymorphism. We show that such an extension can be reduced to the problem of determining subtyping relationships between universal and existential types. We also ensure that syntactically distinct types inhabited by the same sets of values are equivalent under subtyping. Our system has been implemented as part of the open source Fortress compiler.

So it's Sunday, and I'm researching the interaction of multiple dispatch, type-checking, and parametric polymorphism, when Google spits out this new paper by the Fortress team.

Scott Kilpatrick's Master's Thesis Ad Hoc: Overloading and Language Design puts it into perspective:

The intricate concepts of ad-hoc polymorphism and overloading permeate the field of programming languages despite their somewhat nebulous definitions. With the perspective afforded by the state of the art, object-oriented Fortress programming language, this thesis presents a contemporary account of ad-hoc polymorphism and overloading in theory and in practice. Common language constructs are reinterpreted with a new emphasis on overloading as a key facility.

Furthermore, concrete problems with overloading in Fortress, encountered during the author's experience in the development of the language, are presented with an emphasis on the ad hoc nature of their solutions.

All of this is a bit over my head, unfortunately, but I find it very interesting nevertheless. And it's heartening that the somewhat neglected multiple dispatch (and multiple inheritance!) is further developed by such a high caliber team.

By Manuel J. Simoni at 2011-03-20 16:28 | Paradigms | Type Theory | other blogs | 12228 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Once again...

Once again, LtU reads my mind. This is exactly what I needed to read as I look into adding multimethods to my optionally-typed language.

Kilpatrick's thesis is also a good bit more of an enjoyable read than the average paper I try to wade through. It's good to see the craft of lucid prose is still alive and kicking for some.

By munificent at Wed, 2011-03-23 17:46 | login or register to post comments

Embracing the ambiguity using coherence proofs

In mathematics, overloading is very common. Uses of overloading in programming languages are often similar to the one found in mathematics, in particular operator overloading.

Yet there is a feature of mathematical overloading that is never mentioned in these documents, which I find slightly disappointing: in everyday mathematics, it's not a problem if a given symbol may have two different interpretations, as long as they're compatible (equivalent) in the considered context.

Using this approach in a programming language would require a proof system: you should prove that all interpretations are observationally equal. I think that some proof language can do that (I vaguely remember a related idea wrt. coercions in Matita, a cousin of the Coq proof assistant). Of course, embedding a proof system into a programming language is a considerable achievement and I totally understand why the Fortress team didn't choose that route.

It is also possible to ignore it and take any interpretation nondeterministically, implicitly supposing that they will indeed be equivalent. This is the justification for not forbidding ambiguity statically.

By gasche at Fri, 2011-03-25 19:27 | login or register to post comments

The whole point of this kind

The whole point of this kind of overloading is that the two interpretations are not equivalent. Proving that ambiguity doesn't matter provides no value in practice.

By Jules Jacobs at Sat, 2011-03-26 11:37 | login or register to post comments

Multiple dispatch in C++

C++ is a statically typed language with nominal subtyping and multiple inheritance and an unusual form of parametric polymorphism (templates).

Yet there is a proposal to add multiple dispatch, which is likely to be included in the next standard (the one after C++0x).

See http://www2.research.att.com/~bs/multimethods.pdf
The interesting bit is that it also claims very high efficiency.

By Mathias Gaunard at Fri, 2011-05-06 18:03 | login or register to post comments

It's simpler to claim high

It's simpler to claim high efficiency when dispatch is implemented as a lookup in a flat n-dimensional array. Their example has 400 possible tuples of types, and the corresponding table takes 20 KB to represent (!). There's no telling what the performance would be when dispatching over many such multimethods and/or actually processing data (thus rarely hitting cache).

By pkhuong at Sat, 2011-05-07 00:00 | login or register to post comments

First link is now broken.

First link is now broken. Fixed link.

By naasking at Thu, 2012-03-01 16:27 | login or register to post comments