Object-oriented languages have long suffered from insufficient expressiveness
due to the lack of recursive types. Though recursive types are useful to
define binary methods and some kind of factory methods, current object-oriented
languages do not support recursive types because it has been known that using
them entails mismatch between subclassing and subtyping. This mismatch means
that an object of a subclass cannot be safely used in any context where an
object of a superclass is expected, which is unacceptable for most programmers.
The most important contribution of the thesis is to show that subclassing can
match subtyping even in the presence of recursive types in a language, which
is contrary to the general perception of programming language research community.
This result is based on the new perspective on object types and subtyping
presented in the thesis, which clearly distinguishes object types and some-object
types and defines a new subtype relation on some-object types. The thesis
formally proves that the new subtype relation can successfully replace the
traditional one and that subclassing always matches subtyping even in the
presence of recursive types under the new definition of subtyping. This
effectively removes the biggest obstacle for a language to adopt recursive types
to increase its expressiveness.
The thesis also present various language features to support recursive types in
an object-oriented language, such as exact class types and This types, virtual
constructors and four kinds of typing techniques for flexible use of binary
methods. Formal properties of these language features, such as type soundness,
decidable typechecking and subtyping-by-subclassing, are proved in a distilled
nominal type system named CoreThisJava.
In addition to proving the formal results, we also implemented the language
features to test their feasibility in real situations; we extended a full-fledged
open source Java compiler JastAddJ with the language features suggested in this
thesis. As far as we have tested, the extension appears to be backward-compatible
with Java 1.4 and 1.5 as we intended, and the new language features that we added
appear to work harmoniously with existing language features of Java.
재귀 타입(recursive type)은 객체 지향 언어의 표현력을 증가시켜 준다. 특히, 이항
메소드(binary method)나 특정 종류의 팩토리 메소드(factory method)를 정의할 때
재귀 타입을 유용하게 사용할 수 있다. 그러나, 언어에 재귀 타입을 추가했을 때에는
서브클래스가 서브타입에 일치하지 않는 경우가 생긴다는 문제가 있다. 이 불일치는
서브클래스의 객체를 슈퍼클래스의 객체를 필요로 하는 곳에 쓸 수 없는 경우가 생긴다는
뜻으로서, 대다수의 프로그래머들이 받아들일 수 없는 상황을 의미한다. 그러므로, 현재
대다수의 객체 지향 언어에서는 재귀 타입을 지원하지 않고 있다.
본 논문에서는 객체 지향 언어에 재귀 타입을 추가해도 서브클래스와 서브타입의 불일치가
발생하지 않을 수 있다는 것을 밝힌다. 이는 현재까지 프로그래밍 언어 연구 분야에
널리 알려진 사실과는 다른 결과이며, 객체의 타입과 서브타이핑에 대해 본 논문에서
제시하는 새로운 관점과 정의 방식에 근거한다. 본 논문에서는 `객체 타입`과 `어떤 객체
타입`을 명확히 구분하고 서브타이핑을 `어떤 객체 타입`에 대해 정의한다. 이는 `객체
타입`에 서브타이핑을 정의하던 종전의 방식과 구별된다. 본 논문에서는 새로운 서브타이핑이
종전의 서브타이핑을 대체할 수 있음을 증명하고, 새로운 서브타이핑 정의 하에서 서브클래스는
항상 서브타입에 일치한다는 사실을 증명한다. 이는 객체 지향 언어에 재귀 타입을 추가하여
표현력을 증가시키는 데 있어 가장 큰 장애물을 제거하는 효과가 있다고 할 수 있다.
이에 더하여, 본 논문에서는 객체 지향 언어에서 재귀 타입을 사용하기 위해 필요한 몇 가지
언어 기능들을 제시한다. (1) 정확한 클래스 타입, (2) This 타입, (3)가상 컨스트럭터,
(4) 네 가지 종류의 이항 메소드 타이핑 기법들이 그것이다. 열거한 언어 기능들을 포함한
CoreThisJava라는 작은 핵심 언어를 설계하고 타입 시스템의 건실함 (타입 시스템을 통과한
프로그램은 실행 시간에 타입 에러를 일으키지 않음, type soundness), 타입 검사 알고리즘,
서브클래스와 서브타입의 일치를 증명한다.
본 논문에서 제시하는 언어 기능들에 대한 이론적인 결과뿐만 아니라, 이 기능들이 실제
언어에서 사용 가능한지를 테스트해보기 위해 오픈 소스 자바 컴파일러인 JastAddJ를
확장하여 ThisJava 컴파일러를 구현하였다. 현재까지 테스트해 본 바로는, 구현된 새로운
컴파일러가 종전의 Java 1.4와 1.5 버전에 호환성을 가지며, 추가된 언어 기능들이 종전의
언어 기능들과 함께 사용되어도 문제를 일으키지 않는다고 파악이 된다.
