cornell_streams_nats.md

Cornell CS3110 2019 Chapter 8.2 Streams thought process

Context

This is a document in response to a Discord question on how to go about understanding the definition of nats in the chapter listed in title.

We cannot teach intuition, but giving one a more indepth view on how someone else thinks might allow one to draw inspirations and form intuitions more efficiently than just staring at a (very) abstract object for days.

Following documents some of the ways I dissected/thought about nats, as an attempt of achieving the above goal.

Format is roughly a log of an imagined tutorial session.

Notations

We define add1 as follows for convenience

let add1 s =
  map (fun x -> x + 1) s

Replacing appropriate parts with add1, the definition of nats reads as follows

let rec nats = Cons (0, fun () -> add1 nats)

We reuse list notations as follows to represent the stream purely for clarity, but note that we will not be dealing with lists, so there should be no confusion on whether things are lists or streams.

Specifically, we pick:

• x :: xs to mean fun () -> Cons (x, xs),
• [x0; x1; x2; ...] to mean fun () -> Cons (x0, fun() -> Cons (x1, fun () -> Cons (x2, ...))) (... is not a valid OCaml syntax, we just use it as a short hand for "etc"/"and so on")
• hd to mean "pick first element of stream", and tl to mean "pick rest of the stream", similar to List.hd and List.tl

Using the notations above, we observe that map f [x0; x1; x2; ...] can be represented as [f x0; f x1; f x2; ...], or f x0 :: f x1 :: [f x2; ...], and so on.

Again, replacing the appropriate parts with above notations, the definition of nats reads as follows

let rec nats = 0 :: map add1 nats

Observing nats in action in very small (possibly more straightforward) steps

We leave map add1 nats aside for now, and just consider nats as [0; ...] for now (since nats = 0 :: ... above), then we have

nats = 0 :: map add1 [0; ...] (* 1 <- this is just a marker *)

evaluating/rewriting it, we have

nats = 0 :: add1 0 :: map add1 [...] (* 2 *)
nats = 0 :: 1 :: map add1 [...]      (* 3 *)

Cool, now we know nats = [0; 1; ...] from (3). Now we substitute it back into (1)

nats = 0 :: map add1 [0; 1; ...] (* 1 *)

evaluating/rewriting again, we have

nats = 0 :: add1 0 :: map add1 [1; ...]        (* 2 *)
nats = 0 :: add1 0 :: add1 1 :: map add1 [...] (* 3 *)
nats = 0 :: 1 :: 2 :: map add1 [...]           (* 4 *)

And now we know nats = [0; 1; 2; ...] from (4). We can substitute that back into (1), and repeat the above steps again to progressively fill in the definition of nats.

Conclusion/takeaway

In our above steps, we observe that we can resolve if we kept substituting nats into itself (kinda recursion). We also notice that the reason we can do the above steps is that we have at least one element not locked behind a closure - 0.

More specifically, we knew for certain that nats is of the pattern [0; ...] from the very beginning, otherwise we would not have a handle on things - no place to start. Indeed 0 corresponds to our base case essentially - something that allows us to kickstart the entire construction.

Observing nats in slightly more abstract steps

We note that map add1 is essentially performing a "shift right by 1" operation, e.g. map add1 [0; 1] gives [1; 2]. As such, we define shift as follows

let shift s =
  map add1 s

Now lets see how far we can get if we start from beginning, and we think in terms of shift

Play around with shift a bit:

shift [0; ...]                 = [1; ...]
shift (shift [0; ...])         = [2; ...]
shift (shift (shift [0; ...])) = [3; ...]

Noticing the pattern related to the number of shifts, we can draw a table as follows, where shiftN represents N applications of shift, with the stream elements aligned.

                     0  1  2  3  4  5  6  7  8  9  10 ...
shift0 nats          0; ...
shift1 nats             1; ...
shift2 nats                2; ...
shift3 nats                   3; ...
shift4 nats                      4; ...
shift5 nats                         5; ...
shift6 nats                            6; ...
...

Again, taking the perspective that we don't know anything about the stream beyond its first element, we don't know what ... represents in the above table.

However, curiously enough, we notice that if we just somehow "collapse" the above entries together, we actually form 0; 1; 2; 3; 4; 5; 6; ..., where "collapse" works roughly as follows

shift0 nats                  0; ...
shift1 nats                     1; ...
shift2 nats                        2; ...
collapse shift0 to 2         0; 1; 2; ...

It should be obvious from the above tables that there are a lot of overlaps, say for [0; ...] and [1; ...], we can see that [1; ...] = shift [0; ...]

So we can express collapse of [0; ...] and [1; ...] as

0 :: shift [0; ...]

In a more general form, collapse of [n; ...] and [n+1; ...] can be expressed as

n :: shift [n; ...]

Taking a closer look, the term n :: shift [n; ...] itself actually matches the pattern of [n; ...], what if we just substitute [n; ...] part of the term with the term itself?

Naming the term s, using some n, we can do so as follows

let n = (* we pick some value for n *) 100

let rec s = n :: shift s

if we just dry run the definition in our head a bit, it seems to be able to keep going indefinitely to generate 100, 101, and so on!

Since natural number starts at 0 (or 1, depending on whom you're asking), but say we pick it to start at 0, then we can just define nats very similar to how s was defined, hardcoding n to 0.

let rec nats = 0 :: shift nats

which is exactly how it was defined in the textbook.

Conclusion/takeway

Above is a fair bit of trial and error, and playing with the functions you have around to see how they "feel" like, and observing patterns of things (functional programming is also about thinking in patterns).

After looking at different directions, we then arrived at something that seems to work, though we did not prove it formally.