ELI5 the Lambek in Curry-Howard-Lambek correspondence?

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 and B, there exists an object A * B
  • For all objects A and B, there exists an object A ^ 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.

If you're learning math from Wikipedia, I'm in awe of you! I can read a Wikipedia math article about something I already know, to remind myself about a detail.

I'm afraid I know nothing whatever about category theory. @hardmath123, you've studied typed lambda calculus, right? Can you help? Otherwise I'll try asking one of the PL faculty at Berkeley.

I'm not only learning things from Wikipedia. I use other sources, many of which are easier to understand than Wikipedia, but I link to Wikipedia because it seems to be the most "canonical" source out of everything I find.

Rubber duck debugging style, I think that writing things here made me understand the Lambek part of the correspondence.

Okay, according to https://en.wikipedia.org/wiki/Curry–Howard_correspondence#Curry–Howard–Lambek_correspondence, the morphisms in the category are the identity function, the composition operator, the product constructor, a currying function, and a function application (evaluation) function, and the unit type is the terminal object.

I think I was already aware of this relationship before. Haskellers talk about a pseudo-category "Hask" (which does not satisfy the laws in the presence of _|_). The objects are the Haskell types and the morphisms are the Haskell functions. In this case, how types and terms are like the objects and morphisms is obvious.

However, I'm not completely sure if I got this right. After all, Hask has sums and an initial object (AKA identity of the sum operation), and the Cartesian closed category definition does not mention sums.

I also still think that I'm mixing up two different things by relating A ^ B in the Cartesian closed category and B -> A as in the "type" of a morphism, as the "types" of morphisms of functions are written in the latter manner for all categories (even ones that aren't Cartesian closed), so they are probably different?

I found https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory, which seems to confirm that the relationship between types and functions and objects and morphisms that I describe is the Lambek part of the correspondence. However, I also see something about an "internal language," which I don't understand. (Maybe I need real CT background knowledge for this. After all, I understand the relationship between programs and proofs because I've learned implication, conjunction, disjunction, etc.)

Forwarding from Berkeley CS Prof. Kathy Yelick:

Brian,

I studied abstract algebra in grad school, but don’t do type theory so my category theory is a bit rusty. I think the student is on the right track, with respect to currying and the existence of a bijection giving isomorphism. We need to be a bit careful about mixing notions of relations on the object in the category (congruence) with relations on the categories themselves.

I know that learning subjects form Wikipedia and web searches is a great tool, and I often use it myself. But in this case, when you’re really trying to learn a new field of mathematics and associated notation and terminology, I think you’re better off with a single consistent resource, at least to get started. I would recommend reading a more comprehensive textbook. The strongest CS programs in type theory are at CMU and in Europe.

If the student is mostly interested in the CS side of thing, they might want to look at this course by Bob Harper at CMU, which has lecture note available (and a recommended textbook, but that doesn’t seem to be online):
https://www.cs.cmu.edu/~rwh/courses/typesys/
Or this more basic category theory course by Steve Awodrey at CMU.
https://www.andrew.cmu.edu/course/80-413-713/
There are free online textbooks including:



Here is a longer list:

I hope that is helpful. It’s impressive to have someone in high school learning this on their own, so I certainly want to encourage this, but I’m not the best resource. Koushik or Sanjit may be a bit closer to this work, or George Necula definitely would be, although even there I don’t know that he was using category theory.

Kathy


Should I follow up with the other profs she recommends, or is this good enough?

Wow, thank you so much @bh and Prof. Yelick! I think that the materials in the post is more than enough for me. And now, I know that CMU is a college to apply to! :smiley:

I think I better understand Cartesian-closed categories now. A -> B, as in the "type" of a Category theoretic "morphism", isn't an object, whereas B ^ A, as in the exponential in a CCC, is. A CCC relates exponentials to morphisms through the commutative diagram on this Wikipedia page: https://en.wikipedia.org/wiki/Exponential_object. I guess I can view a CCC as the category of pairs and functions, or a category that supports first-class functions.

So, the character in your sig has black hair, but your icon has brown hair, like Yui Hirasawa. What's up with that? :wink:

Yui calls the black-haired character (Azusa) "Azunyan."

Yes, I got that part (DuckDuckGo is your friend), I'm just confused about whether you're identifying with the character in your sig, or the one in your icon.

I'm not "identifying with" any character. I like the way Yui says "Azunyan," so I wrote "Azunyan" in my signature.

Ah, I get it.

I identify with Tarvek. :slight_smile:

I found a minor error in an early proof in the book (an x that should be a y). Should I email the author of the book at the email provided at the front?

Yes, of course. After you look online for an errata page.

I don't see an errata page, and the book I read seems to be the latest version. Now, I need to figure out whether I should address the author with Mr. or Dr...

I looked around his website and didn't see any mentions of a PhD. If I call him Mr and he has a PhD, how bad is that?

Is he a professor? Then you call him "Prof."

Otherwise, nobody gets offended if you round them up to the next title. :slight_smile: He'll correct you, but won't mind.

Should I call a retired person Prof?

Oh, yes. Once a professor, you're a professor forever, retired or no. (He can, for example, still supervise PhD theses, should he want to.)