Thanks for the article. OCaml has long been on my short list of languages to learn, and continuations are an hobby of mine. I'll have to dig into this deeper.
If someone has experience with algebraic effects, I have a question to ask. Why are they needed at all as a type system extension and why can't they just be represented with function types? (excuse my Haskell pseudocode, I'm just a filthy C++ programmer abusing the notation I don't really know the language, also don't assume lazy semantics):
newtype Effect a = Effect (a -> Effect a)
newtype EffectHandler a = EffectHandler (() -> (a, EffectHandler a))
A function with an effect would have an explicit Effect parameter, while an effect handler would take an EffectHandler as a parameter (and return it as well). You could also add phantom types if you really need to distinguish different effects beyond 'a.
The only magic would be in the function that creates the continuation:
typed_callcc1 :: (Effect a -> Effect a) -> EffectHandler a
Of course you could generalize Effect and EffectHandler into a bidirectional typed continuation:
newtype Cont a b = Cont (a -> (b, Cont a b))
I don't pretend to fully understand algebraic effects but from what I see they are pretty much equivalent, except that there is no explicit effect parameter, just the type (so the continuation is not exactly first class and it is logically passed implicitly). For similar reasons, I think you can't hide them in a closure. What is the gain? What am I missing?
You wouldn't be able to use normal code, ie. loops, if statements, pattern matching etc. What you're trying to describe is monad'ish like promise or simply callbacks. Algebraic effects are much more general, code is normal sync like code, you can have async/await semantics without function coloring, you can customize code with dependency injection like behaviour ie. you can define logging effect in your library without specifying which logging library your user has to use as caller can customize it etc. It's not as much type system extension as new language construct – it's simply try/catch'ish yield burrito :)
See my reply to the siblings comment with the working c++ example. The call to the effect function is not a tail call: the effect function will eventually resume its caller, providing the next continuation to call. Definitely there is no colored function problem. So you will be able to yield from a for loop just fine.
As far as I understand effects are similar to delimited continuations in the way the effect handler is found via dynamic scoping, but in addition there is an extension to the type system to guarantee that at least one effect handler of the correct type handler is in place.
So I'm wondering if it wouldn't it be better, or at least equivalent , to simply pass the continuation around (i.e with lexical scope) as a first class value and attach the effect type to it, obviating the need for an ad hoc type system extension.
I'm must be missing something and there must be some use cases that can't be easily expressed this way.
I think I don’t understand your types. The Effect type you define appears to be, essentially, a function that takes infinitely many arguments of type a.
Let’s imagine two simple effects. One prints a string (I’ll call this ‘printer’) and one reads an int entered by the user (let’s call it ‘reader’) In this case, how would those effects be modelled with the types you wrote?
But it still isn’t obvious to me. If you want that IO to be asynchronous then how will you return the Effect Int (by calling the argument with the input) from input_int? I suppose the answer is that you implement a scheduler but I can’t work out how you want the details for yielding to work.
It is not like a continuation, it is exactly a (typed) continuation, or better, an infinite list of continuations (invoking the continuation yields, in addition to a possible value, the next continuation in the stream).
In your example of reading an int the EffectHandler and Effect are simply switched (better names are sink and source). And yes, for IO you will need a scheduler, but streams are much more straightforward.
I have reached my limit of pure functional language knowledge, but I can offer you a working implementation [1] in an imperative language.
I've actually implemented these typed continuations in c++ years ago, and I'm trying to understand how they differ from effects (aside for the whole imperative thing).
In the C++ implementation, for convenience the continuation object is replaced with the next continuation when invoked, but internally actually invoking a continuation function returns the yielded value and the next continuation as for my EffectHandeler example.
If someone has experience with algebraic effects, I have a question to ask. Why are they needed at all as a type system extension and why can't they just be represented with function types? (excuse my Haskell pseudocode, I'm just a filthy C++ programmer abusing the notation I don't really know the language, also don't assume lazy semantics):
A function with an effect would have an explicit Effect parameter, while an effect handler would take an EffectHandler as a parameter (and return it as well). You could also add phantom types if you really need to distinguish different effects beyond 'a.The only magic would be in the function that creates the continuation:
Of course you could generalize Effect and EffectHandler into a bidirectional typed continuation: I don't pretend to fully understand algebraic effects but from what I see they are pretty much equivalent, except that there is no explicit effect parameter, just the type (so the continuation is not exactly first class and it is logically passed implicitly). For similar reasons, I think you can't hide them in a closure. What is the gain? What am I missing?