Theory meeting, Oct. 23rd

[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, October 23rd, 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/nhsbjryznbfc/

[Lyle Kopnicky]

We didn’t end up getting to the lecture notes or chapters of the book.

Instead we discussed Ed’s solution for Exercise Set 3 Problem 5, which he attached in an email in response to the meeting for Oct. 7th. Ed has created a method of generating products in simply typed lambda calculus, as long as the types are built up of (o -> o) as a base type.

I've implemented Ed’s solution in Haskell. You can see it at https://gist.github.com/lylek/8b9620c09c0de3ad23597d8063aa5982. It turned out to be a bit tricker than I thought, and using it involves a bit of annotation. But I allow any type to be used as the base type, as long as it has a special designated “dummy” value. My function ‘inj’ is Ed’s ‘f’ function, and my ‘proj’ is his ‘g’ function. The type class Injectable indicates that, given a base type o, type a can be injected into type c. The type family Union is used to compute the smallest type into which both types a and b are injectable, given base type o.

Unfortunately the type system cannot infer that the types a and be are injectable into their Union, so I had to define ‘pair’, ‘fst’, and ’snd’ without reference to Union, only specifying the Injectable constraints. That means that technically you could use ‘pair’ to pair an o with an o and get an ‘o -> o -> o’, if you like. There’s no way to force ‘pair’ to choose the smallest product type. So instead when you create a pair, you must give in an annotation to tell it which type you want to use for the product. Conveniently, you can use the ‘Product’ type synonym to do this.

Matt also showed us a project he’s working on, involving mapping lambda calculus terms on a projective plane.

- 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/ff4d36ad-7b05-4286-9b25-ab9fd652e2ed%40googlegroups.com.