From e2e98a0c070e350ed80bfe630294675b7da45359 Mon Sep 17 00:00:00 2001 From: Joey Dodds Date: Fri, 1 Feb 2019 14:57:38 -0800 Subject: [PATCH 1/2] quick ixmonad and examples --- _CoqProject | 2 ++ examples/indexedstate.v | 24 +++++++++++++++++++ theories/Data/Monads/IStateMonad.v | 35 ++++++++++++++++++++++++++++ theories/Structures/IXMonad.v | 37 ++++++++++++++++++++++++++++++ 4 files changed, 98 insertions(+) create mode 100644 examples/indexedstate.v create mode 100644 theories/Data/Monads/IStateMonad.v create mode 100644 theories/Structures/IXMonad.v diff --git a/_CoqProject b/_CoqProject index 4623fe1c..cd3fb5cf 100644 --- a/_CoqProject +++ b/_CoqProject @@ -18,6 +18,7 @@ theories/Structures/Foldable.v theories/Structures/FunctorLaws.v theories/Structures/Functor.v theories/Structures/Identity.v +theories/Structures/IXMonad.v theories/Structures/Maps.v theories/Structures/MonadCont.v theories/Structures/MonadExc.v @@ -120,6 +121,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/ListMonad.v theories/Data/Monads/OptionMonadLaws.v theories/Data/Monads/OptionMonad.v diff --git a/examples/indexedstate.v b/examples/indexedstate.v new file mode 100644 index 00000000..c9b02be8 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/theories/Data/Monads/IStateMonad.v b/theories/Data/Monads/IStateMonad.v new file mode 100644 index 00000000..58309baf --- /dev/null +++ b/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. diff --git a/theories/Structures/IXMonad.v b/theories/Structures/IXMonad.v new file mode 100644 index 00000000..97453985 --- /dev/null +++ b/theories/Structures/IXMonad.v @@ -0,0 +1,37 @@ +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. + + 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))) + |}. + + \ No newline at end of file From 85103459160b05abad9e6b02de8be083624a7c99 Mon Sep 17 00:00:00 2001 From: Yishuai Li Date: Thu, 4 Jan 2024 15:34:46 +0800 Subject: [PATCH 2/2] Attribute locality --- theories/Structures/IXMonad.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/Structures/IXMonad.v b/theories/Structures/IXMonad.v index 97453985..c9c8143a 100644 --- a/theories/Structures/IXMonad.v +++ b/theories/Structures/IXMonad.v @@ -28,10 +28,9 @@ Module IxMonadNotation. 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))) |}. - - \ No newline at end of file