Type Reconstruction for General Refinement Types

Abstract. General refinement types allow types to be refined by predicates written in a general-purpose programming language, and can express function pre- and postconditions and data structure invariants. In this setting, with expressive and possibly verbose types, type reconstruction is particularly valuable, yet typeability is undecidable because it subsumes type checking. Using a generalized notion of type reconstruction, we present the first type reconstruction algorithm for a type system with base types refined by abitrary program terms. Our algorithm is a typeability-preserving transformation and defers type checking to a subsequent phase. The algorithm generates and solves a collection of implication constraints over refinement predicates, inferring maximally precise refinement predicates in a largely syntactic manner that is reminiscent of strongest postcondition calculation. Perhaps surprisingly, our notion of type reconstruction is decidable even though type checking is not....

• Type: Conference
• Year: 2007
• Where: ESOP
• Authors: Kenneth W. Knowles, Cormac Flanagan
• Keywords: ESOP 2007, Programming Languages, Type Checking, Type Reconstruction, Type Reconstruction Algorithm