Contractual Types

Real software systems are open and evolving. It is a constant challenge in such environments to ensure that software components are safely composed in the face of changing dependencies and incomplete knowledge. To address this problem, we propose a new kind of type system which allows us to infer not only the type provided by a software component in an open system, but also the type it requires of its environment, subject to certain constraints. The contractual type we infer for components can then be statically checked when components are composed. To illustrate our approach, we introduce the form calculus, a calculus of explicit environments, and we present a type system that infers types for form expressions