The Curry-Howard correspondence says that types are propositions and inhabitants are proofs.
Lambek relates both logic and programming to Cartesian closed categories. I understand that a category is an algebraic structure consisting of objects with a composition operator and identity function. I looked at the definition of a Cartesian closed category:
- There exists a terminal object
- For all objects
A
andB
, there exists an objectA * B
- For all objects
A
andB
, there exists an objectA ^ B
The Wikipedia page states that Hom(A * B, C)
and Hom(A, C ^ B)
are bijective (and also isomorphic? Does the congruence symbol mean isomorphic?).
I know that the function type A -> B
is actually the exponential B ^ A
, so the fact that (a * b) -> c
and a -> b -> c
are isomorphic is the same thing as currying. Is that what the Lambek part of the correspondence is stating, or is there something more?
What is the difference between B ^ A
and A -> B
as in the "type" of a category theory morphism? Am I mixing up two different concepts?
I haven't formally learned category theory; I just pick things up from the Internet.