일반화된 Let - 다형성 타입 유추 알고리즘 = A Generalized Let - Polymorphic Type Inference Algorithm

국문 초록 (Abstract)

본 연구에서는 일반화된 let-다형성(let-polymorphic) 타입 유추 알고리즘을 제시하고, 이로부터 얻어지는 모든 예 알고리즘들은 Hindley/Milner 타입 체계를 안전하고 완전하게 (sound and complete) 구현하고 있음을 증명하여, 일반화된 알고리즘의 두 예 알고리즘들간에 어느 한쪽이 항상 오류를 더 신속히 감지하게 되는 조건을 제시한다.
일반화된 알고리즘으로부터 이론적으로 검증된 두 타입 유추 알고리즘, 즉, 상향성 표준 타입 유추 알고리즘 W 와 하향성 알고리즘 M 뿐만 아니라 두 알고리즘의 혼성 알고리즘(hybrid algorithm)을 만들 수 있다. 만들어진 예 알고리즘들의 안전성, 완전성, 상대적인 신속한 오류 감지 성질들은 본 논문의 증명에 의해 자동적으로 유추된다. 본 논문에서 제시하는 알고리즘으로부터 만들어 낼 수 있는 예 알고지름에는 SML/NJ와 Objective Caml 컴파일러에서 채택한 알고리즘을 포함하고 있다.

다국어 초록 (Multilingual Abstract)

We present a generalized let-polymorphic type inference algorithm, prove that any of its instances is sound and complete with respect to the Hindley/Milner let-polymorphic type system, and present a condition that one instance algorithm always detects. type errors earlier than the other.
By instantiating the generalized algorithm with different parameters, we can obtain not only the two opposite algorithms (the bottom-up standard algorithm Wand the top-down folklore algorithm M) but also other various hybrid algorithms that avoid their extremities in type-checking (W fails too late, while M fails too early). Such hybrid algorithms' soundness, completeness, and their relative earliness in detecting type-errors can be obtained automatically. The set of hybrid algorithms that come from the generalized algorithm is a superset of those used in the two most popular ML compilers, SML/NJ and OCaml.

목차 (Table of Contents)

• 요약
• Abstract
• 1. 서론
• 2. 일반화된 타입 유추 알고리즘 G
• 3. 안전성과 완전성
• 4. 덜 느슨한 알고리즘이 신속히 오류를 감지한다
• 5. 결론
• 부록
• 참고문헌
• 저자소개