Why are there so many libraries for algebraic effects?

Learn
21

do drop me a line if I can be of any help with anything

I appreciate this!

Overall, you, and some other people in this conversation, pay a lot of attention to particular things like whether a state monad is strict and whether an effect system is efficient, while entirely ignoring other things like whether a state monad arises from an adjunction as I mentioned and whether an effect system encodes a free model of an algebraic theory. This is a backwards way of thinking. As if we were trying to decide how many angels can dance on the tip of a pin without ever having agreed what an angel is. This is exactly what I uncharitably called out in my first message:

a case of computer programmers ruining something beautiful out of ignorance

I am sad to see this suspicion confirmed. If the brightest minds of Haskell (I count you here, Tom) cannot tell me in simple words what they have been talking about all this time, then we are in big trouble.

Earlier today I also looked at the documentation of effectful that you have linked, and now I am not sure whether Andrzej is genuinely missing the point of the monad transformers in question or intentionally spinning the discourse in his own favour. Monad transformers implement certain specific categorial constructions — and, as far as I know, they behave exactly as one would expect having understood their categorial specification. No one has the authority to say that they are «incorrect», «confusing» or «even worse» based on their own unchecked expectations.

The state monad transformer arises from the curry–uncurry adjunction

I’ve never found this a useful way of thinking. What non-trivial conclusion have you obtained from that knowledge?

That StateT monad is a monad insofar as monad is, to begin with. This is more than I can say about this Eff thing you displayed. If it does not implement free models of algebraic theories, then how can I know if it is a monad? It looks to me like it could be a chunk of a device driver out of the Linux kernel.

No, effect systems that are IO wrappers (Bluefin, effectful, ReaderT IO, etc.) can only deal with effects that have at most a single continuation. Most effects have a single continuation, exceptions have zero. Therefore IO wrapper effect systems cannot handle the style of “non-determinism” as seen in LogicT.

Now we are getting somewhere. So, effects are things that have zero or one continuation each. Can you explain in simple yet precise language what it means for an effect to have zero, one or two continuations? Without displaying any more device drivers?

Transformers are “synthetic”. They build “effects” from language primitives and allow you to compose them. For example, StateT s (ExceptT e (Reader r)) a is an algebraic data type, just formed from the language primitives sums, products and exponentials.

By contrast, Bluefin and effectful are “analytic”. They are simply IO underneath.

I think better words may be «external» and «internal». The «external» or in your language «synthetic» are those that rely on the denotation of Haskell, and the «internal» or in your language «analytic» are those that rely on the operation of GHC. Is this agreeable?

What about the «freer monads, more extensible effects» thing? What kind of effect system is it in this classification?

This classification does clarify something.

My understanding is now that people gave up on trying to make synthetic effect systems asymptotically efficient, and instead started to move them into GHC. So, first we had external (synthetic) effect systems, and then we started to build internal (analytic) ones.

I do not understand any of the details here, however. Is it true that external (synthetic) effect systems are necessarily asymptotically less efficient than an «ideal» effect system?

I faintly recall Alexander @graninas writing somewhere that the problems of efficiency are solved by using continuation passing style, and this sounded plausible to me at the time, but I cannot right now recall any details… Is this what Armando @Ambrose had in mind when he said «new ideas with continuations» above?

1 Like
22

I am sympathetic with this viewpoint, but I think you must also admit that this is extremely hard to do for all but the simplest concepts. Even explaining what monads are is hard. Also, you might think that “the state monad arises from an adjunction” are simple words, but I think 99% of the people on this forum would disagree.

That said, I agree that programmers are a bit too quick to throw out all of the theory; for example, it seems hardly anyone in the last 10 (or even 20) years has looked at effect laws. In fact, I have never really understood what effect handlers really are. They seem more like a metatheoretical concept, but they are mixed in with the object programs.

If you want to learn more about effect systems from a theoretical point of view then perhaps this paper is a good starting point:

There is a paper about handlers, but I don’t really understand it yet (even after studying this for 3 years as part of my PhD):

11 Likes
23

Right, whether a state monad is strict or an effect system is efficient are questions of direct practical importance to me. I do not see any practical relevance of whether a state monad arises from an adjunction or an effect system encodes a free model of an algebraic theory. Regarding the former, all monads arise from adjunctions, and regarding the latter, I don’t even know what it means!

