quick ixmonad and examples (#55)

Co-authored-by: Yishuai Li <liyishuai.lys@alibaba-inc.com>

Author: jldodds

_CoqProject

@@ -18,6 +18,7 @@ theories/Structures/EqDep.v
 theories/Structures/Foldable.v
 theories/Structures/FunctorLaws.v
 theories/Structures/Functor.v
+theories/Structures/IXMonad.v
 theories/Structures/Maps.v
 theories/Structures/MonadCont.v
 theories/Structures/MonadExc.v
@@ -119,6 +120,7 @@ theories/Data/Monads/FuelMonadLaws.v
 theories/Data/Monads/FuelMonad.v
 theories/Data/Monads/IdentityMonadLaws.v
 theories/Data/Monads/IdentityMonad.v
+theories/Data/Monads/IStateMonad.v
 theories/Data/Monads/OptionMonadLaws.v
 theories/Data/Monads/OptionMonad.v
 theories/Data/Monads/ReaderMonadLaws.v

examples/indexedstate.v

@@ -0,0 +1,24 @@
+Require Import ExtLib.Data.Monads.IStateMonad.
+Require Import ExtLib.Structures.IXMonad.
+
+Section example.
+
+  Import IxMonadNotation.
+  Local Open Scope ixmonad_scope. 
+        
+  Variables A B C : Type.
+
+  Variable function1 : A -> B.
+  Variable function2 : B -> C.
+
+  Definition update1 : istate A B unit :=
+    modify_ function1.
+
+  Definition update2 : istate B C unit :=
+    modify_ function2.
+
+  Definition compose : istate A C unit :=
+    update1 ;;
+    update2.
+
+End example.

theories/Data/Monads/IStateMonad.v

@@ -0,0 +1,35 @@
+Require Import ExtLib.Structures.IXMonad.
+
+Set Implicit Arguments.
+Set Strict Implicit.
+
+Section IStateType.
+
+  Record istate (i s t: Type) : Type := mkIState
+  { runIState : i -> t * s }.
+
+  Definition evalState {i s t} (c : istate i s t) (s : i) : t :=
+    fst (runIState c s).
+
+  Definition execState {i s t} (c : istate i s t) (st : i) : s :=
+    snd (runIState c st).
+
+
+  Global Instance IMonad_Ixstate : IxMonad istate  :=
+    {
+      ret  := fun _ _ v => mkIState (fun s => (v, s))
+      ; bind := fun _ _ _ _ _ c1 c2 =>
+                   mkIState (fun s =>
+                               let (v,s) := runIState c1 s in
+                               runIState (c2 v) s)
+    }.
+  
+Definition get {i : Type} := @mkIState i i i (fun s => (s,s)).
+Definition put {i o : Type} := (fun v => @mkIState i o unit (fun _ => (tt, v))).
+Definition put_  {i o : Type} (s : o) : istate i o unit := (bind (put s) (fun _ => ret tt)). 
+Definition modify {i o : Type} (f : i -> o) : istate i o i :=
+  bind get (fun x : i => bind (put (f x)) (fun _ : unit => ret x)).
+Definition modify_ {i o : Type} (f : i -> o) : istate i o unit :=
+  bind (modify f) (fun _ => ret tt).
+
+End IStateType.

theories/Structures/IXMonad.v

@@ -0,0 +1,36 @@
+Require Import ExtLib.Structures.Monad.
+Import Applicative. 
+
+Set Implicit Arguments.
+Set Strict Implicit.
+
+Polymorphic Class IxMonad@{d c} (m : Type@{d} -> Type@{d} -> Type@{c} -> Type@{c}) : Type :=
+{ ret : forall {i : Type@{d}} {a : Type@{d}}, a -> m i i a
+; bind : forall {i j k a b: Type@{d}}, m i j a -> (a -> m j k b) -> m i k b
+}.
+
+Module IxMonadNotation.
+
+  Delimit Scope ixmonad_scope with ixmonad.
+
+  Notation "c >>= f" := (@bind _ _ _ _ _ _ _ c f) (at level 50, left associativity) : ixmonad_scope.
+  Notation "f =<< c" := (@bind _ _ _ _ _ _ _ c f) (at level 51, right associativity) : ixmonad_scope.
+
+  Notation "x <- c1 ;; c2" := (@bind _ _ _ _ _ _ _ c1 (fun x => c2))
+    (at level 100, c1 at next level, right associativity) : ixmonad_scope.
+
+  Notation "e1 ;; e2" := (_ <- e1%ixmonad ;; e2%ixmonad)%ixmonad
+    (at level 100, right associativity) : ixmonad_scope.
+
+  Notation "' pat <- c1 ;; c2" :=
+    (@bind _ _ _ _ _ _ _ c1 (fun x => match x with pat => c2 end))
+    (at level 100, pat pattern, c1 at next level, right associativity) : monad_scope.
+
+End IxMonadNotation.
+
+  Global
+  Polymorphic Instance Applicative_Monad {m i} {M:IxMonad m}
+    : Applicative (m i i) :=
+    {| Applicative.pure := fun (A : Type) (X : A) => ret X
+       ; Applicative.ap := fun (A B : Type) (X : m i i (A -> B)) (X0 : m i i A) => bind X (fun X1 : A -> B => bind X0 (fun X2 : A => ret (X1 X2)))
+    |}.