To me "What Color is Your Function" (the original article this one refers to) was so obviously discussing monads that I was surprised by the reveal it was specifically focused on async. In retrospect I shouldn't have, because that article was about mainstream languages and few of them mention monads by name.
The curse of those who have used and understood Monads is that we see them everywhere. Async, Exceptions, IO, State machines. Everywhere you look you see a monad.
Seeing beyond the hammer nail thing is kind of part of growing up as an engineer. I had to figure out monads in the mid nineties as part of my functional programming course work. Lot of fun, not very practical at the time since all the mainstream languages of the day were basically not functional programming languages. The way people explain monads has not improved a lot since there. It still sounds like a bunch of gobblygook.
I usually translate in my head to side-effect thingies. Much easier. So, Maybe<T> is short hand for it could be there, or not, you'd have to check. Same with Result<T>. Or Optional<T>. Or Future<T>. It's nicer than having null as a default value and then triggering a null pointer exception because you forgot to check but a bit less readable if you start wrapping them.
But if you have a language with nullable types, like Kotlin, you can your cake and eat it. For example, you can have functions like isNullOrBlank defined on nullable strings (String?) which don't throw a null pointer exception if you call them on a null value. Just syntactic sugar for the common use case.
Likewise, Kotlin has more syntactic sugar that functional programming types would frown upon that is actually nice to use. Like suspend functions that you can use to write asynchronous programs that almost look like they are normal synchronous ones. With proper support for cancelled co-routines, error handling, threading, reactive programming, etc. Yes, they're colored functions. But, colored functions are nice and easy to work with. My compiler will tell me off when I do it wrong.
Is it all monads under the hood or just a pragmatic language?
I'm not sure you quite said this but nullable isn't just another word for Optional with syntactic sugar. You can have Optional<Optional<Integer>>, but Integer?? is not a thing. This means you can't (or shouldn't?) use it for, say, return value of a generic "get a value from a map" because you might want to be able to store nullable values in the map and probably want to distinguish "it wasn't there" from "it was there but the value was null". IIRC, in some languages with generics and nullable you can't actually write a function that applies ? to a generic argument, because there's no way to say that the generic argument isn't itself nullable.
I'm not disagreeing, but this is a very good jumping off point for what is an enormous discussion in the philosophy of programming right now. You've identified the correspondence between the programming language support and relevant monadic constructions. There's also the principle that programming is about applying relevant abstractions. The point of contention revolves around the question of "Should monads be available to programmers in the abstract where programmers are supported enough to write their own monads? Or should monads be reified into language constructs, thus making it a up to the language designer to choose the finite set of available monads and syntactify them into language constructs?
A vocal camp wants monads in the abstract and feels like reified monads as language constructs completely misses the point. The other camp is happy to accept new syntax and keywords to get their work done and see monads as ivory tower language enthusiasm. The choices that language designers make increasingly put their languages on one side or another of this dividing line.
This is true of any sufficiently general abstraction. Like a multi graphs and effects systems.
In fact overly general abstractions are an anti pattern in practical software development, at least in my opinion. Any problem can be successfully extrapolated to a more general case, that doesn't mean it's worth doing it.
They do give you a template for approaching certain problems though. Even if your implementation of the template in your head is specific and therefore easier to follow in the implementation. It's useful to have an understanding of them for that reason.
The results of those templates seems to be a lot different from regular old boring industry standard reusable code, which has design patterns(Developed over the years for everyday practicality) as the templates instead of abstract logic(Seemingly chosen for beauty and ability to express original ideas).
They say you can find monads everywhere, but doesn't that mean that by using monads as a starting point, you'll have more freedom and less structure and predictability than if you used a GoF pattern?
One difference with monads at least in Haskell is we have the concepts of lifting a computation in one type to a type of another (Monad Transformers), and then dropping those transformations to a base type (such as IO) via monad-control. This lets you pretty easily call functions of different colors without a lot of manual wrapping and unwrapping. To make it super convenient you do need to use a lifted version of the base library, which is sort of like a color-agnostic set of IO functions that can be directly called from any transformer stack that implements the proper typeclasses.
Certainly but Scala has that, and it has typeclass like implicits. I'm not sure if it can do monad-control though, here is a list of all the type extensions used for that:
One day ill make the jump from "just" f# to haskell.
While i usually could solve it in a different way, such things would have made it quite a bit nicer (the zoo of .map, .fold and such is a bit annoying)
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.
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).
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.
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?
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).
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.
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).
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.
> 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"?
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:
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.
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.
> 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:
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!
> 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.
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.
> 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.
I apologize if my response sounded dismissive, I typed it out on my phone in a rush.
> I might write foo with an assumption that errors rollback, and bar with an assumption that errors abort. [...] These things have color we're just choosing to be blind to it!
This is more of a question of API design than something inherit to effect systems. I think it would be a good idea to use separate types for rolled-back errors and aborting errors; in the case where two functions use the same effect with different handlers, you can always mask the effect[0].
I do not think effect systems ignore color, rather, they give the end-user control over how color is manifested. Sometimes it's desirable to be blind to color.
On the other hand, I do agree that effect systems throw away layering information, much in the same way that auto-collapsing a nested Option None to None defeats the whole purpose of Option types.
Effects can be used with traditional monads, and it's possible to reify effects into monad-like objects that can be handled like values. I mean, that's what an effect handler does: it matches on the enum of effects in scope as if they were a value!
> but I've come to believe they're simply not an improvement over mtl-style constraints with layering expressed when we need it.
Typed tagless form is great, and (on an unrelated note) I love typed tagless final interpreters.
Although I agree that specifying layering relationships is an important component of managing effectful composition, I think the largest issue with mtl-style constraints is that the constraints require higher-kinded types by design. HKTs are really cool, but like a lot of meta-functiinal features can really drag down compilation times.
Effects are nice because they can be implemented as a single pass + cps transform, and existing control flow constructs can be re-written as sugar in terms of effects with no additional overhead (as delimited continuations do not require making a copy of the stack).
But I digress. Monads (and more generally HKTs) give you powerful tools that allow you to prove certain properties about the way effect constraints propogate through a system. I advocate for effects not because they are a replacement for monads, but because they are a nice method for reifying disparate threads of computation in a trivially composable manner.
I also don't think that all layering should be replaced with effects. I think careful layering with the occasional effect when needed is the way to go. Balance and simplicity in all things.
Sorry for the late comment, but... Do you have any literature references on the combination of delimited continuations and effect systems. I would certainly be interested in some of the formalisms used to discuss the efficiency characteristics of effectful computations.
Oleg has a lot of good work on continuations and effects. You can also check his papers for additional references, but the papers on these two pages of his should serve a good jumping off point:
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.
> 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).
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.
I was half expecting by the end that the punchline of WCIYF was going to be either IO (the Haskell data type) or Java's checked exceptions, the latter of which is mentioned in WCIYM.
Before we get to the end of WCIYF, we could freely substitute in async (promises); the possibility of exceptions (Java-style checked exceptions in particular); outside-world interactions (Haskell IO); or anything else.
Of course, what we experience in Haskell and other strongly-typed functional languages is that we colour our functions all the time! Not just red and blue; but sometimes green, or yellow, or a combination of several colours at once!
Why is it so ergonomic in a language designed around this concept? What we see in JavaScript is that having the colours (effectively, the monadic wrappers) isn't enough. We also need tools for abstracting and generalising these notions, so that composition goes from being a syntactic disaster to a semantic convenience.
> We also need tools for abstracting and generalising these notions, so that composition goes from being a syntactic disaster to a semantic convenience.
I've been speculating for a while that the problem with Java's checked exceptions was principally the impoverished language we had to talk about them. If we could write things like "this throws anything the argument throws, except XYZ" things... might've turned out considerably differently.
> you should just bite the bullet and make everything red
I agree! It's also what I've been seeing in i.e. Scala, where everything is converging to a single Monad. And in that case, monads are basically unnecessary. The point of them is to be able to customize your function colors.
Just use a language whose semicolon/newline semantics reflect the functionality you'd otherwise get with your "red" monad stack.
For me that means Go, where everything is async by default.
I don't think its so easy. Go goes a bit too far and makes the scheduling pre-emptive which can make targeting a specific thread (like a UI thread) harder.
I think an ideal language would need to support cooperative threading and binding to specific thread contexts.
Perhaps "Safe Rust" would be more apt (de-referencing any pointer is unsafe), though I think it's quite fine and well accepted to refer to "Safe Rust" as just "Rust".
Of course, the null pointer can still exist in Safe Rust, but since you can't de-reference it I think it's fine to say Safe Rust is "close enough" to count.
You can only dereference raw pointers from within an unsafe block so they're only useful inside unsafe blocks. IMO Unsafe Rust != Rust, unsafe is an extension to the language that is clearly separated from safe code, and using it essentially means voiding Rust's safety contract.
Not that you're incorrect but to be even more precise, and for the readers who do not know about Rust, I would say "voiding *parts* of Rust's safety contract".
Citing the documentation:
> To switch to unsafe Rust, use the unsafe keyword and then start a new block that holds the unsafe code. You can take five actions in unsafe Rust, called unsafe superpowers, that you can’t in safe Rust. [...]:
> - Dereference a raw pointer
> - Call an unsafe function or method
> - Access or modify a mutable static variable
> - Implement an unsafe trait
> - Access fields of unions
> It’s important to understand that unsafe doesn’t turn off the borrow checker or disable any other of Rust’s safety checks
I’m not even sure that captures it. You must not void the safety contract in unsafe Rust. The distinction is that with unsafe, you must manually uphold the safety contract.
Ah yes, you’re right that I missed that part. The contract isn’t voided by using unsafe, what changes is that responsibility of enforcing the contract is moved to the developer instead of the compiler.
Once had a problem where customers complained about an app keep crashing and losing minutes or hours of work. Boiled down to a "null reference" in C++. Programmer responsible argued till blue in the face that his code could not have a bug because references (&) cannot be null. Of course they can.
Rust, at least, requires that this happens in unsafe code, but for sure, a bug in unsafe code can lead to null references. We are doing noobs a disservice if we claim otherwise.
> Programmer responsible argued till blue in the face that his code could not have a bug because references (&) cannot be null. Of course they can.
It's undefined behavior merely to create a null reference in C++, whether or not it's used. Of course that doesn't mean you can't do it anyway ("int * p = NULL; int &x = * p;") but the bug would be in the code that created the null reference, not the code that used it, just as in Rust the bug would be in the unsafe code which created the null reference—Safe Rust code is allowed to assume that this situation will never occur.
(One side effect of this rule is that the compiler is allowed to assume that "&x == NULL" will always be false for any reference "x", so even if you attempt to check for a null reference the check can be optimized out.)
It was his code the created the null reference. He converted a null pointer into a reference. But doesn't matter: when presented with the evidence of a null reference, it would have been straightforward to diagnose the problem. And after repeated blustering and denials from him, that's what I had to do to get the bug fixed. We do a disservice if we tell people that references (in either language) cannot be null. They can be null, and that would be a bug in some other code - so follow the trail to find where.
Haskell doesn't have null, so Optional is the usual alternative (actually called "Maybe" in Haskell, but it's the same thing)
Haskell values can throw exceptions (e.g. for division-by-zero, etc.); but catching them (and therefore branching on them) is an IO effect.
That sort of exception is treated like an unfortunate necessity in Haskell; and user code tends to use a more structured, well-typed approach like Either (there are a few alternatives floating around in common libraries)
I think this would probably be trivial with TextMate themes (used by VSCode, Sublime, and lots of other editors). If not, certainly it’s possible with a quick tree-sitter query. The latter also presents a wildly expansive set of options for specialized static analysis (eg I built a naive TypeScript “compiler” with it in about a day).
> Javascript, of course, has async/await syntax. I’m curious if that is equivalent to for expressions/do notation and could (in theory) be used for monads other than Promise
It's very similar indeed to do-notation.
The contract for JS async/await is really simple, too, it basically supports any "Thenable" object: an object with a monadic bind function called .then(). It's basically "duck typed" in JS, if it has a .then() function that takes the right sort of callback you can await it.
I haven't seen any practical uses of async/await syntax for monads other than Promise, but it's very doable in theory.
The examples for for-comprehension looks very compelling. But it's painful in practice. It is still way too clunky compared to line-by-line imperative* code.
something(a = effectfulA(), b = effectfulB())
This would be three lines in a for-comprehension. With noisy variable names.
---
> We can even combine things, so F could be CorrelationId => Promise<*>
And then you need to litter your code with `liftF` and whatnot.
---
*You are still doing imperative programming whether you use the language's built-in flow control or use an IO monad.
small nitpick/counter example: in Haskell, you could make your example look like:
something <$> effectfulA <*> effectfulB
<$> and <> are very common in haskell code and basically second nature to any haskeller, and that's how I would personally write it (don't know if scala has equivalents).
Idris in my opinion does this even better, in Idris it would look like the following:
something !effectfulA !effectfulB -- using !-notation, or:
[| something effectfulA effectfulB |] -- using idiom brackets
the two exist separately because !-notation is more general, while idiom brackets abstract _only function application_, and they desugar to map (aka <$>) and ap (aka <>), rather than !-notation which desugars to bind (aka >>=, aka <- in do blocks)
I think given these they are roughly equivalent, with the added benefit (at least IMHO) that the side-effectful/monadic actions are very clearly marked even at a syntactic level
Scala has overloading, currying not-by-default, optional and named parameters. Some similar stuff exist*, but they interfere with those Scala features, which I value more.
77 comments
[ 4.7 ms ] story [ 140 ms ] threadI usually translate in my head to side-effect thingies. Much easier. So, Maybe<T> is short hand for it could be there, or not, you'd have to check. Same with Result<T>. Or Optional<T>. Or Future<T>. It's nicer than having null as a default value and then triggering a null pointer exception because you forgot to check but a bit less readable if you start wrapping them.
But if you have a language with nullable types, like Kotlin, you can your cake and eat it. For example, you can have functions like isNullOrBlank defined on nullable strings (String?) which don't throw a null pointer exception if you call them on a null value. Just syntactic sugar for the common use case.
Likewise, Kotlin has more syntactic sugar that functional programming types would frown upon that is actually nice to use. Like suspend functions that you can use to write asynchronous programs that almost look like they are normal synchronous ones. With proper support for cancelled co-routines, error handling, threading, reactive programming, etc. Yes, they're colored functions. But, colored functions are nice and easy to work with. My compiler will tell me off when I do it wrong.
Is it all monads under the hood or just a pragmatic language?
A vocal camp wants monads in the abstract and feels like reified monads as language constructs completely misses the point. The other camp is happy to accept new syntax and keywords to get their work done and see monads as ivory tower language enthusiasm. The choices that language designers make increasingly put their languages on one side or another of this dividing line.
In fact overly general abstractions are an anti pattern in practical software development, at least in my opinion. Any problem can be successfully extrapolated to a more general case, that doesn't mean it's worth doing it.
They say you can find monads everywhere, but doesn't that mean that by using monads as a starting point, you'll have more freedom and less structure and predictability than if you used a GoF pattern?
https://hackage.haskell.org/package/monad-control
https://hackage.haskell.org/package/lifted-base
While i usually could solve it in a different way, such things would have made it quite a bit nicer (the zoo of .map, .fold and such is a bit annoying)
Under an effect-based system:
Is like having an explicit effect F: 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:
Or: 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:
And we can even ensure that our function is generic over additional effects: 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!
Maybe you already knew about this and is still asking, though?
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.
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_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.
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?
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).
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.
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"?
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.
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.
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:
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!
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.
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.
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.
> I might write foo with an assumption that errors rollback, and bar with an assumption that errors abort. [...] These things have color we're just choosing to be blind to it!
This is more of a question of API design than something inherit to effect systems. I think it would be a good idea to use separate types for rolled-back errors and aborting errors; in the case where two functions use the same effect with different handlers, you can always mask the effect[0].
I do not think effect systems ignore color, rather, they give the end-user control over how color is manifested. Sometimes it's desirable to be blind to color.
On the other hand, I do agree that effect systems throw away layering information, much in the same way that auto-collapsing a nested Option None to None defeats the whole purpose of Option types.
Effects can be used with traditional monads, and it's possible to reify effects into monad-like objects that can be handled like values. I mean, that's what an effect handler does: it matches on the enum of effects in scope as if they were a value!
[0]: Scroll down to 3.4.7 in https://koka-lang.github.io/koka/doc/book.html#sec-combine
> but I've come to believe they're simply not an improvement over mtl-style constraints with layering expressed when we need it.
Typed tagless form is great, and (on an unrelated note) I love typed tagless final interpreters.
Although I agree that specifying layering relationships is an important component of managing effectful composition, I think the largest issue with mtl-style constraints is that the constraints require higher-kinded types by design. HKTs are really cool, but like a lot of meta-functiinal features can really drag down compilation times.
Effects are nice because they can be implemented as a single pass + cps transform, and existing control flow constructs can be re-written as sugar in terms of effects with no additional overhead (as delimited continuations do not require making a copy of the stack).
But I digress. Monads (and more generally HKTs) give you powerful tools that allow you to prove certain properties about the way effect constraints propogate through a system. I advocate for effects not because they are a replacement for monads, but because they are a nice method for reifying disparate threads of computation in a trivially composable manner.
I also don't think that all layering should be replaced with effects. I think careful layering with the occasional effect when needed is the way to go. Balance and simplicity in all things.
https://okmij.org/ftp/Computation/dynamic-binding.html#DDBin...
https://okmij.org/ftp/Computation/#Shonan-handlers
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.
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).
What about the case of needing context like “correlation id,” from the article? Can that be modeled as an effect?
In the case of needing a correlation id, this is a great use case for effects! First we declare an effect type:
Then we set up a handler: 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:
Which, using the above handler, would print: For example. Hope this helps!Before we get to the end of WCIYF, we could freely substitute in async (promises); the possibility of exceptions (Java-style checked exceptions in particular); outside-world interactions (Haskell IO); or anything else.
Of course, what we experience in Haskell and other strongly-typed functional languages is that we colour our functions all the time! Not just red and blue; but sometimes green, or yellow, or a combination of several colours at once!
Why is it so ergonomic in a language designed around this concept? What we see in JavaScript is that having the colours (effectively, the monadic wrappers) isn't enough. We also need tools for abstracting and generalising these notions, so that composition goes from being a syntactic disaster to a semantic convenience.
I've been speculating for a while that the problem with Java's checked exceptions was principally the impoverished language we had to talk about them. If we could write things like "this throws anything the argument throws, except XYZ" things... might've turned out considerably differently.
I agree! It's also what I've been seeing in i.e. Scala, where everything is converging to a single Monad. And in that case, monads are basically unnecessary. The point of them is to be able to customize your function colors.
Just use a language whose semicolon/newline semantics reflect the functionality you'd otherwise get with your "red" monad stack.
For me that means Go, where everything is async by default.
I think an ideal language would need to support cooperative threading and binding to specific thread contexts.
Well, Rust does.
Of course, the null pointer can still exist in Safe Rust, but since you can't de-reference it I think it's fine to say Safe Rust is "close enough" to count.
Citing the documentation:
> To switch to unsafe Rust, use the unsafe keyword and then start a new block that holds the unsafe code. You can take five actions in unsafe Rust, called unsafe superpowers, that you can’t in safe Rust. [...]:
> - Dereference a raw pointer
> - Call an unsafe function or method
> - Access or modify a mutable static variable
> - Implement an unsafe trait
> - Access fields of unions
> It’s important to understand that unsafe doesn’t turn off the borrow checker or disable any other of Rust’s safety checks
https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html#unsa...
Rust, at least, requires that this happens in unsafe code, but for sure, a bug in unsafe code can lead to null references. We are doing noobs a disservice if we claim otherwise.
It's undefined behavior merely to create a null reference in C++, whether or not it's used. Of course that doesn't mean you can't do it anyway ("int * p = NULL; int &x = * p;") but the bug would be in the code that created the null reference, not the code that used it, just as in Rust the bug would be in the unsafe code which created the null reference—Safe Rust code is allowed to assume that this situation will never occur.
(One side effect of this rule is that the compiler is allowed to assume that "&x == NULL" will always be false for any reference "x", so even if you attempt to check for a null reference the check can be optimized out.)
Haskell values can throw exceptions (e.g. for division-by-zero, etc.); but catching them (and therefore branching on them) is an IO effect.
That sort of exception is treated like an unfortunate necessity in Haskell; and user code tends to use a more structured, well-typed approach like Either (there are a few alternatives floating around in common libraries)
Monad is a generalization (as a type-class, which is the particular way of defining an ADT) of an type-level abstraction barrier.
It comes from untyped math which has "structural" notions, such as Monoid, and, indeed Monad could be viewed as a Monoid.
There is nothing more "deep" or "profound" in there, and the whole mass hysteria is similar to those when Java came out.
https://en.wikipedia.org/wiki/ColorForth
It's very similar indeed to do-notation.
The contract for JS async/await is really simple, too, it basically supports any "Thenable" object: an object with a monadic bind function called .then(). It's basically "duck typed" in JS, if it has a .then() function that takes the right sort of callback you can await it.
I haven't seen any practical uses of async/await syntax for monads other than Promise, but it's very doable in theory.
---
> We can even combine things, so F could be CorrelationId => Promise<*>
And then you need to litter your code with `liftF` and whatnot.
---
*You are still doing imperative programming whether you use the language's built-in flow control or use an IO monad.
* https://eed3si9n.com/learning-scalaz/Applicative.html
I know the Haskell operators, but the Idris syntax are new to me.
BTW * has to be escaped with a \.
Also thanks for letting me know about the escaping, sadly I can't edit the comment anymore
An asynchronous 1+1 sounds ridiculous.