Why are there so many libraries for algebraic effects?

Learn
42

My reasoning is more or less the same in this case as in the case of choosing between Haskell and C.

Any program you can write in Haskell, you can write in C. It will only be slightly longer and less general. But C is a much simpler language! Why do I need to go to the Haskell café? What are these programs for which it is easier, overall, to write them in pure functional style, than it is to write them in C?

You have not done half the work with StateT. I have no clue if StateT functor is even a functor when functor is. Is your fish associative? What about the other identity? Can you derive bind from fish? I trust you can do all this. But I am already partying, and you are still washing the dishes.

Maybe you could also prove the corresponding stuff for StoreT along the way. I get it by duality for free. Twice the amount of proof per line of thought!

There are no monads for which it will be easier for you to prove that they are monads by exhibiting them as adjunctions, than it will be to prove that they are monads directly — because you refuse to even try.

As fun as it may be, promoting adjunctions is not really my goal in this conversation. Allow me to get back to the question of IO, in the next message.

1 Like
43

I’m willing to try if you could name one possible candidate other than StateT!

1 Like
44

I already have, or rather Jack and Edward, just above. Here is an adjunction between endofunctors: Free (e ×) ⊣ Cofree (e →). These functors can be defined concretely if you like, and a monad transformer can be constructed out of them. By duality, there must also be a corresponding comonad transformer, though I have no idea what it should look like.

45

OK, so the monad in question is

Cofree (e ->) (Free (e,)) a

What is this? A type of e-ary branching trees with sequences of e followed by a at the branches?

I agree with you! I would much rather prove that to be a monad via abstract nonsense than by hand. In fact I can’t even imagine what the bind operation must be.

But I have never come across such a monad in practice, and never wanted to use something isomorphic to it in an effect system (unless I am very much mistaken). So have adjunctions now helped me with effect systems? I don’t think so.

1 Like
46

You said you are willing to try if I could name one possible candidate. I have named one possible candidate. Назвался груздем — полезай в кузов!

47

I just tried it. Turns out it involved zero work, because it was already expressed as adjunction. You were right! Still, I don’t see the relevance to effect systems.

Here is my current working hypothesis:

The only monad arising from a Hask-Hask adjunction that is relevant to effect systems is State/StateT. If my hypothesis is true it suggests that the relevance of adjunctions to effect systems is minimal, and they only overlap by coincidence.

EDIT: Let me try to explain why I’m not impressed by adjunctions by contrasting with a notion from category theory that I am impressed by, when it comes to effect systems: free monads. Free monads are a very nice model of effects that allows you to build effectful computations out of primitives, such as

data StateF s a = Get (s -> a) | Put s a
  deriving Functor

type StateT s m a = FreeT (StateF s) m a

get :: Monad m => StateT s m s
get = liftF (Get id)

put :: Monad m => s -> StateT s m ()
put s = liftF (Put s ())

StateT is automatically a monad! Then I can define interpreters/handlers for StateT into another monad, I can combine effects by nesting FreeTs, but this is also isomorphic, I believe, to taking FreeT of the sum of the effect functors. In general, most of what one wants from “effects” is encapsulated in this notion! It’s not an efficient encoding of effects, but it is highly pedagogical and actually fairly useful in cases when efficiency is not a main concern.

If adjunctions could approach anywhere near this utility, then I would be convinced that they are useful for effect systems.

49

It’s a pretty dense conversation, but here’s a back and forth between the authors about the differences Advantages over effectful · Issue #2 · re-xyr/cleff · GitHub

1 Like
50

This is somehow symptomatic for this whole thread (and category theory, if you will).

There is only one set of real numbers up to isomorphisms, but that does not mean that these sets are all pairwise equal. While they are equal when talking about “actual numbers” (let’s not discuss that definition ;), the set of points on a pencil line on a sheet of paper are not equal to “actual numbers”. Yes, paper isn’t infinite - either use a roll of toilet paper or fold it into a Möbius band as an approximation - and points drawn with a pencil are not infinitely small, as the tip of the pencil isn’t - that’s why a positive number of angels can dance on it.

If that (the not-equality of pencil drawn points and “numbers”) is too handwavey for you, we can take a look at the natural numbers and apples, oranges, Haskell users and chairs. They are all isomorphic to (a finite subset of) the natural numbers and there are many occasions when treating them as natural numbers is perfectly fine, but there are also many examples where it actually matters if we are talking about apples, oranges, Haskell users or chairs.

6 Likes
51

To be clear, I have no doubt you know about free monads and how to use them. I explained them by way of example of a categorical notion that I do find useful in the context of effects.

I apologise if my contributions to this thread have come across as demonstrating a lack of trust in you. That was not my intention. I am not interested in continuing a discussion where my comments are being interpreted in that morally-loaded way.

7 Likes
52

Let’s take for granted there is some Platonic realm of real numbers, or that we’re only looking at one of these sets. I’m still missing how that determines how many different methods there should be to solving that problem.

The problem statement is still unclear to me. The reason people create computer programs is larger than simply finding some optimal means of calculating a result. A library that trades off performance for ergonomics, or for error reporting or some other reason seems perfectly understandable to me.

As a practical matter, getting someone to understand how to be productive with a library is important, and if two libraries that solve the same problem cater to two different audiences that’s sufficient for both to continue existing.

Stated simply: why shouldn’t there be so many libraries for algebraic effects?

2 Likes
53

I’d say, there is also a possibility that categorical notion is not working well in terms of formulating (useful) effects.

If you consider the origin of category theory like algebraic topology, one can see that the objects are not nice there. For instance, CW complexes are not smooth, or even differentiable. They can also be disconnected. All nice properties they share is that, you have attached cells to construct one. If you go further to topological spaces, all bets are off - you have funky stuff like Hawaiian earrings.

In contrast, the flip side of “dumb object” is that the categories are nice. The category of topological spaces admit products, coproducts, and even all the small limits and colimits. I do not recall category of CW complexes, but they are still quite nice IIRC.

On the opposite side lies the differential geometry, study of smooth manifolds. The smooth manifolds are smooth, and locally alike a part of R^n. All the nice objects like spheres or projective spaces are smooth manifolds, and you can do a rich analysis on them - like, analyzing how a smooth map behaves around a point. Meanwhile, category of smooth manifolds is a famous example of ill-behaved category. Just to categorically define what an surjective submersion is, you need to pull “regular epimorphism”, whatever that means. Now with non-surjective submersion? I dunno if there is a way to avoid tangent bundle and details like this.

Now, you can see the reason category theory is developed from algebraic topology, not differential geometry. The notion of category suits there very well, since the objects are relatively simple.

Now, let’s get back to the notion of effects. Indeed, there are various kinds of effects, but they come with varying degree of utility. If you consider the most prominent ones like State, Reader, and Writer, they come with certain nicety (that admittedly I do not know well). Also with IO, you can “analyze” the structure and deduce new properties - this is my impression of @tomjaguarpaw 's post, could be wrong. What if the nice effects are like differential manifolds, so that you’d rather take an analytic appraoch?

1 Like
54

That’s what I tried to convey with my above post. But I’ve spent way more time doing differential geometry than category theory (or topology), so I guess I’m biased :smile:

55

Let me respond as the author of the heftia effect library.

First of all, in the Haskell effect library community, performance is treated as very important. This is because the focus is more on practical usability than academic soundness. This was not always the case, but seems to have become the trend over the past few years. I only joined the community recently, so I do not know much about how things were before.

I am a complete beginner when it comes to category theory, and I do not know anything about adjunctions. That said, I tend to have an academic mindset, so to be honest, I have some doubts about the current state of the community, where performance is emphasized so heavily that semantic correctness is often treated as secondary.

This concern is exactly what led to the design philosophy behind heftia. It avoids depending on the IO monad, and takes a synthetic approach like transformers. I believe that, using equational reasoning, it should be possible to show that it is strictly equivalent to the formulations in the (higher-order version of) algebraic effects literature.

By the way, it seems like the topic of higher-order effects has not been mentioned yet in this discussion. The issue of how higher-order effects interact with continuations is an important factor when thinking about why so many different libraries exist.

I am not very familiar with the analytic libraries (eff, effectful, bluefin, cleff, etc), so I would like to talk mainly about the synthetic ones (mtl, fused-effects, polysemy, freer-simple, etc). I admit that my understanding may be biased as the author of heftia. As far as I know, the first libraries to encounter this problem were fused-effects and polysemy. When effects like coroutines or nondeterministic computations were combined with higher-order effects (scoped operators), they sometimes produced unexpected behavior. Later (or possibly at the same time), it was found that freer-simple did not have this issue. This led to the understanding that algebraic effects can be implemented correctly in Haskell as long as higher-order effects are not supported.

Note that the original papers on algebraic effects do not include higher-order effects. However, the community came to believe that higher-order effects are essential in practice, and wanted to support them.

So if I had to give a final answer, I would say that freer-simple is the only library that strictly implements the original definition of algebraic effects from the literature. All other libraries are variants that introduce extensions for practical use or restrictions for performance reasons.

To the community, if any part of my understanding of the history is incorrect, please feel free to correct me. I was not part of the community at that time.

I forgot to mention, besides freer-simple, there is also mpeff as a library equivalent to algebraic effects. Since it is an analytic implementation, it cannot be proven sound by equational reasoning. However, it is based on papers related to the Koka language.

8 Likes
56

To begin with, there are three named classes of interpretations assigned to algebraic effect operations (as far as I know). Showing their inclusion relationships at the same time, they are: tail resumptions ⊂ scoped resumptions ⊂ non-scoped resumptions. cf. Effect handlers, evidently
These concepts are likely unambiguous, so it should be possible to translate them into category-theoretic terms.

  • The evidence‑passing (ReaderT IO) style libraries in the bluefin/effectful families speed things up, from the point of view of algebraic effects, by restricting interpretations to only the tail resumption class, and they extend that to higher‑order effects. Because this is an analytic implementation, you cannot prove soundness by equational reasoning, and proving any kind of isomorphism between them is about as difficult as formal verification for C code.

  • polysemy/fused‑effects has a synthetic implementation, but what it encodes is probably a theory different from algebraic effects (what used to be called Scoped effects & handlers or Weaving. cf. A framework for higher-order effects & handlers). Again, please note that these have been extended to higher‑order effects. Algebraic effects itself does not have higher-order effects. At least from the perspective of algebraic effects, these can only be encoded correctly up to scoped resumption. This is why coroutine effects do not work properly. As for polysemy, due to a hack in its implementation, it can probably only encode up to tail resumption (which explains why non-determinism effects do not work).

  • Those that support up to non‑scoped resumption - that is, that fully realize algebraic effects - are, as far as I know, eff, mpeff, heftia, and freer‑simple; I also believe there are several implementations in the form of an freer/operational monad.

    • The first two are analytic implementations, so there is no obvious isomorphism. Their internals include an analytic Haskell implementation of the prompt/control primitives (the multi‑prompt monad) and the IO monad (GHC primitives).

    • The others are synthetic, and except for heftia they should all be encodings isomorphic to the free(r) monad. Only heftia encodes the higher‑order freer monad from the paper “A framework for higher‑order effects & handlers.”

    Among these, only mpeff and the freer-simple/operational series are fully functionally equivalent to algebraic effects. All others are extensions that support higher-order effects.

11 Likes
57

I am, for one, sold into the approach of heftia. Thanks for the write up!

But I am going to be the one ask the silly question too: what are the definitions of analytical and synthetic effects?

1 Like
58

See the end of Tom’s comment up-thread for that.

1 Like
59

I couldn’t find it in GitHub - yallop/effects-bibliography: A collaborative bibliography of work related to the theory and practice of computational effects. I think you should add it!

2 Likes
60

Yes, I basically tried to interpret the meaning based on what Tom said and the discussion that followed, but of course there may be some misunderstandings.

In my view, if we were to give a renewed definition of synthetic/analytic, or external/internal, as discussed so far, it would be that first we have some mathematical object, and encoding it using Haskell’s algebraic data types, and from that the implementation is determined automatically, then the approach is the former. Everything else is the latter. The former is always uniquely determined up to isomorphisms in data types and implementations as defined by the underlying theory. The latter is not.

Thank you! I’ve created a PR.

2 Likes