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 tchnical challenges that arise from structural asymmetries inherent in object-oriented languages (e.g., classes typically declare ancestors explicitly but not descendants).
많은 객체 지향 언어에서 메서드 오버로딩(method overloading), 즉 같은 이름을 가진 다수의 메서드를 선언하는 것을 허용한다. 같은 이름의 여러 메서드 선언 중 호출할 메서드를 선택하기 위해서 다중 디스패치(multiple dispatch)는 모든 인자의 런타임 타입을 고려한다. 이러한 다중 디스패치는 수학적 연산과 같은 이항 연산자를 직관적이고 일관성 있게 정의할 수 있도록 하지만 다중 디스패치를 가지는 언어에서 모든 메서드 호출이 모호성 없이 안전하게 실행되도록 보장하는 것이 어렵다. 특히, 언어가 다중 상속(multiple inheritance)과 다형성(parametric polymorphism) 등을 지원할 때 더욱 복잡해진다. 이 학위 논문에서는 대칭(symmetric) 다중 디스패치, 다중 상속, 다형성, 그리고 가변성(variance)을 가지는 객체 지향 언어를 정의하였다. 또한, 이 언어의 정적 의미(타입 검사)와 동적 의미(디스패치 방법)를 정의하고, 언어의 타입 안전성을 증명함으로써 새로 제안한 동적 디스패치 방법이 정적 의미와 잘 어우러지며 동작함을 보였다.