I value theory, but I don’t see any connection between the sorts of theory you are espousing and practice (that’s not to say they don’t exist).

Well, feel free to try to continue to persuade me it’s backwards, but so far I don’t see the point of discussing angels on a pin, regardless of what angels are! I admit to my ignorance though: although I’m not ignorant of what an adjunction is, I am ignorant of why I should care about them when programming in Haskell.

But you didn’t need to know that curry-uncurry was an adjunction to conclude that StateT s monad is a monad when monad is. You can just obtain that result directly. Regarding Eff (from Bluefin or effectful), it’s a monad in consequence of IO being a monad (since both are wrappers around IO). Why is IO a monad? Well, that’s something you have to prove by reference to the definition of IO. An error in its implementation could make it fail to be a monad! This is a facet of the analytic approach. You make something, and then you have to analyse it to see if it’s the thing you wanted. It’s not the thing you wanted by construction, as would be if you had used the synthetic approach.

(However, what you then synthesise on top of something analytic is again correct by construction.)

No, the effects that Bluefin and effectful support all have zero or one continuation, or I should rather say, all run their continuation at most one time. And no, I can’t explain in any language, let alone simple or precise, what that means. Perhaps it could be done with reference to a specific reference language and evaluation model, but not by me.

Roughly, but I don’t know why you draw a distinction between the “denotation of Haskell” and “the operation of GHC”. IO is a part of Haskell, after all.

Assuming you mean Eff from the freer package, synthetic. It is built up from ADTs, i.e. small axiomatic pieces.

I’m not sure about “people”, by @arybczak noticed that the analytic approach was possible and a couple of people, including me, followed that approach. As far as I know, Polysemy is still widely used, so I don’t think people have given up on the synthetic.

I wouldn’t say they’ve been “moved into GHC”. They’re libraries.

Yes, that is the correct historical order, with the caveat that IO and ST are both “analytic” (IO trivially so), and they both came before anything that we currently recognise as a synthetic effect system.

It sounds implausible to me.

I doubt it. I suspect @Ambrose meant effect systems that use delimited continuation primops under the hood: GHC.Prim

Finally, having explained that I find some forms of theory not to be useful, here is a form of theory I do find useful: equational reasoning. Bluefin satisfies a variety of systems of equations such as

do { x <- get s; put s (f x) } == modify s f 

