Theory meeting, Jan. 22nd

10 views

Skip to first unread message

Lyle Kopnicky

unread,

Jan 18, 2020, 4:07:30 PM1/18/20

to pdxfunc

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 section of Chapter 7 about coinductive types, and try Exercise 4 from Exercise Sheet 4 of the material linked from the above page.

Wednesday, January 22nd, 2020, 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/qjvbnrybccbdc/

Lyle Kopnicky

unread,

Mar 1, 2020, 8:01:02 PM3/1/20

to pdxfunc

We discussed the type in Exercise 4 from Exercise Sheet 4: $\nu X.\ A \times (\mu Y.\ B \times (Y + X))$ . The idea is that $\nu$ and $\mu$ are being used as binding forms with built-in fixed points.

To understand this, first look at the inner expression $\mu Y.\ B \times (Y + X)$ . This defines a functor $F_Y Y = B \times (Y + X)$ . Since $X$ is free, it can be seen as a fixed type. Note that it's a strictly positive functor, since there are no function arrows to the left of $Y$ . The entire expression is then computing the fixed point $\mu F_Y$ , an inductive data type.

The outer $\nu$ binding can be understood in a similar way. It defines the functor $F_X X = A \times (\mu Y.\ B \times (Y + X))$ , which is equal to $A \times \mu F_Y$ . This is also a strictly positive functor, since there are no function arrows to the left of $X$ . The entire expression computes the fixed point $\nu F_X$ , a coinductive data type.

The full data type then works out to an $A$ followed by one or more $B$ s, then another $A$ , one or more $B$ s, and so on to infinity. We weren't quite sure what this could be used for, except perhaps an infinite stream of data with periodic checksums.

One of the things that came up was whether it was possible to write a left or right fold such that it could shortcut in certain cases, not consuming the rest of the list. It turns out that it depends how you define "short-circuit".

A right fold can truly short-circuit. You can give it an infinite list, and, proceeding from the left, if it finds a value that causes it to short-circuit, it will.

A left fold must first do a pass over the entire list. Thus it cannot handle infinite lists. It then does a second pass which can short-circuit, in the sense that it will only perform its operation for values to the right of the short-circuiting value. If the calculation it performs is expensive, but traversing the list is quick, then this could be effective as a short-circuit, since it can save a lot of work.

Here's my code sample, defining foldl and foldr (in a lazy way), and comments showing the expansion of short-circuiting calls: https://gist.github.com/lylek/1e289dcba6455747797502a82408e852. I used https://gist.github.com/CMCDragonkai/81e2b81ddf0c4901ca67 and http://crypto.stanford.edu/~blynn/haskell/warts.html as references.

These are both lazy folds. Note that a strict left fold cannot short-circuit at all.

- 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/0d06b629-d694-4c0f-b034-34e7d52bb62d%40googlegroups.com.

Reply all

Reply to author

Forward

0 new messages