Théo Winterhalter (Mar 29 2023 at 14:35): Théo Winterhalter (Mar 29 2023 at 14:35):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:
Kazuhiko Sakaguchi (Mar 29 2023 at 14:55):@Théo Winterhalter Did you check Monae? Though it uses canonical structures, not type classes.
Kazuhiko Sakaguchi (Mar 29 2023 at 14:55):CC @Reynald Affeldt
Théo Winterhalter (Mar 29 2023 at 15:03):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!
Kazuhiko Sakaguchi (Mar 29 2023 at 15:15):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.
Reynald Affeldt (Mar 29 2023 at 16:21):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.
Reynald Affeldt (Mar 29 2023 at 16:23):Note that you may find some [the … of …] notations disgracious but they should go away with Coq 8.16.
Reynald Affeldt (Mar 29 2023 at 16:27):There is also a theory of monad transformers in an appropriately named file.
Reynald Affeldt (Mar 29 2023 at 16:29):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.
Théo Winterhalter (Mar 29 2023 at 16:36):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