Combining monads with natural transformations

Links
1

I wrote a blog post about an approach to combine multiple effects using natural transformations.

Looking forward to know what people think about it

8 Likes
2

do you really want unrestricted natural transformations? not even monad homomorphisms? i am not sure if that much generality buys you anything. actually probably you can write some counterintuitive code with that much freedom. and it is difficult to reason with arbitrary natural transformations. the general idea reminded me of this: Control.Monad.Morph

also, having a class for embeddings feels odd. a monad may embed into another monad (or even into itself) in many ways. it is not clear that it is possible or advisable to canonize one by a typeclass. here is a zoo of them to give you an idea about what i am trying to say: https://gist.github.com/ekmett/48f1b578cadeeaeee7a309ec6933d7ec

3

You will quickly run into overlapping instances and/or underspecified types with the Embeds class.

You can also replace almost all of mtl by deriving monads and monad transformers from adjunctions, but it suffers from the same problem of underspecified types and class instances.

This is not so much a problem of the math itself but of the GHC type checking mechanism.

1 Like
4

I haven’t read your post yet but the title reminded me of this talk:

3 Likes
5

you’re right the unrestricted natural transformation is not the right abstraction here. It’s some kind of natural transformations, but it’s not really clear to me which one…

If you take a look at the instances, you’ll see that I’m already using MFunctor from the mmorph package

6

If you take a look at the real code (see https://github.com/marcosh/embeds/blob/main/src/Embeds/NatTrans.hs), you’ll see that there’s actually more instances and overlapping instances should have been taken care of.

You can also replace almost all of mtl by deriving monads and monad transformers from adjunctions, but it suffers from the same problem of underspecified types and class instances.

Could you provide more details, please? It’s not clear to me what you mean

1 Like
7

thanks, that looks interesting, I’ll take a look!

8

You probably know that every monad arises via an adjunction. For example, given any monad m on the category Hask a.k.a. (->), there is the adjunction between (->) and the category Kleisli m where

  • The left adjoint maps type a to a and morphism f to Kleisli (return.f)
  • The right adjoint maps type a to m a and morphism Kleisi k to (=<<) k

The composite of the two functors is the monad m. The nice thing about adjunctions is that they always compose: The composite of two left adjoints is a left adjoint.
Many transformers arise as functors on Kleisli categories. For example see Section 8.10 of Haskell for mathematicians. But when composing two adjunctions, the intermediate categories are invisible in the final type signature, whence the type checker has problems selecting the appropriate adjunctions.

2 Likes
9

As a fourth year PhD in programming languages, I can proudly say… kind of. I’ve heard about it, but I don’t feel like I really know what it means.

This is actually the first source I’ve seen that seems to have a good treatment of adjunctions for Haskellers. Thank you for linking it!

I have a GHC plugin for transitive constraints, so maybe that can help:

I’ll see if I can use it to infer adjunctions.

10

Actually the data-category package seems to have it covered pretty thoroughly. In contrast, the adjunctions package talks only about endofunctors in (->) which is a bit boring.

The additional complication is that a certain type constructor m could be an (adjoint) functor between potentially many different categories. That is why apparently data-category uses type-level tags to distinguish what source and target categories are meant.

Monads in other categories are interesting in another surprising way: in point-free topology one studies the lattice of open sets. This can be considered a category with open sets as objects and inclusion relations as arrows. Intersection is the product on such a category. (An endofunctor in this category is a monotone function from opens to opens.) Now it turns out that one of (several equivalent) representations of a sub-space is a so-called nucleus, which categorically is nothing but a strong monad! So we could say that “monads are the sub-spaces of the universe of Haskell types”.

11

This is neat.
I would suggest you use QualifiedDo rather than RebindableSyntax :slight_smile:.

2 Likes
12

To some extent, the idea existed since some time here: Control.Monad.Base

I vaguely remember that we were playing with this approach while doing research on dunai, but I believe the instance resolution was too brittle (as others have suggested) for it to be practical.

13

Ah, nice to see that the idea was already there, thanks for pointing this out.

I’m now convinced that Embeds as I defined it and presented in the post is too week and it should have other functions