Type systems and logic by Alyssa Carter (From Code Word – Hacker School)
From the post:
An important result in computer science and type theory is that a type system corresponds to a particular logic system.
How does this work? The basic idea is that of the Curry-Howard Correspondence. A type is interpreted as a proposition, and a value is interpreted as a proof of the proposition corresponding to its type. Most standard logical connectives can be derived from this idea: for example, the values of the pair type
(A, B)are pairs of values of typesAandB, meaning they’re pairs of proofs ofAandB, which means that(A, B)represents the logical conjunction “A && B”. Similarly, logical disjunction (“A | | B”) corresponds to what’s called a “tagged union” type: a value (proof) ofEither A Bis either a value (proof) ofAor a value (proof) ofB.This might be a lot to take in, so let’s take a few moments for concrete perspective.
Types like
IntandStringare propositions – you can think of simple types like these as just stating that “an Int exists” or “a String exists”.1is a proof ofInt, and"hands"is a proof ofString.(Int, String)is a simple tuple type, stating that “there exists an Int and there exists a String”.(1, "hands")is a proof of(Int, String). Finally, theEithertype is a bit more mysterious if you aren’t familiar with Haskell, but the typeEither a bcan contain values of typeatagged as the “left” side of anEitheror values of typebtagged as the “right” side of anEither. SoEither Int Stringmeans “either there exists an Int or there exists a String”, and it can be proved by eitherLeft 1orRight "hands". The tags ensure that you don’t lose any information if the two types are the same:Either Int Intcan be proved byLeft 1orRight 1, which can be distinguished from each other by their tags.…
Heavy sledding but should very much be on your reading list.
It has gems like:
truth is useless for computation and proofs are not
I would have far fewer objections to some logic/ontology discussions if they limited their claims to computation.
People are free to accept or reject any result of computation. Depends on their comparison of the result to their perception of the world.
Case in point, the five year old who could not board a plane because they shared a name with someone on the no-fly list.
One person, a dull TSA agent, could not see beyond the result of a calculation on the screen.
Everyone else could see a five year old who, while cranky, wasn’t on the no-fly list.
I first saw this in a tweet by Rahul Goma Phulore.