do { x1 <- get s; x2 <- get s; pure (x1, x2)
  == do { x <- get s; pure (x, x) }

Ultimately, I think it can be shown that those can be derived from these foundational properties:

do
  (r1, s1) <- runState s0 $ \s -> body1
  runState s1 $ body2
  ==
do
  runState 0 $ \s -> do { r1 <- body1; body2 r1 }
-- where `s` may occur free in `body1` and `body2`

runState s get == pure (s, s)

runState s (flip put s') = pure ((), s')

runState s (flip modify f) = pure ((), f s)

This is not a Bluefin innovation! All systems off effects with state satisfy something like this. It’s essentially a defining property of state. But it is a sort of theory I find useful. In particular it shows that the analytic approach of Bluefin is equivalent to the synthetic approach of transformers or free monads, in terms of the results they calculate.

[EDIT: Some handles corrections thanks to @jaror]

10 Likes
25

I can assume that you have much stronger equational reasoning skills than me. As for me, I always try to avoid doing any work.

I once tried to prove that Either, State and our other friends from the standard libraries are monads, from first principles, and I recall I could hardly succeed. It takes some careful and tedious paperwork!

Meanwhile, having once proven some easy facts about adjunctions, you can conclude that StateT is a monad transformer merely by looking at its definition, which is StateT s m ≔ x → m (s × y). This is a composite functor of shape T ∘ M ∘ S where M is a monad and S ⊣ T is an adjunction. It follows in one step that we have a monad transformer here. This is way faster and easier than having to state the laws literally (perhaps using chunks of Haskell code as notation) and then to simplify and manipulate them until you (hopefully eventually) get literal equality of terms.

I am not sure why you do not appreciate this ease. With the right kind of theory you could get the same results with less effort. I do not practice recreational or academic mathematics — only the kind that lets me do less work.

… I do not see any practical relevance of whether a state monad arises from an adjunction … all monads arise from adjunctions …

What is special here is that the state monad arises from an adjunction of two endofunctors — in this case the adjunction is given to us concretely as curry and uncurry. This is rare. We can routinely derive the concrete definition of the state monad transformer, along with the proof that it is, indeed, a monad transformer.

You do not not see the relevance of my methods, alright. But I hope you see that I can explain my stuff to you in simple language, at any level of detail and precision. If you want to help me understand your stuff, maybe the same methods would work?

While I generally want to agree with everything you say, it is hard for me to agree with some of the things you said right now.

Regarding Eff (from Bluefin or effectful), it’s a monad in consequence of IO being a monad (since both are wrappers around IO).

I believe that anything of form x → m y is a monad, insofar as m is, in the absence of undefined behaviour. But the chunk of a device driver you have shown me in your previous message does not inspire confidence. What is this SmallMutableArray RealWorld Any thing? What kind of equational reasoning can take me from SmallMutableArray RealWorld Any to a proof of the monad laws for this intricate mechanism?

  • Something being «mutable» means there is no referential transparency.
  • Something being an «array» means there can be memory access errors.
  • Something being an «any» type… I cannot even say what that means. Does not mean nothing good.

To prove anything about such an intricate thing would take a lot of, as you call it, analysis — and you will need to formalize the operation of your compiler along the way.

By the way, this is why I am drawing a distinction between denotational Haskell and operational GHC. Does any Haskell Report define SmallMutableArray, RealWorld and Any, to begin with?

Why is IO a monad? Well, that’s something you have to prove by reference to the definition of IO.

I am not sure about this. Whatever x you choose, IO x does not have equality internal to Haskell. Without equality, we cannot put forward any equations. It is truly murky for me if IO is a monad, and if so, in what sense. The only approach I am aware of is to construct a pure model that looks believable and then talk about that model instead of the real thing.

Contrast this with StateT. I know that, if IO is a monad under some notion of equality, then StateT state IO is also a monad under that notion of equality. StateT cannot make things worse. About Eff of internal (analytic) effect systems, I have no way to be sure!

Returning to state. It is encouraging to see that there are some equations on offer. After some guesswork I figure that the types of the names you are using should be looked up in Bluefin.State. And, as with IO, I am stupefied: what is the equality of terms of type Eff es a? All the equations you showed are between terms of this type. When you say «Bluefin satisfies equations», what do you mean? And if you do not mean anything specific, then how is this a useful theory?

There is no such question with the «traditional» definition of state from transformers — I can test them with QuickCheck, or I can use denotational semantics to convert terms to functions and prove equality pointwise, or I can write them as λ terms and evaluate them… What can I do with Eff?

2 Likes
26

I don’t want to speak for Tom, but I simply didn’t know there was a theorem saying that a composition of adjunctions with a monad in the middle is also a monad.

1 Like
27

It is also a breeze to show. Not like the stuff they make real engineers learn. Lebesgue integral… shivers Maxwell equations…

28

I appreciate all the ongoing discussions, and I believe they contain lots of useful information that many are learning from on the sidelines.

I don’t have theoretical bits to add to the discussion, but as far as the original question goes, may I zoom out and ask: Why not? It’s no different than asking why there are so many brands of cheese if the science of how cheese is made is no longer a mystery. It’s a “free market” of ideas, everyone has their comfort level of learning, aesthetic taste of syntax, ergonomic, performance etc. libraries provide to us. We may try to standardize and make some recommendations canonical into the core library, but even there, we can create the situation of “rebase” and “rerebase”.

If this analogy holds, then the one asking others to please his particular aesthetic taste may bear the burden of proof, instead.

Here goes my digression on aesthetic considerations. Feel free to ignore and continue the good theoretical discussion.

4 Likes
29

It’s more than that though. If we look at a few concrete examples, every effect systems has a very reasonable reason for its existence.
In roughly chronological order (probably):

  • mtl started off as an early generalization of monad transformers. The O(n^2) instances problem massively limits the number of possible effects and handlers are non-commutative in really subtle ways. It’s also quite slow when used as an effect system. It is pretty simple, quite popular across the ecosystem and very easy to integrate with for libraries though!
  • Various free monad libraries tried to fix those issues, but naive free monads can lead to quadratic code so they weren’t widely used.
  • freer fixed the asymptotics but still has pretty bad constants.
  • freer-simple (presumably) simplified the API of freer but inherited the performance issues
  • polysemy tried (and failed) to avoid the performance issues inherent to free(r) monads by aggressively specializing and removing intermediate structures at compile time. IIRC it’s also more powerful wrt. higher order/scoped effects but I don’t know the details.
  • eff is the first library that is actually performant and it achieves this by implementing effects the way the rest of the world does it: delimited continuations! (with very efficient ghc primops) Progress seems to have stalled though and the Github repo hasn’t been updated in 5 years (wow that made me feel old)
  • effectful is the first efficient non-experimental effect system library because it limits effects to single shot tail-resumptive handlers and can therefore be implemented in terms of (essentially) ReaderT IO. This does mean that it is much more limited than e.g. polysemy because it cannot express reentrant effects like NonDet or Cont. However, in practice these aren’t actually all that useful (and existing implementations have their own issues) so effectful is typically more than enough. It also has a nice motivation section that you’ll probably like.
  • bluefin is based on the same implementation strategy as effectful with the same strengths and limitations, but provides a different API based on term-level handlers that especially simplifies uses of multiple instances of the same effect, at the cost of some verbosity. It also has a nice motivation section!

All of these effect sytems had a justification for existing at some point. Today, I really couldn’t recommend freer(-simple) anymore, but at least effectful, bluefin, polysemy and MTL all have pros and cons with no unambiguous winner (although one should probably use effectful or bluefin where possible)

29 Likes
30

Although you missed cleff, this is about where I landed too. effectful and bluefin seem to make the tradeoffs that I like, and then it comes down to choosing whether you want the typeclass machinery or to explicitly pass handles.

With a “library author” hat on, I feel that effect system selection is generally the application developer’s responsibility. When building a library, I like to provide bare functions that return results in IO, or at most MonadIO m, MonadResource m or (rarely, if absolutely required) MonadUnliftIO m. Defining the effects to integrate functions like these with the effect system isn’t too bad (and can be open-sourced as an independent package). If you’re not doing tricky control flow, @ocharles also has a good idiom for defining a typeclass that works well with transformers as well as other effect systems.

Anti-examples include persistent (whose typeclass functions must work for any MonadIO) and katip (whose Katip m class has MonadIO m as superclass). This is an easy and reasonable-looking design decision to make by accident; it’s not obvious why you shouldn’t include the MonadIO until you start wanting to substitute out that layer of your program through an effect system.

4 Likes
31

A very useful review; thank you!

4 Likes
32

missed cleff

So where does cleff fit into this?

33

If we look at a few concrete examples, every effect systems has a very reasonable reason for its existence.

…(reasonable reasons elided)…

Thank you, this is more or less what I wanted to know.

All of these effect sytems had a justification for existing at some point. Today, I really couldn’t recommend freer(-simple) anymore, but at least effectful, bluefin, polysemy and MTL all have pros and cons with no unambiguous winner (although one should probably use effectful or bluefin where possible)

Why could you not recommend freer anymore?

34

I appreciate all the ongoing discussions, and I believe they contain lots of useful information that many are learning from on the sidelines.

That would be a welcome side effect… ha ha.

I don’t have theoretical bits to add to the discussion, but as far as the original question goes, may I zoom out and ask: Why not?

Syntactically, it would then read «why are there not so many libraries for algebraic effects». And this would be starting from the wrong assumption. We all seem to agree that there are rather many than few.

I infer you meant to ask something else. Like, «why is it surprising that there are many libraries for algebraic effects». And this is a fair question.

Answer 1:

There are many cheeses, but there is only one milk. You can object that there are many types of milk: cow milk, goat milk, bird milk… But for every milk, there is a reason. Metaphorically speaking, cheeses are applications, and milk is the library.

Humans also tend to converge to things. For instance, they tend to live in cities, and each city tends to have exactly 1 central post station, positioned more or less in the city center. There is also only one Internet.

In this light, it is very surprising that we should have many libraries that all serve the same purpose, and it is expectable to be curious as to how they differ from one another.

Answer 2:

There are different grades of distinction. For example:

  • You can say that a particular version of a library built with a particular compiler for a particular architecture with a particular set of flags is a different library. This is what Nix does.
  • You can say that there is only one totally ordered complete field. Be it Dedekind cuts or Cauchy sequences or more baroque definitions, they are all classical real numbers. This is what Walter Rudin does.

How could it be that there is only one set of real numbers? This phenomenon is rather common in Mathematics. And this is why I keep saying that there is only one state monad transformer. The coöperating reader will have no trouble understanding what grade of distinction I wish to focus the conversation around. As we saw, there are many ways to assign strictness to a list type, so there are very many different list types — and yet, there is only one free monoid. This corresponds to the way humans construct programs: first it should do the right thing, and only later should it be efficient.

In this light, it is very surprising that we should have many libraries that implement the same mathematical concept, and it is expectable to be curious as to how they differ from one another.

35

A general observation here, again:

I sense two strains of reductionist tendency from what you said:

1) Reduce to: one purpose, one library

