Of note: The definition given of propositional implication is in terms of classical Boolean logic, but, though I don't know much about Swift, it seems likely from the discussion that its inhabitable types correspond to the theorems of intuitionistic logic rather than classical logic. [E.g., it is unlikely to be possible to implement generic functions of types such as "((P -> Q) -> P) -> P" or "Not<Not<P>> -> P", despite these being Boolean tautologies (these are often thought of as in Curry-Howard correspondence with constructs like call/cc, which perhaps is an integral component of Swift, but at any rate, this nuance was never discussed in the article)].