Generally, type-based compilation approaches have advantages of an automatic mechanism of compiler debugging, an opportunity of type-based optimizations, and a framework of certified program execution.
The push-enter model is an important class of compilation methods for higher-order functions, which has been demonstrated by several functional language compilers.
The compilation methods dynamically arrange arguments passed among functions which are called with the arbitrary number of arguments according to the feature of higher-order functions. The eval-apply model is the other class of compilation methods that statically arrange function arguments.
As far as we know, there is no type system for the push-enter model. Traditional type systems never consider such a dynamic property of the model. Even though the push-enter model has its own advantages, all typed compilation approaches are obliged to use only the eval-apply model in compiling higher-order functions.
We develop new type systems for the push-enter model to specify the dynamic arrangement of arguments statically. Our major technical achievement for the type systems is to design the types of states, which all compilation methods based on the push-enter model use in runtime to indicate the status of dynamic arguments. The management of such states in the push-enter model incurs a general typing problem that the absence of arguments is treated in the polymorphic way. The difficulty of the problem is the lack of standard type languages to describe the polymorphic absence of arguments. We propose a general idea to solve it by introducing nonstandard types along with a definitional equivalence relation suitable for the description. We apply this idea to two compilation methods based on the push-enter model, MPS conversion and ZINC machine, by developing their type systems, and show that the type systems guarantee the consistent management of such states by proving the soundness of the type systems.
타입 기반 컴파일 방법론은 일반적으로 컴파일러 자체를 자동으로 디버깅할 수 있고, 타입 정보를 이용해서 프로그램을 최적화 할 수 있고, 프로그램 검증을 통해 안정성이 보장되는 실행 환경을 제공하는 장점을 지닌다. Push-enter 모델은 고차원 함수를 컴파일 하는 일반적인 방법론으로 기존의 함수형 언어 컴파일러에서 이 모델에 기초한 컴파일 방법들을 많이 사용하고 있다. 고차원 함수의 특징은 기존의 정수, 실수, 문자, 문자열 등과 같은 값처럼 함수를 자유롭게 인자로 전달하고 결과 값을 받을 수 있게 하는 것이다. 이 특징으로 인해 고차원 함수를 호출할 때 함수의 형식 인자 수가 함수에 전달되는 실제 인자의 수와 무관하다. Push-enter 모델에 기초한 컴파일 방법들의 특징은, 함수 호출자의 입장에서는 실행 시간에 주어진 실제 인자를 모두 함수에게 전달하고 함수 입장에서는 함수 자신의 형식 인자 수와 무관하게 전달받을 수 있는 실제 인자 수의 모든 가능한 경우에 대해 책임을 지도록 컴파일 하는 것이다. 즉, 실행 시간에 전달될 실제 인자 수에 관한 상태 정보를 반드시 유지해야 한다. 이와 달리 Eval-apply 모델은 함수 입장에서는 항상 정해진 형식 인자 수만큼 실제 인자가 전달된다고 가정하고 함수 호출자의 입장에서는 주어진 실제 인자 수를 조절하여 함수를 호출하는 방식이다. 항상 동일한 수의 실제 인자만 전달하므로 실제 인자 수에 관한 상태 정보를 필요로 하지 않는다.
현재까지 알려진 타입 기반 컴파일 방법론에서 고차원 함수를 컴파일 하는 방법은 모두 Eval-apply 모델에 기초한 컴파일 방법들이었다. Eval-apply 모델에 기초한 컴파일 방법들에 대한 타입 시스템은 Push-enter 모델에 기초한 컴파일 방법들에서 필요로 하는 실제 인자 수에 대한 상태 정보를 다루지 않기 때문에 타입 기반 컴파일 방법론과 Push-enter 모델 기반 컴파일 방법들을 함께 사용할 수 없는 문제가 존재한다.
본 논문에서는 Push-enter 모델에 기초한 컴파일 방법들을 타입 기반 컴파일 방법론과 함께 사용할 수 있도록 하는 타입 시스템 설계 방법을 제안한다. 제안한 방법에서 가장 중요한 점은 Push-enter 모델에 기초하는 컴파일 방법이라면 모두 가지고 있는 실제 인자 수에 대한 상태 정보의 타입이 무엇인가 하는 것이다. 기존의 타입 언어를 이용해 상태 정보의 타입을 결정하기 쉽지 않은 이유는 Push-enter 모델에서 이 상태 정보를 다루는 방법의 특성상 현재 실제 인자가 없음을 나타내는 하나의 특별한 상태 정보가 여러 유형으로 사용되기 때문이다. Push-enter 모델의 특성상 야기되는 다형성을 갖는 상태 정보를 기존의 타입 언어를 가지고 쉽게 표현할 수 없다. Push-enter 모델에 기초해 설계된 컴파일 방법들은 모두 이 문제점을 지닌다. 본 논문에서는 바로 이 다형성을 갖는 상태 정보를 표현할 수 있는 새로운 타입 어휘를 제안하고 이 어휘에 기초한 타입 시스템을 설계함으로써 Push-enter 모델에 기초한 고차원 함수 컴파일 방법과 타입 기반 컴파일 방법론을 함께 사용할 수 있게 되었다. 본 논문에서 제시한 아이디어를 Push-enter 모델에 기초한 두 가지 컴파일 방법인 MPS Conversion과 ZINC Machine에 적용해 타입 시스템을 설계해 보인다. 이 타입 시스템을 통해 Push-enter 모델에 기초한 함수간 인자 전달 방식이 상태 정보와 일관성 있게 구현되었음을 보장할 수 있다.
