💾 Archived View for dcreager.net › papers › Jim1999.gmi captured on 2024-08-25 at 00:28:22. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2023-07-22)
-=-=-=-=-=-=-
Jim, Trevor and Palsberg, Jens. Type inference in systems of recursive types with subtyping. Manuscript, 1999.
We present general methods for performing type inference and deciding subtyping in languages with recursive types. Our type inference algorithm generalizes a common idea of previous work: type inference is reduced to a constraint satisfaction problem, whose satisfiability can be decided by a process of closure and consistency checking. We prove a general correctness theorem for this style of type inference. We define subtyping co-inductively, and we prove by co-induction that a closed and consistent constraint set has a solution. Our theorem makes it easier to find new type inference algorithms. For example, we provide definitions of closure and consistency for recursive types with a greatest type, but not a least type; we show that the definitions satisfy the conditions of our theorem; and the theorem immediately provides a type inference algorithm, thereby solving an open problem.