Lambda the Ultimate

I added the link. Thanks.

I don't think I ever told you, Rys, that you were the one who really got me thinking about the pragmatics of "functional programming" by pointing out that even functional programs have state in the form of bindings. That provided a very important and persistent backdrop to some explorations that came much later for me, e.g. understanding how that insight is manifested in monads and the formulation that "state isn't the problem; unconstrained mutation is the problem." It gave me the impetus to appreciate the Alan Kay quote from "The Early History of Smalltalk" that I posted elsewhere, and to be able to see how programming approaches that I hadn't associated with minimizing the negative impact of unconstrained mutation, such as object-oriented programming, can, in fact, be seen in that same light. So, thanks!

I'll touch 3 things: 1. modesty, 2. paper reaction, 3. bindings associations.

You're welcome and thanks for pleasantries! But I did nothing hard to note functional runtimes mutate state to capture bindings not present before. I'm glad you derived insights — I just don't feel that clever about it.

I went over the paper again (as best I could with two sons talking very loudly a dozen feet away) and still found the frame strings material very engaging, but decided it might only be an algebraic representation of things I visualize spatially when I think about such mechanisms in systems. I gather the paper's motivation is inline substitutions, and analysis to guarantee safety based on equivalence in resulting evironment frames (so bindings are not altered by substition). I probably won't do any such inlining optimizations in my own work, so the analysis is less critical for me to dredge more fully.

The notation to express frame effects was fun. :-) I guess I never thought much about how I've never had notation to express what I see when I simulate changes in spatial systems mentally. (Spatial visualization is my normal thought mode taking least effort; algebra and linear text is hard to get very enthused about.)

I've been mostly interested in knowledge representation the last 30 years, so that's why I gravitated to bindings in languages and other sorts of runtimes. All my fun jobs (like my current day job) have involved creation, maintenance, and optimization of bindings for knowledge apps or servers must have. This is one aspect in which all my non-language reasoning has often looked like reasoning for programming languages. I've often wondered whether a programming language would be more suitable for some things I do.

For example most of my day job lately involves bindings in a server, and how they get created, maintained, and destroyed in a distributed network environment. Hard issues involve avoiding unconstrained mutation in a highly multi-threaded shared memory context, actually involving issues like propagation delay of bindings: when and where they have force, and for how long. The server is "compiling" all the time, and bindings decay radioactively. Optimization primarily focuses on speed in using bindings despite size and stochastic unpredictability. There's probably some sort of programming language that can express what happens, but it's like I implement effects with a naked runtime beneath such a language. Maybe someone will read this and dream up a good language for it.

If anyone's looking for a nice overview of constraining state mutation, implicit state, etc. CTM has a nice treatment of it in chapter 6.