it is very surprising that we should have many libraries that all serve the same purpose, and it is expectable to be curious as to how they differ from one another.

So, that is a view that if it is one purpose it should just have one library. The word “should” perhaps conveys the idea that, teleologically, from global human-resource efficiency perspective, we strive for only ONE library that rules them all.

This one seems easy to challenge, maybe you could prove that we all agree on the substance of that one single purpose, first?

2) Reduce to: one mathematics concept, one library

In this light, it is very surprising that we should have many libraries that implement the same mathematical concept

I admit I myself struggle with this one. I understand the appeal of that, but I also observe that sometimes mathematics can provide different levels of abstractions depending on the context.

What I want say to that is: The fact that sometimes we model computation abstract from machine details is a choice, not necessarily a merit in all cases. That’s where I think the effect library differences in performance arise.

But, I leave it as a more debatable point for others to chime in.

36

Perhaps. But as I’ll show below, your approach involves hard work!

Really? Here’s a proof of the right-identity law for StateT:

stateFish ::
  Monad m =>
  (a0 -> s -> m (s, a1)) ->
  (a1 -> s -> m (s, a2)) ->
  (a0 -> s -> m (s, a2))
f1 `stateFish` f2 = \a0 s0 -> do
  (s1, a1) <- f1 a0 s0
  f2 a1 s1

