Whatever Comes after the Untyped Lambda Calculus

• Dec 5, 2013 · 7:00 PM
• Mixrank

Tikhon gave us the short and sweet introduction to the untyped lambda calculus. He's up for giving another talk next time. On the meetup page, go to More > Polls > What topic for our next meeting and vote on what you'd like to hear!

• Sergei W.

I made a short write-up about lambda-calculus. Still trying to understand why we cannot implement the sum and product types without introducing them by hand. My comments during the meetup (about implementing the sum and product types) turned out to be incorrect!

December 8, 2013

• Sergei W.

My remaining questions: 1. How can we establish that the product type cannot be implemented in simply typed lambda-calculus without introducing new types by hand? I'd like to see a proof by any rigorous method (Curry-Howard isomorphism, category theory, intuitionistic logic). 2. Is there some theoretical explanation for the fact that the sum type can be implemented but product type cannot?

December 8, 2013

• Sergei W.

I aksed this question on Mathoverflow and got an interesting answer. Neither the sum nor the product types are correctly implementable in simply typed lambda-calculus. This can be proved rather easily using the CH isomorphism. http://mathoverflow.n...­

December 9, 2013

• Tikhon J.

I put my slides up on http://jelv.is/talks. I'll also put up pdf versions once I figure out how to get org-mode to output to beamer :).

December 7, 2013

• Juan P.

Thanks for the lecture and discussion, everyone! I'm looking forward to the future meetings. The basic mechanics of this stuff is straight forward. But it's the implications that interest me. Nice to get an appreciation for combinators. I'm studying everything I can find at the moment...

December 6, 2013

• A former member

Finally I have started understanding this stuff! Thank you Tikhon and all other experts!

December 6, 2013

• Byron H.

Once again, I seem to have timed pout. I regret missing.

December 5, 2013

• A former member

My wife got sick so I'll be staying home to look after her. Looking forward to the next meet up.

December 5, 2013

• Sergei W.

Discovered an interesting type theory course http://pauillac.inria.fr/~remy/mpri/ that is being taught right now at Jussieu (Université Paris 7) by Didier Rémy (one of the creators of OCaml). Lecture notes are being posted and revised.

December 5, 2013

• A former member

This conflicts with the SF Clojure meetup by the way.

http://www.meetup.com/The-Bay-Area-Clojure-User-Group/events/133420002/

I would ask that this group try to avoid overlap with FP language meetup groups in future.

December 2, 2013

Darn it, you're right. We need a more complicated scheduling algorithm than just "every other Thursday".

December 2, 2013

The poll is running 5 - 3 for the simply typed lambda calculus, which seems like a logical next step from the untyped lambda calculus. Tikhon, have you got something ready for us?

December 2, 2013

• Tikhon J.

Okay, the simply typed lambda calculus sounds good.

December 2, 2013

17 went

• Jeanine A.
• A former member
• A former member
• A former member
• A former member
• A former member

San Francisco, CA

Founded Oct 29, 2013

People in this Meetup are also in:

899 minds

• Docker San Francisco

4,095 Dockers

• Bay Area Spark Meetup

7,941 Spark Enthusiasts

785 Members

• The San Francisco Java User Group

4,804 Java Developers

• Bay Area Hackathons

4,046 Hackers