We present a new method for type inference. Traditional approaches rely on an inductively defined domain of types. Instead, we specify the properties of the type system as a set of axioms, and give a polynomial-time algorithm for checking whether there is any domain of types for which the program types. We show the correctness of the algorithm and also prove that safety properties are satisfied; any program accepted by the type system will not cause type errors at run-time.
The advantages of our approach is that is simpler and more general. The algorithm for checking that a program types is a simple mechanism for propagating type information which should be easy to extend to support other programming language features. The type checking algorithm is more general than other approaches as the algorithm will accept any program that types under any type system that satisfies the axioms.
We also show how to make type information available to compilers and other development tools through an algorithm to determine entailment.
The language we consider is lambda calculus extended with a constructors and a form of type construct we call open case expressions. Open case expressions allow a program to manipulate abstract data types where the sets of constructors overlap.
Available as PDF (308 kB, no cover)
Download BibTeX entry.