We discussed the type in Exercise 4 from Exercise Sheet 4:
. The idea is that
are being used as binding forms with built-in fixed points.
To understand this, first look at the inner expression
. This defines a functor
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
. The entire expression is then computing the fixed point
, an inductive data type.
binding can be understood in a similar way. It defines the functor
, which is equal to
. This is also a strictly positive functor, since there are no function arrows to the left of
. The entire expression computes the fixed point
, a coinductive data type.
The full data type then works out to an
followed by one or more
s, then another
, one or more
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.
These are both lazy folds. Note that a strict left fold cannot short-circuit at all.