Theory meeting, Oct. 9th

Lyle Kopnicky

unread,

Sep 29, 2019, 11:21:29 PM9/29/19

to pdxfunc

Hi folks,

We'll be going over Exercise Sheet 3 from the MGS 2019 course on Lambda Calculus (http://www.duplavis.com/venanzio/mgs_lambda/index.html). Please try the exercises beforehand. Everyone will be welcome to share their solutions and discuss.

Wednesday, October 9th, 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/vnpwfryznbmb/

Lyle Kopnicky

unread,

Oct 22, 2019, 2:05:01 AM10/22/19

to pdxfunc

What an interesting meeting! We went over the third set of exercises from the MGS 2019 course on Lambda Calculus.

I've attached my solutions. Ed and I came up with basically the same solutions for the streaming problems.

But we arrived at pretty different results for Problem 5, which involved implementing product types (pairing and unpairing). I thought that it wasn't possible to formulate it in terms of the existing types, but one would have to introduce new typing rules to the system. Ed came up with an ingenious solution, in terms of the simply typed lambda calculus, without any extensions. But I believe it only works when you have a single abstract base type $\mathsf{o}$ as described in the lecture. His solution involved finding a least upper bound between the two types to be paired, and deriving injections and projections to and from that type.

For example, if you have a value of type $\mathsf{o}$ , you can can construct a function from $\mathsf{o} \to \mathsf{o}$ , which is just a constant function returning the original value. Hopefully Ed will send out his notes for the complete scheme, which is quite interesting and seems sound. But, there was one flaw - doing a projection could sometimes involve creating a "dummy" value of type $\mathsf{o}$ . Because it's an abstract type, we have no way of coming up with such a value. This could be solved if type $\mathsf{o}$ were pointed, that is, if it had some distinguished value we could name. That would be the case if, instead of this abstract type $\mathsf{o}$ , we had a primitive $\mathsf{Bool}$ or $\mathsf{Nat}$ type, for example. But if we had multiple, arbitrary base types, I don't think Ed's plan would work anymore.

Exercise 7 was about converting between types $\mathsf{Nat}_\mathsf{o}$ and $\mathsf{Nat}_{\mathsf{o} \to \mathsf{o}}$ . An interesting observation was that $\mathsf{Nat}_{\mathsf{o} \to \mathsf{o}}$ is the same type as $\mathsf{Nat}_\mathsf{o} \to \mathsf{Nat}_\mathsf{o}$ ! And it seems that to map from $\mathsf{Nat}_\mathsf{o}$ to $\mathsf{Nat}_\mathsf{o} \to \mathsf{Nat}_\mathsf{o}$ , you can just use Ed's trick from Problem 5: just apply the K combinator to it, that is, $\lambda x.\ \lambda y.\ x$ . But the question is, does that give us the right number? If we start with $\overline{2}_\mathsf{o}$ and apply the K combinator to it, do we get $\overline{2}_{\mathsf{o} \to \mathsf{o}}$ ? And the answer is, no.

But then we wondered if all $\mathsf{Nat}$ values of a particular type aren't actually the same! The reason is that, since $\mathsf{o}$ has no terms, the only term from $\mathsf{o} \to \mathsf{o}$ is the identity function. Since all a $\mathsf{Nat}_\mathsf{o}$ does is apply a function from $\mathsf{o} \to \mathsf{o}$ some number of times, it must be applying the identity function. Thus all $\mathsf{Nat}_\mathsf{o}$ values, when applied to an $\mathsf{o}$ value, must just return the original value. But then, there aren't any $\mathsf{o}$ values, either.

Something clearly isn't right here. I think we're supposed to assume that there are values of type $\mathsf{o}$ , but we just don't know what they are. The author's scheme is unusual. Other presentations I see of the STLC either start with some set primitive types, like $\mathsf{Bool}$ and $\mathsf{Int}$ , or they say that there is some arbitrary set of base types. They don't just have one arbitrary base type. That seems to lead to quirky properties.

Apparently Church's original STLC had two base types: $o$ being the type of propositions, and $\iota$ the type of individuals. (See https://www.classes.cs.uchicago.edu/archive/2007/spring/32001-1/papers/church-1940.pdf.)

- 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/71a20c0e-97d9-46a7-98a0-9dfc87023865%40googlegroups.com.

exercises_3.pdf

Ed Snow

unread,

Oct 22, 2019, 6:39:01 PM10/22/19

to pdxfunc

Okay, about time I got this out: Problem 5 revisited (attached). I think I've got a serviceable workaround to the problem that Lyle found. I look forward to hearing what others think.

-- Ed

Exercises 3.5x.pdf

Lyle Kopnicky

unread,

Oct 23, 2019, 5:00:52 PM10/23/19

to pdxfunc

Thanks for sharing your ideas, Ed! Let's take a look at it tonight in the meeting.

--

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/5af68de3-b932-41de-98be-b89d663c0a83%40googlegroups.com.

Reply all

Reply to author

Forward