Commits

wojc...@gmail.com  committed f777dea Draft

Rename Identity to IdentityMonad

  • Participants
  • Parent commits 6d163ff

Comments (0)

Files changed (3)

-MODULES  := Monads Identity ErrorMonad StateMonad
+MODULES  := Monads IdentityMonad ErrorMonad StateMonad
 VS       := $(MODULES:%=src/%.v)
 
 .PHONY: coq

File src/ErrorMonad.v

 
 
 Require Import Monads.
-Require Import Identity.
+Require Import IdentityMonad.
 
 Inductive error E A :=
 | Ok : A -> error E A

File src/IdentityMonad.v

+Require Import Monads.
+
+(** * Identity monad *)
+Module Identity <: MONAD <: MONADT_RAW.
+
+  Module Raw <: MONADT_RAW.
+
+    Definition m (A : Type) := A.
+    Definition tm := m. (* for MTinfix *)
+
+    Definition ret {A} (x : A) := x.
+
+    Definition bind {A B} (f : A -> m B) (ma : m A) : m B :=
+      f ma.
+
+    Theorem bind_unit : forall A B (a : A) (f : A -> m B),
+      bind f (ret a) = f a
+    .
+    auto.
+    Qed.
+
+    Theorem unit_bind : forall A (ma : m A),
+      bind (@ret A) ma = ma
+    .
+    auto.
+    Qed.
+
+    Theorem bind_bind : forall A B C
+        (ma : m A) (f : A -> m B) (g : B -> m C),
+      bind g (bind f ma)
+      =
+      bind (fun x => bind g (f x)) ma
+    .
+    auto.
+    Qed.
+
+  End Raw.
+
+  Include Raw.
+
+  Module Ops := MTinfix(Raw).
+
+End Identity.