15

I am not particularly knowledgeable in either lambda calculus or category theory, but I am starting to learn Haskell so I would like to ask: are there connections between category theory and lambda calculus? Could anyone describe those connections in layman's terms?

dfeuer
  • 8,889
  • 3
  • 35
  • 62
Adam
  • 3,114
  • 1
  • 28
  • 46
  • 2
    One example might be the Curry-Howard-Lambek correspondence, see e.g. [here](http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Curry.E2.80.93Howard.E2.80.93Lambek_correspondence) and [here](http://www.haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence). – dtldarek Dec 02 '13 at 07:49
  • 2
    One should be careful here which "lambda calculus" one has in mind. Simply typed lambda calculus is the natural internal language of cartesian closed categories. Unityped (aka untyped) is not. – Aleš Bizjak Dec 02 '13 at 08:10
  • 1
    [This talk](https://www.youtube.com/watch?v=dgrucfgv2Tw) would be a very good answer to the question. – Jencel May 02 '16 at 10:09

1 Answers1

13

Every model of a typed lambda calculus is a cartesian closed category.

Every cartesian closed category can be expressed as a typed lambda calculus (with the objects as types and arrows as terms).

Thus, typed lambda calculus and cartesian closed category are essentially the same concept.

Uday Reddy
  • 981
  • 7
  • 15