Lambda the Ultimate

You promised yourself years ago!

That's funny, I learned continuations by reading Leroy's online course material, which motivates continuations that way.

That is because I mostly restricted myself to one shot continuations. Although I already added resume which I planned to simulate using a function.

I also have a system of rules in the plans, which would benefit from backtracking. That does not need to be exposed to the programmer.

I am a little wary of multi-shot continuations...

So, from part one of the post I understand that each mutable memory cell gets associated with a function. You define a map k from memory cells to these functions and:

lookup(k)=λs.k s s, update(t,k)=λs.k t

Then there are rules to reduce eg. update(t,update(u,k)) into update(u,k)
Since Eff is for effect, I believe that mechanism allows for mutable state?

It's not quite right to say that k is a map from memory cells to functions. In what you wrote k is the continuation. And yes, of course, eff has mutable store, which is implemented exactly with lookup and update that you wrote down (it is in prelude.eff).

I think that the lookup() example is just that, an example for the concepts of a carrier set, algebra, etc. Bauer doesn't explain why this choice captures state exactly. But he does give an informal explanation why:

In the single-cell example, our programs cannot be represented simply by return values, as they depend on the current state of the memory.

Thus, programs are functions: for each initial content of the cell, the program gives the corresponding return value. In other words, they are functions from S to T.

Note that this is no different than implementing state in a purely functional language.

In the general theory, covered by Plotkin, Power, Hyland, Pretnar and more, higher-order functions are not a central ingredient. Rather, the theory is presented using equational logic terminology. Programs are interpreted as terms denoting the effects that arise in them, modulo the equations for each particular theory.

So the program that simply looks up the contents of the memory will be denoted by the equivalence class of lookup(\s . return s). You can show that if the program deals with value of type T, then the set of all equivalence classes of terms involving lookup() and update() is isomorphic to (SxT)^S.

As a side note, one consequence of the general theory is that if we want to define state in terms lookup() and update(), satisfying Plotkin's and Power's seven equations of state (which are intuitive for any non-relaxed memory model), then we necessarily get the monad A |-> (SxA)^S. This follows from the argument in the previous paragraph, and the fact that the theory for state is Hilbert-Post complete.

But you have raised a good point. Programming in CPS is not something programmers always like to do. When we write "lookup()" we would like a single S-value, and not a complicated computation. Note that this "lookup()" is nothing else but "lookup(\s. return s)". This idea, of replacing an operation "op(t)" by "op(\s.return s)" holds in general, and gives rise to the concept of a generic operation.

I don't think that generic operations are covered in the blog (yet?), so if you want to learn more about them, try Matija's thesis.