# Curry-Howard-Lambek correspondence

Curry-Howard Isomorphism is an isomorphism between types (in programming languages) and propositions (in logic). Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs (and vice versa).

## Contents

As is well established by now,

```theAnswer :: Integer
```

The logical interpretation of the program is that the type `Integer` is inhibited (by the value `42`), so the existence of this program proves the proposition `Integer` (a type without any value is the "bottom" type, a proposition with no proof).

## Inference

A (non-trivial) Haskell function takes maps a value (of type `a`, say) to another value (of type `b`), therefore, given a value of type `a` (a proof of `a`), it constructs a value of type `b` (so the proof its transformed into a proof of `b`)! So `b` is inhibited if `a` is, and a proof of `a -> b` is established (hence the notation, in case you were wondering).

```toInteger :: Boolean -> Integer
inZ_2 False = 0
inZ_2 True = 1
```

says, for example, if `Boolean` is inhibited, so is `Integer` (well, the point here is demonstration, not discovery).

## Connectives

Of course, atomic propositions contribute little towards knowledge, and the Haskell type system incorporates the logical connectives $\and$ and $\or$, though heavily disguised. Haskell handles $\or$ conjuction in the manner described by Intuitionistic Logic. When a program has type $a \or b$, the value returned itself indicates its type.

```(.) :: (a -> b) -> (b -> c) -> (a -> c)
The type is, actually, `forall a b c. (a -> b) -> (b -> c) -> (a -> c)`, to be a bit verbose, which says, logically speaking, for all propositions `a, b` and `c`, if from `a`, `b` can be proven, and if from `b`, `c` can be proven, then from `a`, `c` can be proven (the program says how to go about proving: just compose the given proofs!)