Another interesting discussion. We decided to start by going through the book chapters (6 and 7) before getting to the exercises. We got through Chapter 6 and most of Chapter 7, but didn't get to the section on coinductive types.
I think we all got a better understanding of System T, and how
works, by using a function that computes one step of the solution and applies it to the solution for the next smaller value of
The reduction rules are:
So for the base case of 0, we just return the value
For the recursive case of
, we compute the result for
and then apply
once to it. Thus the
function will ultimately get applied
We can look at this like mathematical induction, where in the inductive step we have an inductive hypothesis of
and need to prove
. Or we can look at the second argument to
as being an accumulator, containing the accumulated result of computation on the smaller problem.
We even got a pretty good intuition as to how the Ackermann function can be rewritten as as doubly-nested calls to
. Because System T is total, this shows that Ackermann's function must terminate.
We talked about adding primitive booleans, products, and sums to System T. We showed how lists can be built in this way, and how they can be folded using
Then we generalized over products and sums, unifying inductive data types into a common pattern. The combination of products and sums in a data type can be generalized into the idea of a strictly postitive functor
. This functor
is like "one step" of the datatype, so we can compute the full inductive datatype by using the fixpoint operator
. We can generalize all
functions for different data types into a function called
. And we can generalize the
function that we supplied to
to something called an
, which is just a type
and a function from
We also talked a bit about category theory, and what functors look like there, and their laws.
We talked about bit streams, and how they must be generated step-by-step. The bit stream itself is already in a normal form. Then we can apply a selector to get the first bit or the rest of the stream, and that's when the computation takes place. At any point in time, the stream really only holds a current state.
This is true for any kind of coinductive type: There's a state, and further states can be produced by selectors. In a coinductive binary tree, there's a single state, and selecting the left branch advances the state in one way, but selecting the right branch advances the state in a different way. We also represent the state with a type
, and that's no coincidence. The state when building a coinductive type is very much like the accumulator when folding an inductive type, but the process is happening in reverse.
We didn't have time to go over the exercises, but Ed pointed out that Exercises 2 and 3 are already solved in the text. Nobody understands what Exercise 4 is asking for. I'll keep thinking about it.
We'll talk about how to generalize coinductive types next time, and go over the exercises. Happy Holidays!