stateReturn :: Monad m => a -> s -> m (s, a)
stateReturn a s = return (s, a)

{-
  g `stateFish` stateReturn

  \a0 s0 -> do
     (s1, a1) <- g a0 s0
     stateReturn a1 s1

  \a0 s0 -> do
     (s1, a1) <- g a0 s0
     return (s1, a1)

  \a0 s0 -> do
     s1_a1 <- g a0 s0
     return s1_a1

  \a0 s0 -> g a0 s0

  g

-}

I’m not convinced by “easy”. Here’s my attempt to define monad operations for monads arising from adjunctions, and prove the right-identity law:

import Data.Functor.Compose (Compose(..))

class (Functor f, Functor g) => Adjoint f g where
     counit :: f (g a) -> a
     unit   :: a -> g (f a)

adjointReturn :: Adjoint f1 f2 => a -> Compose f2 f1 a
adjointReturn = Compose . unit

adjointFish ::
  (Adjoint f1 f2) =>
     (t -> Compose f2 f1 a1)
     -> (a1 -> Compose f2 f1 a2) -> t -> Compose f2 f1 a2
g `adjointFish` f  =
  Compose . fmap counit . (fmap . fmap) (getCompose . f) . getCompose . g

{-

  g `adjointFish` adjointReturn

  Compose . fmap counit . (fmap . fmap) (getCompose . f) . getCompose . g

  Compose . fmap counit . (fmap . fmap) (getCompose . Compose . unit) . getCompose . g

  Compose . fmap counit . (fmap . fmap) unit . getCompose . g

  Compose . fmap (counit . fmap unit) . getCompose . g

  Compose . fmap id . getCompose . g

  Compose . id . getCompose . g

  Compose . getCompose . g

  g

-}

