1. Dmitry Grebeniuk
  2. coq-practical-monads

Commits

Dmitry Grebeniuk  committed 6d163ff

added/changed doc; wrapped long lines

  • Participants
  • Parent commits 2edde6e
  • Branches default

Comments (0)

Files changed (1)

File src/Monads.v

View file
 (** * Primitive monad module types
  *)
 
-(** ** Raw monad transformer type
+(** ** Raw monad type
 
        This is the minimal signature that must be implemented when
        introducing a new monad module.
   (** [ret v] wraps the value [v] into monad *)
   Parameter ret : forall A (a : A), tm A.
 
-  (** Sequentially compose two actions, passing any value produced by
-      the first as an argument to the second.
+  (** [bind f m] passes value contained in monad [m] to function [f].
+      It's useful for sequentially composing actions executed inside
+      monad.
+      It's equivalent to [m >>= f] found in other languages.
    *)
   Parameter bind : forall A B, (A -> tm B) -> tm A -> tm B.
 
     bind f (ret a) = f a
   .
 
-  (** Identity bind *)
+  (** Passing monadic value to [ret] gives the same monadic value *)
   Parameter unit_bind : forall A (ma : tm A),
     bind (@ret A) ma = ma
   .
 
-  (** TODO: Add doc *)
+  (** Bind is an associative function *)
   Parameter bind_bind : forall A B C
       (ma : tm A) (f : A -> tm B) (g : B -> tm C),
     bind g (bind f ma)
     (at level 56, left associativity)
   .
 
-  (** Right-to-left Kleisli composition of monads. (>=>), with the arguments flipped.  *)
+  (** Right-to-left Kleisli composition of monads. (>=>), with the arguments
+      flipped.  *)
   Notation "g <=< f" := (fun x => @M.bind _ _ g (f x))
     (at level 56, left associativity)
   .
 End MONAD.
 
 
-(** * Monad transformer from monad *)
+(** * Monad transformer type.
+      It takes monad [M] as a module and returns the result of
+      applying monad transformer to [M].
+      Use [lift action] to perform [M]-monad specific [action]
+      inside the transformed monad. *)
 Module Type MONADT (M : MONAD) <: MONAD <: MONADT_RAW.
 
   Module Mo.
 
 End Minher.
 
-(** * Additional proof for bind compose *)
+(** * Additional proof for bind compose.
+      Useful for proving [MONADT.lift_bind]. *)
 Module BindCompose (M : MONADT_RAW).
 
   Require Import FunctionalExtensionality.
   Module Ops := MTinfix(M).
   Import Ops.
 
-  (** Evaluate each action in the sequence from left to right, and collect the results. *)
+  (** Evaluate each action in the sequence from left to right, and collect
+      the results. *)
   Section sequence.
     Variable A : Type.
     Definition sequence (l : list (tm A)) : tm (list A) :=
       List.fold_right f (ret nil) l.
   End sequence.
 
-  (** Evaluate each action in the sequence from left to right, and ignore the results. *)
+  (** Evaluate each action in the sequence from left to right, and ignore
+      the results. *)
   Section sequence_.
     Variable A : Type.
     Definition sequence_ (l : list (tm A)) : tm unit :=
   Parameter msum : forall A, list (tm A) -> tm A.
   Parameter mfilter : forall A, (A -> bool) -> tm A -> tm A.
   Parameter filterM : forall A, (A -> tm bool) -> list A -> tm (list A).
-  Parameter mapAndUnzipM : forall A B C, (A -> tm (B * C)) -> list A -> tm (list B * list C)%type.
-  Parameter zipWithM : forall A B C, (A -> B -> tm C) -> list A -> list B -> tm (list C).
-  Parameter zipWithM_ : forall A B C, (A -> B -> tm C) -> list A -> list B -> tm unit.
+  Parameter mapAndUnzipM : forall A B C, (A -> tm (B * C)) ->
+                           list A -> tm (list B * list C)%type.
+  Parameter zipWithM : forall A B C, (A -> B -> tm C) ->
+                              list A -> list B -> tm (list C).
+  Parameter zipWithM_ : forall A B C, (A -> B -> tm C) ->
+                               list A -> list B -> tm unit.
   Parameter foldM : forall A B, (A -> B -> tm A) -> A -> list B -> tm A.
   Parameter foldM_ : forall A B, (A -> B -> tm A) -> A -> list B -> tm unit.
   Parameter replicateM : forall A, nat -> tm A -> tm (list A).
     Definition join (mm : tm (tm A)) : tm A := @bind _ _ (fun x => x) mm.
   End join.
 
-  Definition msum : forall A, list (tm A) -> tm A := fun _ l => List.fold_right (@mplus _) (@mzero _) l.
+  Definition msum : forall A, list (tm A) -> tm A :=
+    fun _ l => List.fold_right (@mplus _) (@mzero _) l.
 
   Definition mfilter : forall A, (A -> bool) -> tm A -> tm A :=
     fun _ f m => @bind _ _ (fun x => if f x then ret x else @M.mzero _) m.
   (*     end. *)
   (* End filterM. *)
 
-  End List.
+  End List.