6 ms·

I've been waiting for this piece for a while. Monads don't compose! Under an effect-based system: fn get_user<F>() -> F<User> Is like having an explicit

I've been waiting for this piece for a while. Monads don't compose! Under an effect-based system: fn get_user<F>() -> F<User> Is like having an explicit effect F: fn get_user<F>() ->{F} User Where {F} is the effect set. Note that User is no longer wrapped in F, and that we can extend the effect set (e.g. {F, G, H}) Consider a function that is async and throws an error. Is this: Promise<Exn<T>> Or: Exn<Promise<T>> Convention (and common sense) dictates the former, but in the face of many effects, who's to say there even is an order at all? By using an effect set, we get: {Promise, Exn} T And we can even ensure that our function is generic over additional effects: {Promise, Exn, F} T Individual monads compose, but multiple requires explicit composition. By modeling monadic effects using the free monad (i.e. effect sets), we can circumvent the colored function problem entirely: functions can have different colors, and be generic over any other color it might come in contact with. Cool beans!

contravariant 5y ago
Are you sure you don't mean 'commute'? Monads, being endofunctors, compose just fine. Though the composition may or may not be a monad I suppose.
- the-alt-one 5y ago
  "Monads don't compose" is a common sentence (google it!), for example here: https://stackoverflow.com/questions/7040844/applicatives-compose-monads-dont https://stackoverflow.com/questions/7040844/applicatives-com... Maybe you already knew about this and is still asking, though?
  - contravariant 5y ago
    I wasn't aware. The examples given here are all cases where the monad doesn't commute, hence my question. If two monads commute you can show that the composition of the two is (trivially) a new monad, but I'm not sure if the converse also holds.
    - kmill 5y ago
      It's not very precise talking about whether a monad commutes -- it's not clear what "commutes" should really mean (certainly not F . G = G . F since that's way too restrictive). I started working it out by hand, but then figured nLab had it somewhere, and indeed: https://golem.ph.utexas.edu/category/2017/02/distributive_laws.html https://golem.ph.utexas.edu/category/2017/02/distributive_la... F, G, and F.G are monads if and only if there is a "distributive law," which is a natural transformation G.F -> F.G satisfying some properties. It's like something that satisfies half the braiding properties, where braidings are already a weaker version of commutativity.
      - contravariant 5y ago
        That's a very interesting article, thanks. That said while FG = GF is indeed restrictive, requiring there to be a natural isomorphism between them is slightly less restrictive and just requiring the existence of a distributive law seems a bit too broad. What's preventing the existence of multiple distributive laws? Is there even anything preventing monads from always having a distributive law?
        kmill 5y ago
        There is nothing at all preventing the existence of multiple distributive laws, and I can think of some (non-programmy) examples that have multiple possibilities. I wouldn't be surprised if some cohomology group classifies them, at least in certain settings. I don't know about whether distributive laws always exist, but what is probably true is that there's no universal distributive law -- that's in the sense that you have a function from pairs of monads to distributive laws that is natural with respect to homomorphisms of monads, whatever those are (I know there's a bicategory of monads, but that's about it).
- isaacimagine 5y ago
  As you said, the composition of a monad may not be a monad, which means it may not be possible to compose the result of a monadic composition with another monad. You can always trivially compose a set of effect sets (union), though.
  - contravariant 5y ago
    That doesn't sound right, even if the composition fails to be a monad it's still a functor so there's no reason you couldn't keep composing with other functors (in particular other monads).
    - pdpi 5y ago
      But that is precisely why we say that functors compose (in the general case) and monads don't (again, in the general case)!
    - dllthomas 5y ago
      While getting at a real issue, people are being sloppy with what they mean by "monads" and "compose" on both sides of it. Types which are monads compose to make types that are definitely functors but maybe (probably?) not monads. That "maybe not" is what type theory people mean when they say "monads don't compose" but it's mostly not what's bugging people because... Most monads can be rewritten as monad transformers (where applying them to the identity monad reproduces the original monad), which do compose in that way, and this is often what people do in Haskell when they have code that needs multiple effects. But! Values of different types (like, say, a `WriterT t (Identity u)` and a `WriterT t (IO u)` can't be composed using the ever-so-convenient Monad interface which is the reason we wanted to make things Monads in the first place. This is what the article is discussing and it's what programmers often mean when they say "monads don't compose". The workaround in the Haskell ecosystem (at least in those parts that haven't adopted effect systems or free monads w/ interpreters) is to write as much of your logic as possible using an unspecified monad, only asking for the functionality you need by way of constraints. Constraints compose like gangbusters! Values with unifiable types that have different sets of constraints? Well, it must've been a type that satisfies all of those constraints. And the abstract type is a nice place to stick in mocks as you test the pieces of things. This shares much of the downside of effect sets, in that it is awkward to specify order ("layering"?) of effects when they do matter; it's possible to be more concrete about the types for those pieces but it does spread to the pieces that contain them and can sometimes get boilerplatey. Whether that's worth it for the added safety is going to be context dependent.
rawling 5y ago
> Consider a function that is async and throws an error. Is this [x] or [y]? Is it not that one of these is "an async function that may throw an error immediately" and one "an async function that may throw an error asynchronously"?
- isaacimagine 5y ago
  This wasn't the best example, as async is directly tied to execution order. But consider a function that is nondeterministic, does IO, and may raise an exception. Is this a: Ndet<Io<Exn<T>>> Ndet<Exn<Io<T>>> Io<Ndet<Exn<T>>> Io<Exn<Ndet<T>>> Exn<Ndet<Io<T>>> Exn<Io<Ndet<T>>> There isn't really a good general answer. Most languages sweep this under the rug in sone way or other: 'Io, and Ndet, and Exn can be done at any point' or 'just use hidden mutable state' are common. By using effect sets, we can extract fine-grained over the effects in a program at a given point, without having to worry how effects are assembled and dispatched (indeed, in effect-based languages, most of these effects can be statically inferred). Most functional languages do model these effects using monads, and provide powerful transformations to ensure that the ordering of encapsulation doesn't matter. The composition is explicit, but at least it's a lot easier than languages that don't support monads. Writing a language is as much about choosing limitations as it is features. Going from the untyped to the typed lambda calculus limits the number of programs that can be expressed (at least until dependent types get involved), but makes it easier to reason about the remaining set of programs. Monads are more powerful, but harder to reason about. A language without monads that doesn't compromise on an effect system is a pretty great language in my book.
  - rawling 5y ago
    Fair enough, thanks for explaining.
steinuil 5y ago
I was trying to write a comment making the same point but honestly, I'm not familiar enough with effects to know what exactly you can do with them. Good to know that I wasn't far off! I'm curious about one thing though: unless you're passing a parameter that introduces an additional effect F into the function, what's the point of making it generic over the effect set? In a language with typed effects, all effects that could be performed by a function would already be known, so letting a unit function `fn get_user<F>() ->{F} T` where i.e. `F: DiagnosticData -> ()` decide which instance of an effect that takes a DiagnosticData and yields unit, as opposed to `fn get_user<F>(g: () ->{F} ()) ->{F} User` where the effect is clearly introduced by `g`, seems a bit overkill to me.
- isaacimagine 5y ago
  > unless you're passing a parameter that introduces an additional effect F into the function This definitely is overkill, I just wanted to illustrate that it was possible. You're correct: usually, a generic effect indicates you're passing a closure to the function that may execute additional effects: fn filter_users<F>( cond: fn<F>(User) ->{F} Bool, users: List<User> ) ->{F} List<User> If filter_users calls the closure cond, effect F will be performed, so filter_users must perform F as well. In the case where there are no external effects, F will be inferred to be the union of the empty set and whatever effects are used in the body of the function. Some languages are actually pretty strict about this, and explicitly declaring an empty effect set may mark the function as pure, which may not be what you want!
dllthomas 5y ago
> Convention (and common sense) dictates the former, but in the face of many effects, who's to say there even is an order at all? It might come down to implementation, but I would expect the different types to signify different behavior. With Exn<Promise<T>>, we have something that can throw errors in producing an promise, but then that Promise reliably returns a T (if it completes at all, but then we probably don't have a termination checker in non promise code anyway so we're probably used to hand waving that away). With Promise<Exn<T>>, on the other hand, you definitely have a Promise and the computation won't raise an exception until after you've awaited it (or equivalent). You have errors and nondeterminism? Well, do errors cause rollback or abort the entire thing? Nondeterminism and a Writer? Do we collect observations from execution traces that didn't complete? Effect sets either greatly restrict the kinds of effects we can talk about (and your example already includes some that we need to rule out), or pretend that ordering does not matter when it clearly does.
- isaacimagine 5y ago
  I agree, Promise<Exn<T>> is an admittedly bad example. See my response to the sibling comment for a better example. Effect sets don't prevent you from using monadic wrappers when appropriate. In combination with delimited continuations, effects allow languages to reify effectful computation in an understandable and computationally efficient manner. > You have errors and nondeterminism? Well, do errors cause rollback or abort the entire thing? It depends on how the handler is implemented, meaning the user of a function who is calling an effect has the ability to override the way the effect is performed. Traditional exceptions, exceptions that resume, or computations that can be canceled can all be implemented using an effect system. There are a lot of papers on Algebraic effects, but the best way to convince you of their utility is to look into the literature yourself. The koka language guide, 'Algebraic effects for the rest of us' and (later) oleg's work are good starting points. > or pretend that ordering does not matter when it clearly does. Ordering does matter; effects are performed in the order they are produced.
  - dllthomas 5y ago
    > See my response to the sibling comment for a better example. Your better example isn't better; it's a more complicated version of an example I discussed. > It depends on how the handler is implemented, meaning the user of a function who is calling an effect has the ability to override the way the effect is performed. Yes, and that's my point. I might write foo with an assumption that errors rollback, and bar with an assumption that errors abort. Now I can't use foo and bar with the same handler, the types don't make that visible, and the errors might be subtle. These things have color we're just choosing to be blind to it! > Ordering does matter; effects are performed in the order they are produced. There are two different senses of "ordering" here - let's call mine "layering" then? > There are a lot of papers on Algebraic effects, but the best way to convince you of their utility is to look into the literature yourself. I've read papers, I've been variously excited about them at various points over the past ~10 years, but I've come to believe they're simply not an improvement over mtl-style constraints with layering expressed when we need it. I believe what's missing from mtl-style is a better way to partially specify necessary layering relationships, and that's not something I've seen effects systems provide.
iamwil 5y ago
Have you used Algebraic Effects a lot? What are the downsides to using them in your experience, if you have?
- isaacimagine 5y ago
  I have some experience with effects, mostly from noodling around with Koka and implementing a small effect-based toy language. (Which I intend to integrate into a larger language I'm working on.) There are a few downsides, and they fall into four categories: 1. Effect sets get rid of external effect ordering. If you have an effect set {A, B}, you can't know if A happens before B without reading the code. Same issue as monad transformers. 2. Handlers are sometimes hard to reason about. A handler is essentially a fancy try/catch block for resumable exceptions. And construct that introduces a non-local control-flow dependency can be hard to reason about. (This is especially true as a compiler writer, haha) 3. The syntax is hard. I'm serious: how do you even represent an effect set? I went with a unison-like approach in my post, but this breaks down in an unsatisfactory if you make some other decisions. Also, what is an effect set in relation to your languages type system? Is it just a fancy enum? Should we allow other sets of types? What does an effect set mean on its own? 4. Lack of idioms and libraries. Result<T, E> is well-established - what idioms arise when programming with effects? In my experience, effects are rarely explicit, and are only used if you're trying to implement something using non-trivial control flow, like generators or cancellation.
  - dwohnitmok 5y ago
    > If you have an effect set {A, B}, you can't know if A happens before B without reading the code. Same issue as monad transformers. Monad transformers don't have this issue. They have a well defined order in their types (e.g. `ExceptT e (StateT s)` is different from `StateT s (ExceptT e)` the latter blows away the state and aborts on an error, while the former preserves state on an error).
    - isaacimagine 5y ago
      When working with monad transformers, I tend to stick to constraining functionality over unspecified monad. This essentially acts as a set (of constraints), which results in all the set-based woes that arise when effects are used. So not monad transformers themselves per se, you're right.
dgreensp 5y ago
Interesting. What language is a good example of having effect sets? Koka? What about the case of needing context like “correlation id,” from the article? Can that be modeled as an effect?
- isaacimagine 5y ago
  Koka is a good example of a language having effect sets: in koka, it's called a row of effects, and is written as <exn, console, e> where single letters denote generic params. In the case of needing a correlation id, this is a great use case for effects! First we declare an effect type: effect correlation_id ctl id(): int Then we set up a handler: with ctl id() resume(7) log("nice!") Here we just use 7, but we could be incrementing a counter per request or something. Then any functions that are called in this scope, when they call 'id', will receive 7: fun log(message: string): <console, correlation_id> () { println(id()) println(message) } Which, using the above handler, would print: 7 nice! For example. Hope this helps!

contravariant 5y ago

Are you sure you don't mean 'commute'? Monads, being endofunctors, compose just fine. Though the composition may or may not be a monad I suppose.

the-alt-one 5y ago
"Monads don't compose" is a common sentence (google it!), for example here: https://stackoverflow.com/questions/7040844/applicatives-compose-monads-dont https://stackoverflow.com/questions/7040844/applicatives-com... Maybe you already knew about this and is still asking, though?
- contravariant 5y ago
  I wasn't aware. The examples given here are all cases where the monad doesn't commute, hence my question. If two monads commute you can show that the composition of the two is (trivially) a new monad, but I'm not sure if the converse also holds.
  - kmill 5y ago
    It's not very precise talking about whether a monad commutes -- it's not clear what "commutes" should really mean (certainly not F . G = G . F since that's way too restrictive). I started working it out by hand, but then figured nLab had it somewhere, and indeed: https://golem.ph.utexas.edu/category/2017/02/distributive_laws.html https://golem.ph.utexas.edu/category/2017/02/distributive_la... F, G, and F.G are monads if and only if there is a "distributive law," which is a natural transformation G.F -> F.G satisfying some properties. It's like something that satisfies half the braiding properties, where braidings are already a weaker version of commutativity.
    - contravariant 5y ago
      That's a very interesting article, thanks. That said while FG = GF is indeed restrictive, requiring there to be a natural isomorphism between them is slightly less restrictive and just requiring the existence of a distributive law seems a bit too broad. What's preventing the existence of multiple distributive laws? Is there even anything preventing monads from always having a distributive law?
      - kmill 5y ago
        There is nothing at all preventing the existence of multiple distributive laws, and I can think of some (non-programmy) examples that have multiple possibilities. I wouldn't be surprised if some cohomology group classifies them, at least in certain settings. I don't know about whether distributive laws always exist, but what is probably true is that there's no universal distributive law -- that's in the sense that you have a function from pairs of monads to distributive laws that is natural with respect to homomorphisms of monads, whatever those are (I know there's a bicategory of monads, but that's about it).
isaacimagine 5y ago
As you said, the composition of a monad may not be a monad, which means it may not be possible to compose the result of a monadic composition with another monad. You can always trivially compose a set of effect sets (union), though.
- contravariant 5y ago
  That doesn't sound right, even if the composition fails to be a monad it's still a functor so there's no reason you couldn't keep composing with other functors (in particular other monads).
  - pdpi 5y ago
    But that is precisely why we say that functors compose (in the general case) and monads don't (again, in the general case)!
  - dllthomas 5y ago
    While getting at a real issue, people are being sloppy with what they mean by "monads" and "compose" on both sides of it. Types which are monads compose to make types that are definitely functors but maybe (probably?) not monads. That "maybe not" is what type theory people mean when they say "monads don't compose" but it's mostly not what's bugging people because... Most monads can be rewritten as monad transformers (where applying them to the identity monad reproduces the original monad), which do compose in that way, and this is often what people do in Haskell when they have code that needs multiple effects. But! Values of different types (like, say, a `WriterT t (Identity u)` and a `WriterT t (IO u)` can't be composed using the ever-so-convenient Monad interface which is the reason we wanted to make things Monads in the first place. This is what the article is discussing and it's what programmers often mean when they say "monads don't compose". The workaround in the Haskell ecosystem (at least in those parts that haven't adopted effect systems or free monads w/ interpreters) is to write as much of your logic as possible using an unspecified monad, only asking for the functionality you need by way of constraints. Constraints compose like gangbusters! Values with unifiable types that have different sets of constraints? Well, it must've been a type that satisfies all of those constraints. And the abstract type is a nice place to stick in mocks as you test the pieces of things. This shares much of the downside of effect sets, in that it is awkward to specify order ("layering"?) of effects when they do matter; it's possible to be more concrete about the types for those pieces but it does spread to the pieces that contain them and can sometimes get boilerplatey. Whether that's worth it for the added safety is going to be context dependent.

rawling 5y ago

> Consider a function that is async and throws an error. Is this [x] or [y]? Is it not that one of these is "an async function that may throw an error immediately" and one "an async function that may throw an error asynchronously"?

isaacimagine 5y ago
This wasn't the best example, as async is directly tied to execution order. But consider a function that is nondeterministic, does IO, and may raise an exception. Is this a: Ndet<Io<Exn<T>>> Ndet<Exn<Io<T>>> Io<Ndet<Exn<T>>> Io<Exn<Ndet<T>>> Exn<Ndet<Io<T>>> Exn<Io<Ndet<T>>> There isn't really a good general answer. Most languages sweep this under the rug in sone way or other: 'Io, and Ndet, and Exn can be done at any point' or 'just use hidden mutable state' are common. By using effect sets, we can extract fine-grained over the effects in a program at a given point, without having to worry how effects are assembled and dispatched (indeed, in effect-based languages, most of these effects can be statically inferred). Most functional languages do model these effects using monads, and provide powerful transformations to ensure that the ordering of encapsulation doesn't matter. The composition is explicit, but at least it's a lot easier than languages that don't support monads. Writing a language is as much about choosing limitations as it is features. Going from the untyped to the typed lambda calculus limits the number of programs that can be expressed (at least until dependent types get involved), but makes it easier to reason about the remaining set of programs. Monads are more powerful, but harder to reason about. A language without monads that doesn't compromise on an effect system is a pretty great language in my book.
- rawling 5y ago
  Fair enough, thanks for explaining.

steinuil 5y ago

I was trying to write a comment making the same point but honestly, I'm not familiar enough with effects to know what exactly you can do with them. Good to know that I wasn't far off! I'm curious about one thing though: unless you're passing a parameter that introduces an additional effect F into the function, what's the point of making it generic over the effect set? In a language with typed effects, all effects that could be performed by a function would already be known, so letting a unit function `fn get_user<F>() ->{F} T` where i.e. `F: DiagnosticData -> ()` decide which instance of an effect that takes a DiagnosticData and yields unit, as opposed to `fn get_user<F>(g: () ->{F} ()) ->{F} User` where the effect is clearly introduced by `g`, seems a bit overkill to me.

isaacimagine 5y ago
> unless you're passing a parameter that introduces an additional effect F into the function This definitely is overkill, I just wanted to illustrate that it was possible. You're correct: usually, a generic effect indicates you're passing a closure to the function that may execute additional effects: fn filter_users<F>( cond: fn<F>(User) ->{F} Bool, users: List<User> ) ->{F} List<User> If filter_users calls the closure cond, effect F will be performed, so filter_users must perform F as well. In the case where there are no external effects, F will be inferred to be the union of the empty set and whatever effects are used in the body of the function. Some languages are actually pretty strict about this, and explicitly declaring an empty effect set may mark the function as pure, which may not be what you want!

dllthomas 5y ago

> Convention (and common sense) dictates the former, but in the face of many effects, who's to say there even is an order at all? It might come down to implementation, but I would expect the different types to signify different behavior. With Exn<Promise<T>>, we have something that can throw errors in producing an promise, but then that Promise reliably returns a T (if it completes at all, but then we probably don't have a termination checker in non promise code anyway so we're probably used to hand waving that away). With Promise<Exn<T>>, on the other hand, you definitely have a Promise and the computation won't raise an exception until after you've awaited it (or equivalent). You have errors and nondeterminism? Well, do errors cause rollback or abort the entire thing? Nondeterminism and a Writer? Do we collect observations from execution traces that didn't complete? Effect sets either greatly restrict the kinds of effects we can talk about (and your example already includes some that we need to rule out), or pretend that ordering does not matter when it clearly does.

isaacimagine 5y ago
I agree, Promise<Exn<T>> is an admittedly bad example. See my response to the sibling comment for a better example. Effect sets don't prevent you from using monadic wrappers when appropriate. In combination with delimited continuations, effects allow languages to reify effectful computation in an understandable and computationally efficient manner. > You have errors and nondeterminism? Well, do errors cause rollback or abort the entire thing? It depends on how the handler is implemented, meaning the user of a function who is calling an effect has the ability to override the way the effect is performed. Traditional exceptions, exceptions that resume, or computations that can be canceled can all be implemented using an effect system. There are a lot of papers on Algebraic effects, but the best way to convince you of their utility is to look into the literature yourself. The koka language guide, 'Algebraic effects for the rest of us' and (later) oleg's work are good starting points. > or pretend that ordering does not matter when it clearly does. Ordering does matter; effects are performed in the order they are produced.
- dllthomas 5y ago
  > See my response to the sibling comment for a better example. Your better example isn't better; it's a more complicated version of an example I discussed. > It depends on how the handler is implemented, meaning the user of a function who is calling an effect has the ability to override the way the effect is performed. Yes, and that's my point. I might write foo with an assumption that errors rollback, and bar with an assumption that errors abort. Now I can't use foo and bar with the same handler, the types don't make that visible, and the errors might be subtle. These things have color we're just choosing to be blind to it! > Ordering does matter; effects are performed in the order they are produced. There are two different senses of "ordering" here - let's call mine "layering" then? > There are a lot of papers on Algebraic effects, but the best way to convince you of their utility is to look into the literature yourself. I've read papers, I've been variously excited about them at various points over the past ~10 years, but I've come to believe they're simply not an improvement over mtl-style constraints with layering expressed when we need it. I believe what's missing from mtl-style is a better way to partially specify necessary layering relationships, and that's not something I've seen effects systems provide.

iamwil 5y ago

Have you used Algebraic Effects a lot? What are the downsides to using them in your experience, if you have?

isaacimagine 5y ago
I have some experience with effects, mostly from noodling around with Koka and implementing a small effect-based toy language. (Which I intend to integrate into a larger language I'm working on.) There are a few downsides, and they fall into four categories: 1. Effect sets get rid of external effect ordering. If you have an effect set {A, B}, you can't know if A happens before B without reading the code. Same issue as monad transformers. 2. Handlers are sometimes hard to reason about. A handler is essentially a fancy try/catch block for resumable exceptions. And construct that introduces a non-local control-flow dependency can be hard to reason about. (This is especially true as a compiler writer, haha) 3. The syntax is hard. I'm serious: how do you even represent an effect set? I went with a unison-like approach in my post, but this breaks down in an unsatisfactory if you make some other decisions. Also, what is an effect set in relation to your languages type system? Is it just a fancy enum? Should we allow other sets of types? What does an effect set mean on its own? 4. Lack of idioms and libraries. Result<T, E> is well-established - what idioms arise when programming with effects? In my experience, effects are rarely explicit, and are only used if you're trying to implement something using non-trivial control flow, like generators or cancellation.
- dwohnitmok 5y ago
  > If you have an effect set {A, B}, you can't know if A happens before B without reading the code. Same issue as monad transformers. Monad transformers don't have this issue. They have a well defined order in their types (e.g. `ExceptT e (StateT s)` is different from `StateT s (ExceptT e)` the latter blows away the state and aborts on an error, while the former preserves state on an error).
  - isaacimagine 5y ago
    When working with monad transformers, I tend to stick to constraining functionality over unspecified monad. This essentially acts as a set (of constraints), which results in all the set-based woes that arise when effects are used. So not monad transformers themselves per se, you're right.

dgreensp 5y ago

Interesting. What language is a good example of having effect sets? Koka? What about the case of needing context like “correlation id,” from the article? Can that be modeled as an effect?

isaacimagine 5y ago
Koka is a good example of a language having effect sets: in koka, it's called a row of effects, and is written as <exn, console, e> where single letters denote generic params. In the case of needing a correlation id, this is a great use case for effects! First we declare an effect type: effect correlation_id ctl id(): int Then we set up a handler: with ctl id() resume(7) log("nice!") Here we just use 7, but we could be incrementing a counter per request or something. Then any functions that are called in this scope, when they call 'id', will receive 7: fun log(message: string): <console, correlation_id> () { println(id()) println(message) } Which, using the above handler, would print: 7 nice! For example. Hope this helps!