We present type inference algorithm $V$, which can be applied to incremental type inference systems for functional languages. Our research is motivated from our work on incremental type inference system for smart editor, which can notify type errors while you are editing a program.
An algorithm for incremental type inference system should fulfill some requirements. First, it should be agile in response to the continual changes of the program. Second, it must not be panic on free variable and stop analyzing, because unbound variables are frequent in your incomplete program. Although $W^*$ which is given by Bernstein and Stark naturally satisfies the requirements for incremental type inference system, it may induce exponentially many assumptions, which are type contexts for free variables. Moreover, $W^*$ cannot give concise self-contained type information for declarations.
In this thesis, we present algorithm $V$ which does not have the defects of $W^*$ by utilizing type scheme while it still satisfies the requirements for incremental type inference systems. The assumptions given by $V$ are at most linear to the given expression. And $V$ can supply concise type information about declarations in the form of type scheme, which can be utilized as interface information for the declarations. We also proved soundness of $V$ which guarantees that if $V$ is successful for a closed expression, evaluating the expression does not go wrong.
본 논문에서는 이전의 합성적인 상향성 타입유추 알고리즘 $W^*$를 보완한 알고리즘 $V$를 제시하였다. $W^*$ 알고리즘은 합성적인 상향성 알고리즘으로서, 자유변수가 있는 표현식에도 적용가능한 특징을 가지고 있다. 그러나 이 알고리즘은 출력물이 클 뿐만 아니라 사용자에게 유용한 정보를 주는데에 문제점을 가지고 있다. 이 문제는 $W^*$가 단순 타입만을 이용하여 조건식을 생성하기 때문에 발생한다.
제안한 해결책은 타입스킴을 이용한 일반화이며, 이를 실현한 구체적인 알고리즘 $V$를 제시하였다. $V$는 $W^*$에서 두 가지를 개선하였다. 첫째, 양적인 측면에서 $W^*$가 최악의 경우 표현식 크기에 대해 지수함수 크기의 출력물을 주는 것에 반해, $V$는 최악의 경우 표현식 크기의 제곱에 비례하는 출력물을 준다. 둘째, 질적인 측면에서, $W^*$가 \texttt{let} 정의부의 타입에 관해 주는 정보는 다른 변수의 타입을 추가로 요구하는 형태이나, $V$가 주는 정보는 간결한 타입스킴의 형태로서 다른 변수의 타입 정보를 추가로 요구하지 않는다. 이런 간결성은 프로그래머가 프로그램을 작성할때 간결한 타입 원형을 참조하며 편하게 작성할수 있게 돕는다. 더불어, $V$알고리즘의 안전성을 증명함으로써, 닫혀진 표현식에 관해 $V$가 성공하면, 그 표현식을 계산하는 동안 문제가 발생하지 않음을 보장하였다.
반면 단점으로는, $V$는 $W^*$보다 더 많은 정보를 수집한 후 정의와 사용상태를 점검하기 때문에 $W^*$가 타입에러가 있음을 말해주는 표현식에 대해 $V$가 침묵하는 경우가 생긴다. 이 문제는 $V$의 출력을 검사하는 장치를 마련함으로써 완화할수 있다.
차후 $V$알고리즘을 이용하여 점진적 타입유추를 지원하는 개발환경을 만듦으로써 $V$의 실용성을 검증할 계획이다.
