Personal tools

Curry-Howard-Lambek correspondence

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
(starting a semi-project, need help! (especially for Indexed Types))
(oops)
Line 5: Line 5:
== The Answer ==
== The Answer ==
As is well established by now,
As is well established by now,
-
 
-
 
<haskell>theAnswer :: Integer
<haskell>theAnswer :: Integer
theAnswer = 42</haskell>
theAnswer = 42</haskell>
 +
The logical interpretation of the program is that the type <hask>Integer</hask> is inhibited (by the value <hask>42</hask>), so the existence of this program ''proves'' the proposition <hask>Integer</hask> (a type without any value is the "bottom" type, a proposition with no proof).
-
The logical interpretation of the program is that the type <hask>Integer</haskell> is inhibited (by the value <hask>42</hask>), so the existence of this program ''proves'' the proposition <hask>Integer</hask> (a type without any value is the "bottom" type, a proposition with no proof).
+
== Theorems for free! ==
 +
Things get interesting when polymorphism comes in. The composition operator in Haskell proves a very simple theorem.
 +
<haskell>(.) :: (a -> b) -> (b -> c) -> (a -> c)
 +
(.) f g x = f (g x)</haskell>
 +
The type is, actually, <hask>forall a b c. (a -> b) -> (b -> c) -> (a -> c)</hask>, to be a bit verbose, which says, logically speaking, for all propositions <hask>a, b</hask> and <hask>c</hask>, if from <hask>a</hask>, <hask>b</hask> can be proven, and if from <hask>b</hask>, <hask>c</hask> can be proven, then from <hask>a</hask>, <hask>c</hask> can be proven (the program says how to go about proving: just compose the given proofs!)

Revision as of 03:08, 2 November 2006

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


1 The Answer

As is well established by now, 

theAnswer :: Integer
theAnswer = 42
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).

2 Theorems for free!

Things get interesting when polymorphism comes in. The composition operator in Haskell proves a very simple theorem. 

(.) :: (a -> b) -> (b -> c) -> (a -> c)
(.) f g x = f (g x)
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!)
Retrieved from "http://www.haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence"