Hi!

Say I define a monad type class as follows:

```
Class Monad (M : Type → Type) := {
ret : ∀ A, A → M A ;
bind : ∀ A B, M A → (A → M B) → M B
}.
```

I may want to write some code in `M (N A)`

where `M (N A)`

itself might be a monad. When I try to use `bind`

or even `ret`

, Coq will be confused trying to figure out which monad I mean. I suppose monad transformers might help, but I'm not sure how to define it so that Coq will pick it up. And it might also be the case that I don't have a transformer but still want to use `bind`

in `M (N A)`

to either mean the one of `M`

or the one of `N`

.

My question is: does anyone have pointers to developments that do this kind of stuff? @Meven Lennon-Bertrand and I would be interested. Thanks! :blush:

@Théo Winterhalter Did you check Monae? Though it uses canonical structures, not type classes.

CC @Reynald Affeldt

No I didn't look. Is it convenient to use when Coq needs to infer stuff? In my case I don't care about naturality or things like this. Thanks for the reference!

Yes, I expect that inference works without any significant issues. Reynald would be able to confirm it.

Even if Monae is not what you need or it is too much in some sense, I hope that imitating what it does (basically, it just uses Hierarchy Builder) solves your issue with inference.

Maybe the file monad_composition.v can be informative. It reproduces as an exercise some proofs from the 1993 paper by Jones and Duponcheel on composing monads.

Note that you may find some [the … of …] notations disgracious but they should go away with Coq 8.16.

There is also a theory of monad transformers in an appropriately named file.

As you can see the use of canonical structures as provided by HB allowed us to go easily from paper to Coq. You will maybe have the same experience.

It will take some time for to digest because mathcomp style is pretty hard to read for me. Thanks.

To clarify, my problem is that I have a general recursion monad and that sometimes you want to write partial functions that are themselves monadic. Merging the two inside one monad seems wrong as you expect a recursive call to return something in the monad, but when you have two monads at play, Coq fails at unification.

So I guess maybe I should provide a canonical instance of Monae instad.

Last updated: Oct 04 2023 at 22:01 UTC