Theory meeting, Nov. 13th

[Lyle Kopnicky]

Hi folks,

We're going through the MGS 2019 course on Lambda Calculus (http://www.duplavis.com/venanzio/mgs_lambda/index.html). For this meeting, please read the Lecture 4 slides and Chapters 6 and 7 of the draft book (linked from the above page).

Wednesday, November 13th, 2019, 6:30-8:30pm

Location:
Collective Agency

3050 SE Division, Suite 245 · Portland, OR

We'll be in the second floor conference room, not in the Collective Agency suite. It's just off the lobby area in the middle of the second floor. Elevator access is available.

RSVP at: https://www.meetup.com/Portland-Functional-Programming-Study-Group/events/vnpwfryzpbrb/

[Ed Snow]

I apologize for the last-minute notice, but I'm going to have to be a no-show at tonight's meeting. I look forward to the next one.

-- Ed

[Lyle Kopnicky]

No worries! We're just going over what we were planning on going over last time. See you next time!

[Lyle Kopnicky]

We had an interesting meeting! We got through all the lecture slides, but didn’t get into the draft book material. We figured out a lot of things, but were left with some questions, which perhaps would be answered in the book.

Some things we couldn’t quite understand just from reading the slides:

• How exactly does the lambda calculus implementation of the Ackermann-Péter function work?
• We aren’t quite clear how the concepts of “introduction” and “elimination” apply with the typing rules for recursion and corecursion.

One additional thing I pointed out was that the functions ‘in’ and ‘out’ in recursion and corecursion do nothing - they are just there to make the typing rules work out. This is an example of isorecursive typing, as opposed to equirecursive, which wouldn’t have the ‘in’ and ‘out’ keywords. But isorecursive types are easier to implement in practice. Here’s a lecture about recursive types from Cornell: https://www.cs.cornell.edu/courses/cs4110/2012fa/lectures/lecture27.pdf.

I also explained the Haskell code that I wrote for last time, to implement Ed’s pairing operation for simply typed lambda calculus.

We decided to start working on the exercises for next time, but also go over the book material to see if we can answer some of our questions. Look for an announcement about the next meeting, on Dec. 11th.

- Lyle

--
You received this message because you are subscribed to the Google Groups "pdxfunc" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pdxfunc+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/pdxfunc/3a74569e-e311-488c-80be-07aa0c91879d%40googlegroups.com.

[Lyle Kopnicky]

Oh, I also pointed out that “strictly positive” functors are also called “covariant” functors.