This relies on the following being id, which I assume is a consequence of parametricity, but my parametricity skills are worse than my equational reasoning ones. How are yours?

counit_fmap_unit :: forall f g a. (Adjoint f g) => f a -> f a
counit_fmap_unit = counit @f @g . fmap (unit @f @g)

What do we get in return for this work? We get that StateT is a monad. Anything else? Possibly not! I’m not sure there is any other monad used in practice that arises from an adjunction between Hask and Hask. Is there? If not then we have dived deep into a general theory to discover we can only apply it in one specific instance.

I’m not sure I’d call this use of adjunctions “simple”! But taking you at face value, what of “my stuff” would you like explained at an equivalent level?

I don’t understand. You already said you believe anything of the form x -> m y is a monad when m is (it’s ReaderT in fact). Parametricity guarantees that no property of the device driver is relevant, because it’s all part of x. The behaviour of the device driver is relevant for other properties of Eff indeed, such as the correctness of runState, but not to the correctness of the Monad instance.

But this its why I prefer Bluefin to effectful: there is no such device driver, just an IO wrapper.

This is tangential, but I’m not sure what you mean by “referential transparency” then, because by my definition Haskell upholds referential transparency even in the presence of mutability. That’s essentially the purpose of IO.

I think this is too pessimistic. Imagine this conversation between two colleagues:

  • A: “Did you refector that IO-heavy code yesterday?”
  • B: “Yeah, it’s a lot clearer now, but it does the same thing”

So we do have an informal notion of what “same” means for IO.

Furthermore, I’m not convinced we do truly have a formal equality internal to Haskell in the sense you expect. For example, suppose I want to show that Either e is a monad, and I have deduced one of the required properties return x >=> f == f x. What does == mean there? It can’t be from Either e’s Eq instance, because we don’t have the necessary Eq constraints. For example, what have we shown when we show the “equality” of two terms of type Either (Int -> Bool) (forall a. a -> (a, a))? I guess we can say "oh, when we apply any possible Intas an argument, and when we apply any possible type a as an argument, and then recursively follow the same process to eliminate all arrows appearing in a then we get something that satisfyies the Eq instance’s equality. OK, but that’s an appeal to a process that happens outside the language. We can’t hope to verify that equality within the language as it requires infinite work.

Then suppose we did boil it down to the Eq instance, a == b. That’s a Bool. How can I observe that Bool to check that it is True? I can feed it to a function, but what does that function do with it? Ultimately it returns another value that I can’t observe either. The only way I can observe is to run something of type IO, such as print (a == b).

Suppose we run that print (a == b) and get True printed to the console. Are we happy that our equality check was satisfied? I am, but that depends on having at least some notion of equality of IO operations, so I can convince myself that print False is distinct from print True.

So I don’t think a notion of equality of IO is avoidable.

But even if you want to avoid IO as much as possible, that’s fine in Bluefin and effectful. You can use runPureEff on any Bluefin or effectful computation to obtain value that refers to IO in no way, and compare it for equality to another value in your favourite way.

I’m not saying I have plugged every conceivable hole in my explanation here, but I hope you can see that there is no lack of attention to detail in the semantics of these sorts of effect systems.

I mean when I substitute something on one side of == with the thing on the other side, my program behaves in the same way. You may say that’s not very satisfying and is in fact begging the question, but every day programmers are doing this with IO without problem, so this informal notion does work in practice!

Sure, ultimately I can do exactly the same with terms of type IO or Eff. I can define IO as some very large equational theory and then proceed to reason equationally about them, or in some semantics. It’s a very large theory! But that’s actually part of the point of effect systems that are IO wrappers: to carve out the space of things whose behaviour we understand well (state, exceptions, streams, reader, writer) from general IO.

If you want to take this kind of approach, you might like to say “there is only one ‘exception’ effect”, ‘there is only one ‘state’ effect’", yet accept that there are many ways of encoding them, like there are many ways of encoding a complete ordered field in ZF. Furthermore, there are many ways of combining those effects, just like R^2 and C are two distinct ways of combining two copies of R.

1 Like
37

I don’t recall. There are good contrasts between cleff and effectful written by at least one of their authors, available through a web search.

