Category theory, or polymorphism, or something else

  • January 13, 2014 · 7:00 PM
  • Mixrank

Tikhon's been doing a great job of picking topics and explaining them. Thanks to his efforts, I finally get continuations, and I have a much firmer grasp of the Curry-Howard correspondence. Let's keep going!

Join or login to comment.

  • Jack F.

    Tikhon, did you ever post notes/slides from this talk (which I missed). I hope to catch up on my trip out of town this weekend.I plan to make it Monday night and drag along my boss.

    January 22, 2014

    • Tikhon J.

      Ah, afraid I didn't have slides this time. I'm writing up a little blog post covering the same ideas, but it might take a little while. I haven't even figured out a good way to draw category theory diagrams yet!

      January 22, 2014

  • Sergei W.

    So far it seems that only a few notions are useful from category theory:
    - if you have seen that a generic construction is useful (monad, lens, ...), try reversing all arrows and find the use case for the co-construction.
    - if you have a generic construction, try defining it as a new category and finding initial / final objects, functors, limits, etc., in that category; maybe some of these constructions will have a use case, and probably they will be as easy to implement as the initial construction anyway.

    So, in order to understand the motivation for these tricks, only very few things from category theory need to be learned. *That* kind of presentation would be really a "computer science view of category theory".

    January 15, 2014

    • Adrian K.

      Although of course it's always dangerous to say that only certain ideas are useful from a branch of mathematics. People have an annoying habit of discovering new uses for mathematical ideas.

      1 · January 15, 2014

    • Sergei W.

      Of course, more ideas might prove useful in the future. However, mathematics today has developed an immense quantity of ideas and methods that, for the most part, remain without application. In my view, any useful pedagogical presentation of category theory today must avoid the "full generality" and "here are eighteen nifty constructions" but instead concentrate on meaningful applications. Once you understand a small chunk of the theory, you can always continue learning more math as you see fit.

      January 15, 2014

  • Sergei W.

    I'd like to see a book where the basic notions of category theory are explained in direct correspondence with programming examples. For instance, adjoints or limits and other such notions sound quite abstract, and it's not clear what they are useful for, until one can see a use case for programming. Books such as "Category theory for computing science" (Barr-Wells) or "Basic category theory for computer scientists" (Pierce) are just books on mathematics, with no examples from computing. These books are not really suitable "for computer scientists", in my view.

    There is a good tutorial named "Typeclassopedia", which goes in the right direction, but it's not really a pedagogical presentation of category theory.

    January 15, 2014

    • Christopher B.

      I agree, a general book on category theory for programming doesn't really exist. A few more partial matches: Steve Awodey's Category Theory is mainly math but has some good PL examples sprinkled throughout. Roy Crole's Categories for Types covers categorical models for various kinds of types in a relatively accessible manner. Lambek and Scott's Intro to Higher-Order Categorical Logic covers correspondences with typed lambda calculi on a theopretical level.

      January 15, 2014

    • Christopher B.

      Another older one that covers implementation of some category theory in ML is Rydeheard and Burstall Computational category theory.

      January 15, 2014

  • Christopher B.

    Hats off to Tikhon for being brave enough to try to present intro to category theory in a single session. I thought the previous sessions on lambda calculus were truly outstanding, but by comparison found this one only moderately successful. The problem is that the most interesting stuff in category theory (functors, natural transformations, monads, adjoints, internal logic of a topos, categorical semantics of types, alternative foundations of mathematics...) requires a good deal more depth and time, but spending that much time would take us far afield from the main focus of this meetup. For those interested in more, see the Bay Area Categories and Types meetup.

    January 15, 2014

  • Byron H.

    A bit of explanation of Category Theory with mapping to and from programming constructs. Among the better talks in that mapping. Excellent audience comments in that regard. At length discussions.

    January 14, 2014

  • Tikhon J.

    I gather some people wanted something to code to go along with the theory stuff. Unfortunately, most category theory used to libraries (like in Haskell) involves a whole bunch of structures that I did not talk about today. (I'll talk about some of them after covering polymorphism.) However, it might still be interesting to see some of the ideas in practice.

    For a pretty compelling representation, take a look at Haskell's lens library that we talked about. The library and its documentation is rather intimidating; I suggest starting with a wonderful talk[1] by Simon Peyton Jones introducing the key concepts. That said, the talk assumes a bit of knowledge about functors, typeclasses and polymorphism.

    Lens is a great practical example of category-theory-inspired library design. A fun exercise after watching the talk is implementing a mini lens library yourself--it's not that difficult and really helps cement the basic ideas.

    January 14, 2014

    • Tikhon J.

      Oops, forgot the link for [1]. It's http://skillsmatter.c...­

      January 14, 2014

    • Sergei W.

      I would certainly like to implement something in Prolog or another logic programming language. If it get to it, I'll let you guys know.

      January 14, 2014

  • Tikhon J.

    Also, if you want a little coding project, I would try implementing an interpreter for the simply typed lambda calculus. It's actually pretty straightforward just going by the abstract syntax and typing rules from previous slides. This is a great way to review the material we covered in past meetups--being able to implement something means you really understand it.

    Once you've got typechecking and evaluation, you can try adding type inference. It might be good to look at logic or nondeterministic programming for this.

    After that, you can throw in a parser and some syntax sugar for things like algebraic data types and numbers. This'll give you your own cute little functional language. In the future, we can extend this with polymorphism.

    It also gives you a nice testbed for experimenting with different PL ideas. You could extend your interpreter with mutable state, continuations, first-class patterns, concurrency primitives or whatever else you're interested in.

    January 14, 2014

  • Juan P.

    Thanks everyone for another great meet up! I got a couple book suggestions from Tikhon and Sergei. Note PDF available for the first one:

    > http://www.amazon.com/Category-Theory-Computing-Science-Michael/dp/0131204866
    > http://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf

    > http://www.amazon.com/Category-Computer-Scientists-Foundations-Computing/dp/0262660717

    1 · January 13, 2014

  • Dragisa K.

    Unfortunately, I won't be able to make it tonight.

    January 13, 2014

  • Christopher B.

    Last time, none of us had a ready answer for the question "So what is the Curry-Howard logical correlate for polymorphism?" I looked in Sorensen and Urzyczyn's Lectures on the Curry-Howard Isomorphism, and the answer seems to be that polymorphism corresponds to quantification over propositional variables. Sorensen and Urzyczyn define a logical system they call second-order propositional logic, which is just the propositional logic that corresponds to simply typed lambda calculus, with the addition of quantifiers that can bind propositional variables. This seems to be the simplest logic that can translate polymorphism. I would assume this means that polymorphism can be translated into any second- or higher-order constructive logic.

    December 18, 2013

People in this
Meetup are also in:

Create a Meetup Group and meet new people

Get started Learn more
Henry

I decided to start Reno Motorcycle Riders Group because I wanted to be part of a group of people who enjoyed my passion... I was excited and nervous. Our group has grown by leaps and bounds. I never thought it would be this big.

Henry, started Reno Motorcycle Riders

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy