Curry-Howard-Lambek correspondence

From HaskellWiki
Revision as of 03:01, 2 November 2006 by Uchchwhash (talk | contribs) (starting a semi-project, need help! (especially for Indexed Types))

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

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

The Answer

As is well established by now,


theAnswer :: Integer
theAnswer = 42

The logical interpretation of the program is that the type Integer</haskell> is inhibited (by the value <hask>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).