I don’t think the article’s characterization of ‘types a la Curry’/extrinsic types is the commonly used understanding in discussions about Type Theories. While

I don’t think the article’s characterization of ‘types a la Curry’/extrinsic types is the commonly used understanding in discussions about Type Theories. While the article claims the extrinsic types are ‘not part of the semantics of the language’, I can not agree. My experience in the area leads to extrinsic types which are described better in the following way: extrinsic types are those types which may be ascribed to a syntactic construct in a formal language. In other words, while the types are not present as annotations in the formal syntax of language terms, the fact that every term is of some type is built into the semantics of the formal type theory. One of the best descriptions and formal treatments of Curry-style types in in ‘Functors are Type Refinement Systems’ by Melliès and Zeilberger [1]. That paper is discussed in detail and the formal definitions and properties of Church vs Curry types are explored in Zeilbergers OPLSS lectures on Type Refinement. 1 - http://noamz.org/papers/funts.pdf http://noamz.org/papers/funts.pdf 2 - Zeilberger at OPLSS in 2016, 4 lectures