 (See Hindley (1997) Table of principal types for a more extensive listing.) If we read ‘\(\rightarrow\)’ as implication and type variables as propositional variables, then we recognize three familiar tautologies in the right-hand column of the table. The language used is meager: there are only propositional variables and implication; there are no other connectives.