Church and Curry: Combining Intrinsic and Extrinsic Typing

Church’s formulation of the simple theory of types [1] has the pleasing property that every well-formed term has a unique type. The type is thus an intrinsic attribute of a term. Furthermore, we can restrict attention to well-formed terms as the only meaningful ones, because the property of being well-formed is evidently and easily decidable. Curry’s formulation of combinatory logic [3], later adapted to the λ-calculus [9], assigns types to terms extrinsically and terms may have many different types. In other words, types capture properties of terms which have meaning independent of the types we might assign. This formulation very easily supports both finitary and infinitary polymorphism. Especially the former, expressed as intersection types [2], seems to be incompatible with uniqueness of types. In this paper we show that it can be very fruitful to consider a two-layer approach. In the first layer, we have an intrinsically typed λ-calculus in the tradition of Church. A second layer of types, constructed in the tradition of Curry, captures properties of terms, but only those already well-formed according to the first layer. In order to avoid confusion, in the remainder of the paper we call types from the second layer sorts and use types only to refer to the first layer.