Compositional bottom-up type inference algorithm using type scheme

Abstract

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 \texttt{let} declarations. In this thesis, we present algorithm $V$ which does not have the defects of $W^*