Proof in Functions(fewbutripe.com)
fewbutripe.com
Proof in Functions
http://www.fewbutripe.com/swift/math/2015/01/06/proof-in-functions.html
1 comments
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)].