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

logicsystem.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 types`A`

and`B`

, meaning they’re pairs ofproofsof`A`

and`B`

, 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) of`Either A B`

is either a value (proof) of`A`

or a value (proof) of`B`

.This might be a lot to take in, so let’s take a few moments for concrete perspective.

Types like

`Int`

and`String`

are propositions – you can think of simple types like these as just stating that “an Int exists” or “a String exists”.`1`

is a proof of`Int`

, and`"hands"`

is a proof of`String`

.`(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, the`Either`

type is a bit more mysterious if you aren’t familiar with Haskell, but the type`Either a b`

can contain values of type`a`

tagged as the “left” side of an`Either`

or values of type`b`

tagged as the “right” side of an`Either`

. So`Either Int String`

means “either there exists an Int or there exists a String”, and it can be proved by either`Left 1`

or`Right "hands"`

. The tags ensure that you don’t lose any information if the two types are the same:`Either Int Int`

can be proved by`Left 1`

or`Right 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.