 There is no one-one correspondence between types and combinators in either style of typing: not all combinators can be assigned a type, and some implicational formulas cannot be assigned to any combinatory term. A combinator that can be assigned a type is said to be typable, and a type that can be assigned to a combinator is said to be inhabited. For instance, \(\textsf{M}\) has no (simple) type, because an implicational formula is never identical to its own antecedent. On the other hand, Peirce’s law, \(((A\rightarrow B)\rightarrow A) \rightarrow A\) is not the type of any combinator in the type assignment system TA\(_\textrm{CL}\).  Despite (or, indeed, due to) the discrepancy between implicational formulas and combinatory terms, classes of implicational formulas that can be assigned to certain sets of combinatory terms coincide with sets of theorems of some important logics.