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.
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 meanfun () -> Cons (x, xs)
,[x0; x1; x2; ...]
to meanfun () -> 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", andtl
to mean "pick rest of the stream", similar toList.hd
andList.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
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
.
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.
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 shift
s, 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.
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.