quasarbright / PongChamp

Other
1 stars 1 forks source link

Continuations / Algebraic Effects #15

Open RyanRio opened 3 years ago

RyanRio commented 3 years ago

Implement continuations in the language using the Cont monad. Look into how this could be used to support the implementation of algebraic effects. @jasonhemann @quasarbright the cool stuff 😎

RyanRio commented 3 years ago

Delimited vs undelimited continuations (a look at each one for our reference to decide what we want to implement, using racket syntax):

Undelimited:

(add1 (add1 
              (let/cc k (+ 2 (k (* 4 (k 10)))))

This evaluates to

(add1 (add1 10))

Delimited (referring to reset/shift - I don't think my example is exactly correct so would love a correction):

(reset (add1 (add1 (shift k (k (* 4 (k 10))))))

would evaluate to

(add1 (add1 (* 4 (add1 (add1 10)))))
quasarbright commented 3 years ago

We need to learn more about how algebraic effects work before we start thinking about how to implement them. We should get some practice using them, get a good understanding of the semantics, then think about implementation.

Good intro that isn't too technical or formal: https://overreacted.io/algebraic-effects-for-the-rest-of-us/

Language based on algebraic effects: https://www.eff-lang.org/

Paper on the theory: https://www.eff-lang.org/handlers-tutorial.pdf

quasarbright commented 3 years ago

Delimited vs undelimited continuations (a look at each one for our reference to decide what we want to implement, using racket syntax):

Undelimited:

(add1 (add1 
              (let/cc k (+ 2 (k (* 4 (k 10)))))

This evaluates to

(add1 (add1 10))

Delimited (referring to reset/shift - I don't think my example is exactly correct so would love a correction):

(shift k (add1 (add1 (reset k (* 4 (reset k 10))))))

would evaluate to

(add1 (add1 (* 4 (add1 (add1 10)))))

pretty sure it's (reset ... (shift k ... )) and the stuff between reset and shift gets bound to k. And I think there can be a stack of those things with reset being like push and shift being like pop

RyanRio commented 3 years ago

In addition to that, need to learn about the upsides and downsides of different types of continuations and for that matter what Haskell uses.

argument against call/cc: http://okmij.org/ftp/continuations/against-callcc.html the general page: http://okmij.org/ftp/continuations/ (lot to read here)

RyanRio commented 3 years ago

Delimited vs undelimited continuations (a look at each one for our reference to decide what we want to implement, using racket syntax): Undelimited:

(add1 (add1 
              (let/cc k (+ 2 (k (* 4 (k 10)))))

This evaluates to

(add1 (add1 10))

Delimited (referring to reset/shift - I don't think my example is exactly correct so would love a correction):

(shift k (add1 (add1 (reset k (* 4 (reset k 10))))))

would evaluate to

(add1 (add1 (* 4 (add1 (add1 10)))))

pretty sure it's (reset ... (shift k ... )) and the stuff between reset and shift gets bound to k. And I think there can be a stack of those things with reset being like push and shift being like pop

I believe you're correct, updated to reflect.

quasarbright commented 3 years ago

I'm thinking of how we could use the ContT monad transformer here. If we use ContT a Interpreter Effect (where Effect will just be Cell for now), effect handlers would be treated as callbacks. The expanded signature would be

evalExpr ::
     Expr -- normal input
  -> (Effect -> Interpreter Cell) -- effect handler
  -> Interpreter Cell -- output

problems

can't just add it to the stack

Since ContT r m a is monadic in its effect type a instead of its return type r, you can't just add it to the Interpreter monad stack. So everything needs to be a ContT a Interpreter Effect now, and that means handlers are going to have to get passed down. Maybe you could just use reader to automate handler passing and do your own small ContT logic when you need to. The instances of ContT aren't useful since you won't be using continuations in do-notation (I think?).

reader context switch

newtype ContT r m a = ContT { runContT :: (a -> m r) -> m r

m is Interpreter, which has Reader Env in it. But the tricky thing is that a handler needs to use its environment, not the environment that it's called from. We don't want dynamic scope. But both computations need to share the same global state. So for a handler, we need to bake in its environment (like local (const env)) so it ignores the Reader env that'll get passed to it when it is called in the effectful computation

Handlers get run from the effectful child computation, but use the parent's local environment, not the child computation's environment

composition and sequencing are going to be hard

Does everything need to be a ContT a Interpreter Effect now? That won't compose well. When I recur in a monadic function, I don't want to have to pass that handler around. I guess you could just shove it in a go function though. But that's what reader is for. Requires more thought

handler overriding

There needs to be a master handler that just prints the effect like an exception. Similar to how if an exception is uncaught, it'll terminate the program and get printed, an unhandled effect must also terminate the program and get printed. So when you have a handler, you'll need to set the effectful computation's handler to that one instead of the parent one. But you'll need the parent handler as a backup if the child doesn't resume:

function f() {
  try {
    print(go())
  } handle (e) {
    print("oopsie")
  }

You'll need to defer to the parent handler in that case, but you still want the print to run. Tricky

multiple effectful computations

try {
  print(go())
  print(foo())
} handle (e) {
 ...
}

you need the handler to get passed to all those computations. I guess you could just bake the handler and then run all statements in the try using that handler. not too bad actually. That's actually really good, bc then return/break/continue inside the try will propagate.

break/continue/return inside handle

Just don't allow it. Doesn't make any sense since that code gets ran inside the child computation

result vs cell

With ContT r m a, the r has to be the same everywhere. But it seems like r has to be Cell. Actually, I guess it could be result and that'll just have to be handled? You could have a function Result -> Interpreter Cell for easy unwrapping if you have to go that route. But that'll be weird with break/continue, but I guess that should be impossible anyway if wf prevents misplaced breaks/continues

Other thoughts

I don't think you could use this machinery for exceptions. An exception stops the thrower's computation and control resumes in the handler and stays with the handler. If an effect is handled, but there's no resume, it'll need to bubble out until it hits a resume. If a handler does some stuff and then doesn't resume, those effects should happen and then the effect should bubble. It'll be tricky to get these semantics right, since control eventually has to resume in whoever called the effectful computation. But if you do the handler passing right and handlers are just monadic computations that get passed around and can be executed in isolation, and calling an effectful computation just may or may not use that code, I think it'll all just work. It's just that evaluating an effectful computation might run some outer code, but it'll still give you an answer.