From Imperative to Pure-Functional and Back: Monads vs. Scoped Continuations 58 points by pron on Sept 5, 2015 | hide | past | web | favorite | 31 comments

 The interesting part of this whole thing to me is that you can get composition between your continuations without using something like Monad Transformers[1].However, the part that I haven't been able to get past yet is that monads are not closed over composition (so there exist some monads that are no longer monads when you compose them). If it turns out that monads and delimited continuations are duals then it seems that there ought to be some continuations that compose only to yield invalid results. (With the alternative being that scoped continuations always compose which suggests something odd is going on.)I haven't worked through the math yet because it looks suspiciously dreadful, but if anyone knows why scoped continuation composition is closed I would appreciate your input.[1] - the most disappointing thing about monads to me.
 Interesting, and disappointing in a way. I assumed that all Monadic compositions would be closed analogous to linear algebra operations and vector spaces. Out of curiosity, do you have a reference to read up on Monadic Composition not being closed? Particularly any lighter references (it's a Saturday after all).
 Here's a simple counter-example.The state monad is the following functor`````` St s a = s -> (a, s) `````` if we compose it with itself (using `d` as the second state parameter)`````` St s (St d a) = s -> (d -> (a, d), s) `````` is `F a = St s (St d a)` a monad? The return operation is clear enough`````` return a = \s -> (\d -> (a, d), s) `````` but the join operation fails`````` join :: F (F a) -> F a :: St s (St d (St s (St d a))) -> St s (St d a) :: s -> (d -> (s -> (d -> (a, d), s), d), s) -> s -> (d -> (a, d), s) join m0 = \s0 -> let (m1 :: St d (F a), s1) = m0 s0 in (\d0 -> let (m2 :: F a, d1) = m1 d0 (m3 :: St d a, s2) = m2 s1 (a, d2) = m3 d1 in (a, d2) , ??? ) `````` The trouble is the ??? bit where we'd like to place the furthest advanced `s` state named `s2`, but it's not in scope to return at the top since we have to apply the d state to reach it.This however only means that St does not compose with itself as a functor. It composes just fine in another method. If we install the inner monad "wrapped around" the tuple`````` StT s m a = s -> m (a, s) -- T for "transformer" `````` then the composition of states looks like`````` StT s (St d) a = s -> St d (a, s) = s -> d -> ((a, s), d) = (s, d) -> (a, (s, d)) = St (s, d) a `````` which is obviously a monad.
 It's an interesting article and something I would like to think deeply about, but I hope the author will forgive me if it isn't immediately obvious to me. Especially the statement that "monads have no place in imperative languages".For example, I do a lot of Java/Coffee script lately. I don't have access to first class continuations. Don't get me wrong; I'd love to have them. I'm sick as the next person of blowing up in a callback and having my stack completely hosed.But in Coffee script, monads are nearly trivial to implement. The use of the Maybe monad makes doing repeated transformations and filtering incredibly nicer. It is not obvious to me that a continuation based implementation would be clearer at all.Perhaps the author is trying to make the case that first class continuations are more important than first class monads for imperative languages. If that's the case, then I tend to agree because, like I said, monads are not difficult to implement even if you don't have explicit support for them. Stack preserving continuations on the other hand... :-PI think the idea of using composable continuations is a very interesting one and I'd like investigate it further, but unless I'm being very dim-witted (a definite possibility) I don't think the matter is as clear as the author hopes.
 Author here. I'm not trying to claim that nested scoped continuations (what the literature calls "delimited continuations with multiple prompts") are objectively easy, although I do think they're a lot easier than monad transformers, especially for imperative programmers. In fact, in the post I say that I'm not sure languages should expose this abstraction directly.It is merely discussed here to show that the theory behind the imperative style is not different from the one behind the PFP style, aimed for those who believe "PFP is just math, while imperative is 'not math'", or to those who are curious to see (as I was) if the imperative style has something like PFP's monad, namely an elegant abstraction that's at the heart of everything.In practice, however, most continuations should be used sparingly if at all, except one -- the thread (in particular, the lightweight thread). Lightweight threads make the most annoying problems of monads in an imperative language go away, and are easy for imperative programmers to use.
 Thanks for the clarification. That makes some sense to me.Also, thank you for the article. It has made me think quite a lot. It's one of those times where my subconscious is saying, "You should pay attention to this", but I'm not quite smart enough to understand what I want to do with it. It will be fun to puzzle it out for a while ;-)
 You don't need to pay attention to scoped continuations. They're a powerful "general" abstraction (like monads), but in practice all you need to know is just the most common kind of continuations -- the (blocking) thread. You'll rarely need to use other instances of continuations, as imperative languages already has their function built into the language (exceptions and even mutable variables).
 I like this because it addresses part of the problem of why I've stopped paying any attention to PLT related topics like denotational semantics, monads, category theory, and higher-order/dependent static type systems in general.In my day to day work the programming language is never the problem because hacking around the limitations of the language to bridge the gap between the problem domain and the computational domain is never the bottleneck. The real problem is when these systems go into production and all static guarantees and beautiful abstractions become basically useless. What I want is something to help me reason about dynamic and evolving large scale software systems. What I get is PLT researchers and library authors bickering over dependent types, monads, and continuations.Here's a concrete and unsolved problem. How do you specify some kind of topology for your production environment and then have whatever system understands this specification reason about performance, error recovery, failover, and scaling issues. In fact the lower level components don't even matter because you could write it in Haskell or Python or Java or whatever is your favorite language. Right now there is nothing because everyone is arguing about continuations and monads. Basically everyone involved is thinking too small. The one person that I think comes close to approaching the problem from the right angle is http://www.cl.cam.ac.uk/~srk31/.
 Nope, my problem isn't reasoning about the lower level components. In fact you can assume I have correctness proofs for every piece of the infrastructure. What I don't have is the higher-level piece that can reason about the lower level components and do so when new pieces are added, old pieces removed, new guarantees enforced, old ones relaxed, etc. A static type system no matter how advanced doesn't help with any of it.
 Yep, that's called the "halting problem", and I hear it's very hard to solve :)Here's how I generally see it. Writing large software is hard (and a software composed of multiple components is large software, even if you decide using the network stack when calling some functions is a good idea ;)). "Type" people (and I'm certainly for some kinds of static types, I just don't think that they're the solution to everything) would tell you that types help restrict your computation in such a way that reasoning about it is easier. To that I say, but I want to do something specific which it's pretty annoying in PFP, and they answer, just do it a different way, to which I say, if I can do it differently, so can the compiler on my behalf. In short, I don't think that explicit types (i.e. those that can be defined in the language you use) are stronger than implicit types (i.e. anything that a verifier can prove about your program), and at least in theory, they are both "the same" (though, see another comment here on what I think about two things being the same in a mathematical sense). We should use whatever is easier for our minds to grasp.The more essential problem -- although I don't know if it's more interesting or less interesting -- is what exactly do we want to do in our programs? If we require a Turing complete model, then no matter how many types -- explicit or implicit -- we throw at the problem, we just won't be able to formally prove properties we might care about. Some people, however, claim that we don't really need Turing completeness, and if we don't, that might open a whole new world of possibilities. But once we start restricting the computational model, the representation we use -- say, PFP or imperative -- might become much more important, each being able to compute things that the other cannot (we know that lambda calculus and Turing machines both compute the same functions, but once we restrict each in some arbitrary ways, it gets harder to find equivalences between restrictions in the PFP model and those in the imperative model).Finally, I think that the notions of what it means "to reason about" or even what it means to be correct (and certainly how important it is to be correct) are themselves vague and require answers from empirical psychological/sociological/economic research than from math.
 I think the people that say we don't need Turing completeness say that because their models can't really accommodate proper reasoning about exactly the kinds of systems I want to reason about. Proving theorems is nice and all but at the end of the day the temporal and dynamic aspects of the system I'm building are what I really care about. Not some static snapshot of it but the actual evolving gestalt.
 Oh, absolutely, but there are formal methods for working with that, too -- well, maybe just the "evolving" part if not the "gestalt" -- mostly based on temporal logic (I can't believe I'm arguing on the side of formal methods now...) See, e.g. the Esterel language[1] used in the industry (directly or through its descendent languages) to write full, safety critical real-time systems. It is an imperative, non-Turing complete language, that is fully verifiable, and actually able to track an evolving gestalt for some restricted definition of "gestalt". Esterel, BTW, has had much more success than Haskell in the industry.Another example is TLA+, which is used by Amazon to verify their (Java, I assume) web services[2]. Unlike Esterel, TLA+ is Turing complete, and can therefore fail to prove many things. It will also take longer and longer to run the bigger the code is, and therefore only verify algorithms, not entire systems.Also, see the history of Statecharts[3], a predecessor to Esterel, that was designed first and foremost to assist humans in writing specifications and only later combined with Pnueli's temporal logic to facilitate formal methods.BTW, the same David Harel who worked with Pnueli on Statecharts and temporal logic, is now involved with Behavioral Programming[4] a very interesting programming style that makes human specifications easier to translate to code. For a usage example, see Harel et al., Programming Coordinated Behavior in Java[5]
 Thanks for the references.
 Then, it seems to me, you are not complaining about programming languages, but some higher-level tools. In production, the “static guarantees and beautiful abstractions” you write about do not become useless. They are just not meant to directly solve the larger-grain emergent problems of distributed systems.
 That's exactly my point. PLT stuff is a minor nuisance for all the stuff that I deal with day to day. It might be the echo chamber but whether a language has support for monads, higher-order types, etc. is not even in list of top 100 things of my concerns and yet it seems like every other PLT researcher is constantly worried about some category theoretical construct or another and trying to jam it into yet another language.
 I don't think we're disagreeing at all in principle. I'm mostly trying to point out that your change is a group whether you think about it or not (actually, several). Then, let the best representation win.Monads aren't a representation, they're a functionality.
 Oh, I know we're not disagreeing in principle, but I do think monads are a representation of a functionality -- effects -- in an algebra that does not have impure functions. Once effects are introduced as fundamental constructs, there is no need to be "thinking in monads" anymore.Imagine if we defined our algebra in such a way that there were no functions -- i.e. nothing that can take parameters and return values -- just sequences of instructions that read and assign global variables (and then define -- outside the calculus -- other effects, such as IO, as changing certain variables). We could then define pure functions in terms of this calculus, rather than doing the opposite and defining change to state in terms of pure functions (i.e. monads). We could then say that a pure function is really a subroutine that performs a transformation on variable addresses which we'll call "variable renaming", and writes its output in some well-known address that the "caller" then renames.In fact, that calculus exists in the Turing Machine, or in our actual computers, and the work of the Haskell compiler is to transform the "high level" concept of pure functions to the "fundamental" representation of instructions and effects... We could then say that even when working with functions you still have to think in terms of instructions (this is actually true if you care about complexity or its earthly form -- performance).Of course, there is no objective way to decide which of these representations is more fundamental.. They are just different, requiring a compiler -- or a mind -- to switch from one to the other. It is, however, possible that one of them results in more efficient programs on current hardware than the other, and one of them might be more natural for human cognition than the other. Or the same one could be both ;) but actually I think reality is more interesting than that.I think both human cognition and compilers might not prefer either but a combination of both. Messy from a mathematical perspective, but that's the nature of computation -- in neurons or silicon. When we need to formally reason about the program, the formal verification tool can then transform the messy representation into one or the other "robust" algebras and do its thing there.
 Uh... What do you think monad transformers do?
 It's pretty interesting that the author did not talk about async/await which gives us back the imperative coding style with futures, effectively solving the problem - it has been adopted by many languages like Python, C# and JavaScript and can be implemented with generators. Generators, are the generalization that gives you the expressiveness you need (not fibers) here. Where are they ineffective here?
 async/await are a form of stackless coroutines (or stackless delimited continuations although that term is rarely, if ever used). They're a limited form of delimited continuations, and are mostly used as a compromise when implementing full coroutines is hard (or not wanted for some reason). Clojure's core.async's go blocks are also stackless coroutines. Basically, they're delimited continuations that only allow suspension ("shift") at the topmost stack frame of the continuation, and don't allow suspending at deeper stack frames.
 I think that most languages don't want the complexity of coroutines, as they are a unfamiliar concept to most programmers. It is a shame that they've never gained popularity as they are very general concept.
 A different take on the merits of explicit yielding (whether by async/await or raw generators), and the perils of full coroutines, by Glyph Lefkowitz of Twisted Python fame:
 I'd say that Lefkowitz's claims are mostly relevant when your runtime has no multicore support (like Python). If your runtime is single-threaded, explicit yields might (it's mostly a matter of taste), make explicit reasoning about state-change ordering easier. But then you're using shared-state concurrency again, and unsafe shared-state to boot. If your runtime has multicore support -- like Java or .NET -- all this doesn't matter, because those concurrent changes Lefkowitz is talking about may happen any time -- not just at yield points.The solution, of course, is not to use unsafe-shared-state-concurrency! Either use threads with messages (like Erlang), or threads with transactional shared-state, like Clojure, or both (in fact even Erlang has both actors and ETS, and Clojure has agents and channels as well as atoms and refs).
 He does (briefly) mention that kind of variation and why it's a slightly different idea in the original presentation. It's around 28 minutes into the video.

Applications are open for YC Summer 2019

Search: