Type inference for partial types is decidable

Abstract

The type inference problem for partial types, introduced by Thatte [15], is the problem of deducing types under a subtype relation with a largest element Ω and closed under the usual antimonotonic rule for function types. We show that this problem is decidable by reducing it to a satisfiability problem for type expressions over this partial order and giving an algorithm for the satisfiability problem. The satisfiability problem is harder than the one conventionally given because comparable types may have radically different shapes.