OK, I think there's a fundamental misunderstanding at play here, of what purity, effects and monads are. Koka's effects system is monadic! Crazy huh? Well lo

OK, I think there's a fundamental misunderstanding at play here, of what purity, effects and monads are. Koka's effects system is monadic! Crazy huh? Well look: function main() { bind(foo, bar) } function foo() { println("Returning 3") return 3 } function bar(x) { println("Adding 1 to my argument and printing") y = x + 1 println(y) } function bind(x : () -> e a, f : a -> e b) : e b { y = x() return f(y) } function return_(x) { return x } I can define return and bind generically over effects e just like in Haskell! Checked exceptions in Java are also monadic! Well, in a sense but I don't know enough about Java to write down the types correctly. Maybe the types can't even be written, but it doesn't stop the nature of checked exceptions being monadic. Specifically, if I have A method1() throws Exception1, Exception2, ... B method2(A) throws Exception1, Exception2, ... then combining them thusly method2(method1()) is exactly binding in a monad. It's not a monad defined as a specific datastructure in your language, but it is a monadic operation. It's pretty much the same monadic operation as the bind in the hypothetical "universal monad"[2] you propose in your talk. The reason effects are monadic is that if you have a computation C1 that does effects of type E and that returns a value of type A, and an computation C2 that does effects of type E and that takes a value of type A as argument and returns a value of type B, then you can combine them to form a function that does effects of type E and returns a value of type B. This is the bind of a monad! Different languages may have different levels of support for the syntax of effects/monads at the type or value level, for programming generically with effects/monads, and for defining your own and combining them, but the fact remains that effects are monadic. The misunderstanding is that you seem to think a monad is a value along with some extra stuff. In particular, you think that in a pure language a value of type IO is a value along with some extra stuff. This is wrong! It's understandable that you came to this conclusion given the thousand misleading monad tutorials that say "a monad is a value in a context" or "when you use IO you are building up a computation for an impure runtime to run". But this is wrong! Haskell is not a "pure language". "Pure language" is a not a well-defined concept. It's simply a neat slogan to summarize one of Haskell's characteristics without getting technical. What is pure in Haskell is let bindings and function application. That's it. (In fact I would classify Koka under the slogan "pure language" since you can tell from its type whether a function performs any effects.) IO in Haskell is exactly an effect type like 'console' in Koka. It is monadic in Haskell, like in Koka. In Haskell it's slightly more awkward because let bindings and function application are pure so you are forced to use monad combinators (or do notation) to combine them, but this is just a syntactic difference not one of any substance[1]. Koka has better support for combining effects through essentially the "universal monad"[2] you mentioned in your talk. In the implementation of Haskell[3] a function of type 'a -> IO b' is exactly the same as a function of type 'a -> b'[4]. It isn't a function "which returns an 'IO b' which is an instruction to an impure runtime to run some effectful code". It isn't "a 'b' in a context". It isn't "a 'b' with some other stuff". Haskell does not "trigger effects in the runtime by returning monadic values". Haskell has effects! I'll reiterate because this is important. A function of type 'a -> IO b' is exactly a function 'a -> b'. It's just been tagged with an effect type called 'IO'. We combine these effect types with monadic combinators because the nature of effects in monadic, not for any other reason. Some other monads (Either, Maybe, State) are more like what you are thinking of. But they're different monads! They don't somehow subsume the entire nature of monads. Monads, like effect types, can simply be used for tracking effects. Monads will always be part of effect systems. [1] I am very happy to consider syntactic improvements that make effects more easy to work [2] I disagree that the "universal monad" is not typeable in Haskell. At least some version of a "universal monad" is typeable. It may look a bit awkward though. [3] At least in GHC. Other implementations are free to do what they want. [4] Actually slightly augmented with a trick to stop the optimizer breaking, but that's not of substance.