K combinator ($K\equiv \lambda xy.x$)

In lambda calculus, the closed lambda term $K\equiv \lambda xy.x$ discards its second argument. In combinatory logic, its primitive constant satisfies $KAB=A$. The corresponding principal type in the simply typed lambda calculus is $\alpha \to (\beta \to \alpha )$.