suspend, i.e. the Secret Master Plan for Fixing All The Things

[byorgey]

The big idea

What happens, theoretically and practically, when you type stuff at the REPL? The way I always think about it is that it's as if you're writing one big long block of commands chained by semicolons; it just so happens that you get to enter them one at a time. This explains why names defined at the REPL should be in scope for later things entered at the REPL. (Well, you can also enter expressions to be evaluated in addition to commands, but this can easily be explained by saying that anything without a command type gets implicitly wrapped in return.)

So what is the base doing in between REPL entries? Currently, it is idle, just like any robot that has finished running its program. But this is wrong! We should have a new CESK machine state to represent what the base is doing while waiting for another REPL input.

• Fundamentally, the base is doing something different than an idle robot. An idle robot will never do anything more unless another robot comes to salvage or reprogram it. The base will resume executing as soon as something else is entered at the REPL. If only for conceptual reasons it makes sense to distinguish between these states.

• If the base is idle, its CESK machine no longer remembers any context or store. So we have to save them into the robotContext just so we can load them back into the new CESK machine state on the next REPL input. I now realize how silly this is! Why not just have the CESK machine remember it all along?

Details

I propose adding a new CESK machine state Suspended and a new primitive constant suspend.

• The new machine state could be called Suspended, and will contain a result Value, a current Env, and a current Store. I do not think it needs to have a continuation (since I cannot think when we would ever want anything besides the empty continuation), but we could easily add a continuation if it turns out to be useful later.

• The new primitive is suspend : a -> cmd a.

  • When suspend v is executed, it has the effect of putting the machine immediately into the Suspended state, with v as the value, and the current environment and store.
  • suspend should not be available for players to use, but will only be used internally.
  • Whenever a command like x; y; z is entered at the REPL, it will be automatically rewritten to x; y; v <- z; suspend v.
    • Note that the suspend comes last, so there will in fact be an empty continuation at the point when it is executed, which is why the Suspended state does not need to store one.
    • On the other hand if we later decided we wanted to allow things like x; suspend v; y then we would need to save a continuation.

• Instead of checking to see when the base is idle, the REPL will now check to see when it becomes Suspended

• When something is entered at the REPL, the environment stored in the current Suspended machine state will be used to typecheck it, and then the Suspended state will be replaced with a state appropriate to evaluate/execute the given input (with the environment and store carried over), just as if the original suspend v call had been replaced with the new input. In other words, if you type a; b; c at the REPL and then later enter x; y; z, the net effect of the suspend is to make it as if you had literally written a; b; c; x; y; z.

• We will need to put some thought into what happens with uncaught exceptions that bubble up to the top level. The current environment and store will have to be captured somehow and put into a Suspended state with a unit value. In other words, if x; y; z is being executed and y throws an exception, it should be as if y; z is replaced by suspend ().

• This will actually be better than the status quo, which one could argue has a bug: if you execute something like def m = move end; move in Classic mode the move throws an exception (since the base does not have tank treads), and m is not added to the context. In other words the entire command fails if any part of it fails; but one could argue that the def m should succeed and add m to the context before going on to try the move.

Implications

• There will no longer be any such thing as a "global context", only local scopes managed according to the usual rules. The top-level REPL scope will just be an open-ended "local" scope where each new command is nested within the scope of previous ones.

• The only reason we needed all the VResult and FLoadEnv stuff is to collect up exported names so we can stuff them into the robotContext to save them across times when the base is idle waiting for the next REPL input. That will now just happen automatically.

  • This will automatically fix Variables in a local monadic binder escape to outer scopes #681 and Values referenced after a recursive call get overwritten #1032; we will no longer need to specially export names from binds. Just managing them according to the usual local scoping rules will work fine, and will get rid of this issue of names leaking out of their scope.
  • This will make Refactor Value into command and expression values #1047 irrelevant.
  • This will also prevent issues like Counting inventory does not work for goal criteria #858 and Fatal error when using itN resulting from a bind #977 and Fatal error with try block + bind #327.

• However, this does mean that any Env stored in a CESK machine state will now need to store not just the value of each name but also its type and requirements (because we will may need to typecheck stuff entered at the REPL later). Essentially Env will become RobotContext.

• We can also get rid of FDiscardEnv, which was only a bandaid created to prevent names leaking via the VResult machinery.

Definitions and import

Now that there is no longer any such thing as a global context, we should seriously reconsider #997. In fact we could simply get rid of def and only allow let ... in. Or we could make def x : ty = e end; c2 syntax sugar for let x : ty = e in c2. Only having let ... in would be awkward for typing definitions at the REPL since you would have to explicitly say let x = e in suspend () or something like that. But then again having both let and also def which is syntax sugar for let would be confusing. Maybe we could have ... as syntax sugar for suspend () so you could write let x = e in ... . Or we could just replace the def keyword with let, that is, let x = e end; c2 would be syntax sugar for let x = e in c2 (and let x = e end by itself would be let x = e in suspend ()).

One difficulty is how to handle imports (#495). All of this makes run even more problematic than before. A few ideas:

• If def is replaced with (or syntax sugar for) let ... in, the question arises what we should do at the end of a sequence of definitions (say, in a .sw file). One idea would be to make a sequence of defs syntax sugar for a chain of lets with a call to suspend () at the very end.
• The simplest idea would then be to replace run with a syntactic construct import <text_literal> in e, which would load the contents of the file with the given name and run it, replacing the final suspend with e. The downside of this idea is there would be a distinction between importing a file of definitions (using import ... in ...) and importing a file containing an expression.
• A much more sophisticated idea is to add record types (Records #1093) to the language, and make a module just a record, like Agda does. I used to think this was a nice idea, but after implementing records (Records #1148) I realize there are a number of impediments to having this work well:
  • To make it work well we would want some kind of open ... in ... construct to dump all the names in a record into the current scope, so we wouldn't be tied to always having qualified imports. However, checking such a construct seems problematic (see the discussion at Records #1148).
  • We would also need to have records with polymorphic fields, which seems like it could open a big can of worms with higher-rank types etc; I also thought about it a bit and I have no idea how to go about implementing it.

[kostmo]

Very exciting! Not to derail the topic, but is there any overlap with the concept of suspend and the watch/wait proposal (i.e. supporting interrupts) from #687?

[byorgey]

I don't think they are related, but I could be wrong; maybe there is some more fundamental underlying mechanism.

[xsebek]

Thanks for the detailed write-up @byorgey, I will study it on my 2-hour train journey tomorrow. 😄

On a more serious note, the simplifications sound very promising and I am hopeful this will end our CESK bugs.

Afterwards, we should add a way to inspect the CESK machine environment in UI (tweezers) and outside with Web API.

[xsebek]

Instead of getting rid of def, I would argue for an indentation-sensitive version like in Python:

def m2 =
  move;
  move;

// no end

m2;

Or a similar version of let, just to get around the odd trailing in which I would like to avoid.

---

EDIT: a fun idea is to keep def for mutually recursive definitions - we could consider all definitions in a chain at once.

[byorgey]

Just adding a note to say that we (and by we I mean "I") shouldn't let the issues with run/import and #997 derail this idea. We can still implement the stuff with suspend but leave run in for now, leave def as it is, and so on.

[byorgey]

I have started working on this. So far I have deleted a LOT of code (mostly weird special cases), and it makes me so happy. I still have some new code to write as well, but I think overall this will end up being a big net decrease in the number of lines of code.