Looking at the instances in package adjunctions, I see three flavours of instance:

  1. Trivial things like instance Adjunction Identity Identity;
  2. The curry/uncurry instance: instance Adjunction ((,) e) ((->) e); and
  3. Instance that lift an existing adjunction through other structures, e.g., instance Adjunction f u => Adjunction (Free f) (Cofree u)

This is not a disproof that more interesting adjunctions exist, but it certainly wiggles its eyebrows in that direction.

38

I recalled this video. I need a re-watch to see if it’s relevant to the conversation here.

39

The amount of adjunctions on offer is not really important because the logic of Tom’s post is flawed, as I shall shortly elucidate. However…

I do not recall anything in particular about this package, but from what you just said it follows in one step that there is an adjunction between Free (e ×) and Cofree (e →). (Please allow me this more pleasant notation for tuple and function type constructors.) What are these?

  • A term of type Free (e ×) A is a list of e with the tip A.
  • A term of type Cofree (e →) B is a tree with B at branches, with cardinality (e) smaller trees at each branch.

So, there must be a one to one correspondence between functions from these lists and functions to these trees. This seems to me rather unusual. We can think of Free (e ×) A as a trace of a state machine with initial state A and events e… And we can think of Cofree (e →) B as a kind of a Kripke structure or something such? So, theorem: interpretations of traces correspond to unfoldings of possible worlds.

Would you call this a triviality?

40

I am very glad that you are moved to write such a substantial message! I am not sure I can give it the attention it deserves right now. But there is a flaw in your reasoning that I shall now point out.

When I said that the state transformer is defined by a rare adjunction — an adjunction of endofunctors — I did not mean that the theory of adjunctions only applies to these rare cases. What I meant is that the state transformer is defined simply and uniquely. There are many other adjunctions you can implement in Haskell. There are only few if you insist on limiting yourself to the standard classes, which are only defined for one particular category. This limitation has already been developed into the state of a fine smoothie by people like Mike Izbicki (see subhask) and Iceland Jack (see FunctorOf) (and surely many others whom I do not right now recall), so I assume you are aware of the idea.

Of course, it would be hard for one to explore the variety of possible adjunctions if one were to dismiss the theory from the outset.

  • To start somewhere, for any given monad there is an adjunction bridging the category of types and functions and the category of all algebras of a monad and the appropriate commutative squares. Algebras are familiar to the reader familiar with recursion schemes as the stuff you use with folds, so this is nothing useless or abstract. This adjunction is compactly defined by (. pure) and (=<<). As a curiosity, it follows at once that these two functions are inverses of one another — the curious reader may entertain themself showing this using equational reasoning, it took me 15 lines in total.
  • For any numeric type, there is a simple and useful adjunction between functions on finite sets and matrices of numbers, the latter being arrows of a category of finite dimensional linear spaces (or, more generally, modules) and linear maps. This adjunction can be defined in an evening, and it is helpful in solving various computational problems.

Further, you assume that you need to do the work that you have shown to be non-trivial. This is as if I told you «there is this nice café 5 minutes by car from here» and you went by foot and then said «this was really far». Why go by foot? Hop in the car!

  1. To any monad, we can have an adjunction. I mentioned it above in this message — it is the adjunction between the category of functions and the category of algebras of that monad. You can also choose the category of free algebras of that monad if you prefer — it does not matter.
  2. Since adjunctions are invertible functions, they compose into other, more intimidating adjunctions.
  3. Since to every adjunction corresponds a monad, you can instantly have a monad made out of the curry–uncurry adjunction and the adjunction corresponding to any usual Monad monad.

This is all. We have proven that the state monad transformer is a monad, and we can now enjoy our fine abstract smoothie in the pleasant shade of wisdom.

I do not mean this as a joke or some kind of entertaining distraction. I am a working programmer, for entertainment I play guitar. All of this directly translates into Haskell programs that run and compute stuff for you.

41

Sure, but there’s also a cafe one minute away by car where they’ve already proved that StateT is a monad transformer, by equational reasoning. Why do I need to go the adjunction cafe?

You seem to be suggesting that there are more varieties of the same product on offer at the adjunction cafe. But what are they? What are these monads for which it is easier, overall, to prove that they are monads by exhibiting them as adjunctions, than it is to prove that they are monads directly?

2 Likes