From ac6e122037f87385567fc37593b091cad8fc82fd Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Tue, 21 Jan 2025 16:28:56 +0100
Subject: [PATCH] [Kernel] Improving Composition doc

---
 src/libraries/monads/composition.mli | 27 ++++++++++++++++++++-------
 src/libraries/monads/monad.mli       |  3 ++-
 2 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/src/libraries/monads/composition.mli b/src/libraries/monads/composition.mli
index a45665a64b..fa260d44db 100644
--- a/src/libraries/monads/composition.mli
+++ b/src/libraries/monads/composition.mli
@@ -20,9 +20,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** This module exposes two functors that, given a monad M called the
-    "interior monad" and a monad N called the "exterior monad", build
-    a monad of type ['a M.t N.t]. To be able to do so, one has to provide
+(** This module exposes two functors that, given a monad T called the
+    "interior monad" and a monad S called the "exterior monad", build
+    a monad of type ['a T.t S.t]. To be able to do so, one has to provide
     a [swap] function that, simply put, swap the exterior monad out of
     the interior one. In other word, this function allows fixing
     "badly ordered" monads compositions, in the sens that they are
@@ -40,10 +40,17 @@
         | None -> State.return None
         | Some s -> State.map Option.return s
     ]}
-
     Note here that trying to reverse the order of the Option and State
     monads makes the [swap] function way harder to write. Moreover, the
     resulting function does not actually satisfy the required axioms.
+
+    Indeed, all [swap] functions will not result in a valid composed monad.
+    To produce such a monad, the given [swap] function must verify the
+    following equations:
+    1. ∀t: 'a T.t, [swap (T.map S.return t) ≣ S.return t]
+    2. ∀s: 'a S.t, [swap (T.return s) ≣ S.map T.return s]
+    3. ∀x: 'a S.t S.t T.t, [swap (T.map S.flatten x) ≣ S.flatten (S.map swap (swap x))]
+    4. ∀x: 'a S.t T.t T.t, [swap (T.flatten x) ≣ S.map T.flatten (swap (T.map swap x))]
     More details on this at the end of this file.
     @since Frama-C+dev *)
 
@@ -72,9 +79,15 @@ module Make_with_product
     Monads composition is a notoriously difficult topic, and no general
     approach exists. The one provided in this module is, in theory,
     quite restrictive as the [swap] function, also called a distributive
-    law, has to satisfy four axioms to guarantee that a valid monad can
-    be built. Roughly speaking, those axioms enforce the idea that
-    the distributive law must preserve all structures in the two monads.
+    law, has to satisfy the four presented axioms to guarantee that a
+    valid monad can be built. Roughly speaking, those axioms enforce the
+    idea that the distributive law must preserve all structures in the
+    two monads.
+
+    Distributive laws, their application to monads composition and weakenings
+    of their axioms are a broad topic with profound implications in category
+    theory. Even if none of this formal knowledge us required to use this
+    module, one can check the following references to satisfy their curiosity.
 
     @see Jon Beck paper "Distributive laws" for more details on this topic.
     @see Alexandre Goy thesis "On the compositionality of monads via weak
diff --git a/src/libraries/monads/monad.mli b/src/libraries/monads/monad.mli
index 222c759b42..9d1ed937b9 100644
--- a/src/libraries/monads/monad.mli
+++ b/src/libraries/monads/monad.mli
@@ -24,7 +24,8 @@
     to build them based on minimal definitions. Those tools are provided
     for advanced users that would like to define their own monads. Any
     user that only wants to use the monads provided by the kernel can
-    completly ignore them. *)
+    completly ignore them.
+    @since Frama-C+dev *)
 
 
 
-- 
GitLab