Delimited continuations for modeling effectful computations - Haskell

@Alexis King :wave:

Hello!

So, just to include the most recent context, the grammar of terms and evaluation contexts in a call-by-value lambda calculus:

v ::= (\x -> e) | <number>
e ::= v | e e | e + e
E ::= ● | E e | v E | E + e | v + E

What’s going on here? Let’s start with the base case: ● by itself is always a legal evaluation context. It’s a very boring one, but it’s allowed.

The evaluation context ● + 1 is also legal, as is ● + (1 + 2). We’re using the E + e production rule to make those evaluation contexts, where the E is ● and the e is 1 or 1 + 2.

The evaluation context 1 + ● is legal, too… but note that (1 + 2) + ● is not! Why?

Because the production rule for “going inside” the right argument of a + requires the left side be v, a value. And 1 + 2 is not a value, it’s an expression.

This is why this is a grammar for a call by value lambda calculus; it enforces a left-to-right evaluation order just by restricting the grammar of E.

So what we mean by just dot is that anything from the e list can go there

No, the dot is a literal dot! It’s the ● from continuation frames!

As a Haskell datatype, the definition of E would look like this:

data E = Hole | AppL E Expr | AppR Value E | PlusL E Expr | PlusR Value E

Right, but I mean in an E[e], the dot case just means we have e

Yes, that’s right—the notation E[e] means “replace the ● in E with e.”

In other words, “plug the hole.”

Let’s consider the beta reduction rule from earlier:

(\x -> e) v   --->   e[x := v]

We can make this more precise by adding an evaluation context around the outside:

E[(\x -> e) v]   --->   E[e[x := v]]

Now consider where this is/is not allowed to be used. We can reduce (\x -> x + 2) 1 + 3 to (1 + 2) + 3, because we can take the evaluation context E = ● + 3, so we have

E[(\x -> x + 2) 1]   --->   E[1 + 2]

hmm, actually I'm probably not understanding it correctly, given that E e is also an evaluation context. Shouldn't dot feature somewhere in every possible evaluation context?

sorry if I'm being slow

No, it’s fine—evaluation contexts are confusing.

Genuinely think of evaluation contexts like an algebraic datatype. Note that in the Haskell type above, every value of E has to have one and exactly one Hole somewhere inside it, since every other case contains another E.

ah, I see my mistake. for some reason I was reading E e as some kind of special construct, when it just means anything that's an evaluation context can go there

Yes, that’s right. The grammar we’re defining here is 100% syntactic.

ok, thanks. that makes sense

We have an idea of what it all “means”—v represents values, e represents expressions, and E represents evaluation frames—but the formal system is technically just a bunch of string rewriting rules.

Anyway, going back to your original example of E = throw f; ●, that wouldn’t be a legal evaluation context because monads enforce an evaluation order. You have to evaluate throw f before you can evaluated the statement after it.

what I meant in that context would be modeled in a monadic computation by throw f >> ●, but I'm not sure whether that's a valid evaluation frame either

It isn’t, for the same reasons—I was just blurring the language and metalanguage a little bit.

An evaluation context extended with do might look like this:

E ::= ... | do { x <- E; e }

Interestingly, we don’t have a rule for going inside the next statement at all. But we could define a reduction rule to do it:

E[do { x <- pure v; e }]   --->   E[e[x := v]]

So, going back to our catch example, the rules might reasonably look like

$E[\operatorname{catch} (\operatorname{pure} v) f] \longrightarrow E[\operatorname{pure} v]$

$E_1[\operatorname{catch} E_2[\operatorname{throw} e] f] \longrightarrow E_1[f e]$

and E again has a dot case for the do notation stuff

I'm having trouble imagining how to model general purpose monadic computations without reinventing something like beta reduction inside the string rewriting rules

Yes, indeed! You do have to do that if you want to model it all formally. Of course, you wouldn’t bother if you’re just using the ideas to reason informally—I wouldn’t recommend actually thinking about “evaluation contexts” and all that just to think about some monadic code. But I’m afraid I have to go for the moment—I have some plans. But I would be happy to continue this some other time. The interesting tidbit we didn’t get to is the rule for <|> in the list monad, which duplicates the evaluation context, since that corresponds to invoking the continuation multiple times.

Thanks for the explanation so far, this has really helped!

@Asad Saeeduddin In case you happen to be interested: I’ve written up an example of using reduction semantics to reason about code that uses continuations in a GitHub comment on my proposal.

@Alexis King As it is, this interface should basically stay unchanged if it gets merged? (not asking for guarantees, just curious if there are some details to sort out :slight_smile:)

Yes, I think so. I may try to figure out how to make reset# levity-polymorphic as well, but otherwise I think the interface is pretty reasonable.