> You'll be disappointed if you're expecting a discussion of effect systems...

I'm expecting a discussion of why continuations are enough.

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
    }

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, ...

    method2(method1())

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.

I both agree and disagree, because that very much depends on the domain. From a mathematical point of view, whenever two things are isomorphic, then they are the "same". But from a programming point of view, the two can be very different, as abstractions are psychological interactions with the programmer's mind, and two isomorphic mathematical concepts can psychologically interact very differently with the programmer. Therefore, if I don't have to "think in monads" when working with an abstraction, then the abstraction is not a monad, even if an isomorphism exists between them.

As it has been proven (I think) that any effect can be modeled by monads, you could say that all effects are monadic, and just like the mathematician in the famous joke, that's absolutely true yet absolutely useless. In a programming language, abstractions are defined (and measured) both by mathematical as well as psychological properties.

So I think the difference is of substance because it has vastly different psychological properties (more than just thin syntactic sugar).

Right, it's not just syntactic sugar, it's also the type system, and it may also touch on the run-time system. I think we've been in violent agreement from the beginning but I just didn't realise it. I interpreted your language as being somewhat combative and that put me on the defensive.

I'm sorry, then, and take full responsibility. Internet culture -- at least in forums such as this -- rewards texts with emotional content more than those devoid of it. As there are many texts breathlessly extolling the virtues of monads, I had to offset that a bit ;)

That is an understandable impetus ;)

    ^x {
        ...
        cont c
        ...
    }

    c() {
        ...
        pause(^x = foo)
        ...
    }

    ^x {
        ...
        cont c
        ...
        cont c
        ...
    }

This was all a bit confusing, so if you can point me to a reference I would be grateful. Unfortunately "scoped continuations" has very few hits on Google. In fact by the time you read this, this comment is probably one of the top hits!