I've only read the first twenty pages approximately. I'd like to see a little more disentangling of characters and strings as inputs to automata from text as something people read. The narrow technical meaning is implied in the text, but the use of "string" as a synonym for "text" is common enough that it might be worth being a little more explicit or didactic or pedantic or whatever.

The second thought is that lists smell like a type of stream. Successive calls to `next` on `rest` don't necessarily discern between lists and streams. The difference seems to be a compile time assertion that a list is a finite stream. Or in other words, a sufficiently long list is indistinguishable from an infinite stream (or generator).

I'm not sure you can have a lisp without lists, but they seem more like objects of type stream that are particularly useful when representing computer programs than a fundamental type. Whether there are really two fundamental types of sequences, depends on how platonic really really is.

All with the caveat, that I'm not smart enough to know if the halting problem makes a terminating type fundamental.