You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
David Egolf (Apr 04 2020 at 17:25):I'm trying to read a paper on applied category theory, and it talks about the "Curry-Howard-Lambek correspondence". Does anyone have a resource (paper/blog article/other?) that they would recommend for understanding this correspondence? I'm an engineering student, so resources that don't assume a high level of computer science or category theory understanding would be most usable for me.
Nathanael Arkor (Apr 04 2020 at 17:41):have you taken a look at the Wikipedia article (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence)?
Nathanael Arkor (Apr 04 2020 at 17:42):I think it gives a good introduction to the concepts
David Egolf (Apr 04 2020 at 17:44):I suspect it would be helpful to me if I knew more logic. Maybe what I'm really looking for is a resource that talks about terms like "types" and "proof systems" which the wikipedia article uses freely. I guess this is a case where I need to first learn "thing A" to learn "thing B".
However, without knowing what "thing B" is all about, it can be hard to know what "thing A"'s need to be learnt first...
Nathanael Arkor (Apr 04 2020 at 17:54):perhaps it would be worth searching for an introduction to natural deduction first, in that case
Nathanael Arkor (Apr 04 2020 at 17:55):searching for that on Google brings up lots of results, although I don't know one off the top of my head that I'd recommend
Stelios Tsampas (Apr 04 2020 at 17:55):David Egolf said:
I suspect it would be helpful to me if I knew more logic. Maybe what I'm really looking for is a resource that talks about terms like "types" and "proof systems" which the wikipedia article uses freely. I guess this is a case where I need to first learn "thing A" to learn "thing B".
However, without knowing what "thing B" is all about, it can be hard to know what "thing A"'s need to be learnt first...
You could try getting your hands dirty with the correspondence in Agda. This book requires very little background. You should emphasize on intuitions, force yourself to complete exercises and the "Curry-Howard" part of the correspondence will eventually become clear... you should forget about Lambek for the time being :P.
Amar Hadzihasanovic (Apr 04 2020 at 18:00):I'm a big fan of these notes by Abramsky and Tzevelekos, Section 1.6 is about CHL. It first explains the Curry-Howard part and only then goes into categories.
David Egolf (Apr 04 2020 at 18:02):Thanks Stelios, Amar. Those look like good starting points!
Johannes Drever (Apr 04 2020 at 19:00):Philip Wadler has a nice paper called “Proposition as Types”. And there are some talks on YouTube derived from this paper.
David Egolf (Apr 04 2020 at 19:39):I'm having fun digging into these resources.
It bugs me though that they all seem to use the word "type" from the start.
Does the question "What is a type?" make sense? Or is it a primitive concept in this case that we don't define in terms of other things?
Stelios Tsampas (Apr 04 2020 at 19:56):You can say a type is a possibly empty collection of terms.
Matteo Capucci (he/him) (Apr 04 2020 at 20:09):David Egolf said:
It bugs me though that they all seem to use the word "type" from the start.
Does the question "What is a type?" make sense? Or is it a primitive concept in this case that we don't define in terms of other things?
What's a set?
David Egolf (Apr 04 2020 at 20:11):Stelios Tsampas said:
You can say a type is a possibly empty collection of terms.
Let's see if I have this right...
As far as I can tell a "term" is an expression in a formal language made up of some symbols. So, then a "type" is a collection of such symbols. For example, we could say the type of "integers" is the collection of symbols: .
Do we distinguish types that are isomorphic in some sense? For instance, the type {1,2,3} and the type {1_a, 2_a, 3_a} would seem very similar if our formal language has the same rules for dealing with the second set of symbols as it does the first set of symbols.
David Egolf (Apr 04 2020 at 20:21):Matteo Capucci said:
David Egolf said:
It bugs me though that they all seem to use the word "type" from the start.
Does the question "What is a type?" make sense? Or is it a primitive concept in this case that we don't define in terms of other things?What's a set?
I generally think of a set of a collection of elements. We could then ask what a "collection" is and what an "element" is, though, and I'm not sure I'd have a good answer. It seems that I can somehow work with these "elements" without really defining them properly. Perhaps I'm largely working from physical intuition about "things" in the physical world that's hardwired into my brain?
I suppose one way to define collections of elements is to say how they behave when we do things to them: we can combine collections of things for example to make new collections of things so that the new collection relates to the old collections in a certain way.
So, maybe we can think of types and terms in a similar way. We don't say what they are in terms of more primitive concepts (but perhaps appeal to some intuition) and then formalize their behavior by saying how types and terms interact as we perform operations on them.
David Egolf (Apr 04 2020 at 20:22):In this way of thinking, to answer my question above about isomorphic sets representing types, we wouldn't distinguish "symbol representations" of types if the two symbol representations behave in the same way under all operations of interest.
Dan Doel (Apr 04 2020 at 20:22):It is probably not ideal to say that types are collections of terms. That is overly limiting.
Matteo Capucci (he/him) (Apr 04 2020 at 20:26):David Egolf said:
So, maybe we can think of types and terms in a similar way. We don't say what they are in terms of more primitive concepts (but perhaps appeal to some intuition) and then formalize their behavior by saying how types and terms interact as we perform operations on them.
Bingo!
Matteo Capucci (he/him) (Apr 04 2020 at 20:27):Intuitively, types are quite like sets. But what exactly is a 'type' and what exactly is a 'set' is entirely up to your axiomatization.
Stelios Tsampas (Apr 04 2020 at 20:27):David Egolf said:
Let's see if I have this right...
As far as I can tell a "term" is an expression in a formal language made up of some symbols. So, then a "type" is a collection of such symbols. For example, we could say the type of "integers" is the collection of symbols: .Do we distinguish types that are isomorphic in some sense? For instance, the type {1,2,3} and the type {1_a, 2_a, 3_a} would seem very similar if our formal language has the same rules for dealing with the second set of symbols as it does the first set of symbols.
I think you're getting it. As far as isomorphism is concerned then yes, two isomorphic types are generally not the same type but you can definitely exploit their properties.
Dan Doel (Apr 04 2020 at 20:29):It might be better to say that types mean collections, and terms mean things in those collections, and if a type classifies a term in the type theory, the thing meant by the term is in the collection meant by the type.
Dan Doel (Apr 04 2020 at 20:30):And the specifics of that are up to a semantic mapping.
Dan Doel (Apr 04 2020 at 20:31):And the mapping where types mean collections of the syntactic terms is a special one.
David Egolf (Apr 05 2020 at 02:59):For the record, I also have been finding this book helpful for learning Agda.
Gershom (Apr 06 2020 at 08:52):Wadler's "propositions as types" article is considered a good introduction to curry howard https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
I find it is cleaner to learn "curry-howard" and "lambek-scott" distinctly and then glue them together. Each is a binary correspondence -- the first between proofs (logic) and types (computation), and the second between proofs (logic) and objects in cartesian closed categories (category theory). So better to only keep two different ways of thinking in your head at any given time, rather than three!
Here, btw is a (paywalled) version of one of the original Lambek papers, which is very readable: https://link.springer.com/chapter/10.1007/3-540-17184-3_44
Gershom (Apr 06 2020 at 08:55):Oh and the ur-text on the latter correspondence is as far as I know Lambek and PJ Scott's (not the Scott of Lambek-Scott correspondence, which is Dana, I believe!) "Introduction to Higher Order Categorical Logic" which the NY Category Theory Seminar had been doing a reading group on until we were rudely interrupted by a pandemic.
Robert Seely (Apr 16 2020 at 22:43):"Lambek and PJ Scott's (not the Scott of Lambek-Scott correspondence, which is Dana, I believe!)"
No (AFAIK) - "Lambek & Scott" is Jim Lambek and Phil Scott - not Dana Scott. The "Lambek-Scott correspondence" is (usually?) meant to reference the correspondence between proofs and types and objects and maps etc (It's a 3-fold correspondence between logic, type theory, and category theory). (I don't know of any Lambek-Dana_Scott correspondence, but if there is one, please comment about that!)
Gershom (Apr 17 2020 at 01:25):my understanding was it was dana, due to lambek’s “from lambda calculus to cartesian closed categories” and dana scott’s “relating theories of the lambda calculus” (https://www.semanticscholar.org/paper/Relating-theories-of-the-lambda-calculus-Scott/d77273932b8a3c443b41c914f12f98ef92b0ff9d ) both printed in “To H.B. Curry” which establish both sides of the correspondence when taken together, just as curry and howard both produced work which when taken together gives the full correspondence.
Robert Seely (Apr 17 2020 at 20:43):Ah - right! Thanks for clarifying that. To be honest, I refer to this as "Curry-Howard" (sometimes and "-Lambek", as in the title of this thread), and so mixed up how one might add "Scott" to "Lambek"! Thanks for the clarification of my confusing comment! I never think of "Lambek & Scott" in any other way than the joint authorship of their book (and articles), and never in connection with that correspondence. But that's a poor excuse! Now, having said that, the connection between proof theory and categories is really just "Lambek" - he had a series of papers on the subject, mainly in connection with Cartesian closed cats and intuitionist propositional logic, which was extended to type theory and toposes, in the Lambek-Scott book. Of course, since then there have been many many similar results for various logics and their corresponding categorical structures ...
Robert Seely (Apr 19 2020 at 04:51):Addendum: Phil Wadler's blog has a (historical) note/reminiscence by Howard on "Curry-Howard"... worth a read definitely:
https://wadler.blogspot.com/2014/08/howard-on-curry-howard.html
Henry Story (Apr 19 2020 at 05:56):I found this book from 2005 "Lectures on the Curry-Howard Isomorphism" yesterday. It looks very complete.