Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 14:29 - 14:51 at Sala I - Type Inference I Chair(s): Michael Hicks

Many object-oriented languages provide method overloading, which allows multiple method declarations with the same name. For a given method invocation, in order to choose what method declaration to invoke, multiple dispatch considers the run-time types of the arguments. While multiple dispatch can support binary methods (such as mathematical operators) intuitively and consistently, it is difficult to guarantee that calls will be neither ambiguous nor undefined at run time, especially in the presence of expressive language features such as multiple inheritance and parametric polymorphism. Previous efforts have formalized languages that include such features by using overloading rules that guarantee a unique and type-sound resolution of each overloaded method call; in many cases, such rules resolve ambiguity by treating the arguments asymmetrically. Here we present the first formal specification of a strongly typed object-oriented language with symmetric multiple dispatch, multiple inheritance, and parametric polymorphism with variance. We define both a static (type-checking) semantics and a dynamic (dispatching) semantics and prove the type soundness of the language, thus demonstrating that our novel dynamic dispatch algorithm is consistent with the static semantics. Details of our dynamic dispatch algorithm address certain technical challenges that arise from structural asymmetries inherent in object-oriented languages (e.g., classes typically declare ancestors explicitly but not descendants).

Polymorphic Symmetric Multiple Dispatch with Variance (POPL19_PolymorphicSymmetricMultipleDispatchWithVariance.key)7.46MiB

Thu 17 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

13:45 - 14:51: Type Inference IResearch Papers at Sala I
Chair(s): Michael HicksUniversity of Maryland, College Park
13:45 - 14:07
Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types
Research Papers
Jana DunfieldQueen's University, Kingston, Ontario, Neel KrishnaswamiComputer Laboratory, University of Cambridge
Link to publication DOI Media Attached
14:07 - 14:29
Abstracting Extensible Data Types; Or, Rows By Any Other Name
Research Papers
J. Garrett MorrisUniversity of Kansas, USA, James McKinna
Link to publication DOI Media Attached
14:29 - 14:51
Polymorphic Symmetric Multiple Dispatch with Variance
Research Papers
Gyunghee ParkKAIST, Oracle Labs, Jaemin HongKAIST, South Korea, Guy L. Steele Jr.Oracle Labs, Sukyoung RyuKAIST, South Korea
Link to publication DOI Media Attached File Attached