Church and Curry: combining intrinsic and extrinsic typing.

*(English)*Zbl 1226.03020
Benzmüller, Christoph (ed.) et al., Reasoning in simple type theory. Festschrift in honor of Peter B. Andrews on his 70th birthday. London: College Publications (ISBN 978-1-904987-70-3/pbk). Studies in Logic (London) 17. Mathematical Logic and Foundations, 303-338 (2008).

From the introduction: Church’s formulation of the simple theory of types [A. Church, J. Symb. Log. 5, 56–68 (1940; Zbl 0023.28901; JFM 66.1192.06)] 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 [H. B. Curry, Proc. Natl. Acad. Sci. USA 20, 584–590 (1934; Zbl 0010.24201; JFM 60.0850.01)], later adapted to the \(\lambda\)-calculus [W. A. Howard, in: J. P. Seldin (ed.) et al., To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism. London: Academic Press. 479–490 (1980; Zbl 0469.03006)], 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 [M. Coppo, M. Dezani-Ciancaglini and B. Venneri, Z. Math. Logik Grundlagen Math. 27, 45–58 (1981; Zbl 0479.03006)], 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 \(\lambda\)-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.

The resulting system combines the strengths of the two approaches. We can restrict attention to well-formed terms, and we exploit this when defining substitution and related operations. Moreover, we can easily define finitary sort polymorphism, and the system is quite precise in the properties it can assign to terms without losing decidability of sort checking.

For the entire collection see [Zbl 1196.03002].

Curry’s formulation of combinatory logic [H. B. Curry, Proc. Natl. Acad. Sci. USA 20, 584–590 (1934; Zbl 0010.24201; JFM 60.0850.01)], later adapted to the \(\lambda\)-calculus [W. A. Howard, in: J. P. Seldin (ed.) et al., To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism. London: Academic Press. 479–490 (1980; Zbl 0469.03006)], 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 [M. Coppo, M. Dezani-Ciancaglini and B. Venneri, Z. Math. Logik Grundlagen Math. 27, 45–58 (1981; Zbl 0479.03006)], 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 \(\lambda\)-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.

The resulting system combines the strengths of the two approaches. We can restrict attention to well-formed terms, and we exploit this when defining substitution and related operations. Moreover, we can easily define finitary sort polymorphism, and the system is quite precise in the properties it can assign to terms without losing decidability of sort checking.

For the entire collection see [Zbl 1196.03002].

##### MSC:

03B15 | Higher-order logic; type theory (MSC2010) |

03B40 | Combinatory logic and lambda calculus |