# 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,

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
toInteger False = 0
toInteger True = 1

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