The principle type-scheme of an object in combinatory logic
Roger Hindley · Transactions of the American Mathematical Society · 1969
Introduction.In their book Combinatory Logic [1], Curry and Feys introduced the notion of "functional character" (here called "type-scheme") of an object of combinatory logic.Roughly speaking, each object of combinatory logic ("ob" for short) represents a function or an operator on functions ; for instance the ob I represents the identity operator, and we have for all obs X, IX = X.One of the aims of combinatory logic is to study the most basic properties of functions and other concepts, with as few restrictions as possible; hence in the simplest form of combinatory logic there is nothing to stop a function being applied to itself; thus XX is an ob for all obs X. However it is also natural to look at the consequences of introducing type-restrictions, formulated by assigning types to the obs according to certain rules, to be described later.Each type is a linguistic expression representing a set of functions, and for any type a the statement " X has type a" is intended to mean that the ob X represents a member of the set represented by a.Given types