feat(data/sum): add monad instance

category/applicative.lean

@@ -132,6 +132,7 @@ by { refine { .. @comp.is_lawful_applicative f g _ _ _ _, .. },
      congr, funext, rw [commutative_map], congr }
 
 end comp
+
 open functor
 
 @[functor_norm]

category/basic.lean

@@ -112,6 +112,29 @@ def mtry {α} (x : F α) : F unit := (x $> ()) <|> pure ()
 
 end alternative
 
+namespace sum
+
+variables {e : Type v}
+
+protected def bind {α β} : e ⊕ α → (α → e ⊕ β) → e ⊕ β
+| (inl x) _ := inl x
+| (inr x) f := f x
+
+instance : monad (sum.{v u} e) :=
+{ pure := @sum.inr e,
+  bind := @sum.bind e }
+
+instance : is_lawful_functor (sum.{v u} e) :=
+by refine { .. }; intros; cases x; refl
+
+instance : is_lawful_monad (sum.{v u} e) :=
+{ bind_assoc := by { intros, cases x; refl },
+  pure_bind  := by { intros, refl },
+  bind_pure_comp_eq_map := by { intros, cases x; refl },
+  bind_map_eq_seq := by { intros, cases f; refl } }
+
+end sum
+
 class is_comm_applicative (m : Type* → Type*) [applicative m] extends is_lawful_applicative m : Prop :=
 (commutative_prod : ∀{α β} (a : m α) (b : m β), prod.mk <$> a <*> b = (λb a, (a, b)) <$> b <*> a)
 

category/functor.lean

@@ -106,20 +106,3 @@ instance : functor ulift :=
 { map := λ α β f, up ∘ f ∘ down }
 
 end ulift
-
-namespace sum
-
-variables {γ : Type u} {α β : Type v}
-
-protected def mapr (f : α → β) : γ ⊕ α → γ ⊕ β
-| (inl x) := inl x
-| (inr x) := inr (f x)
-
-instance : functor (sum.{u v} γ) :=
-{ map := @sum.mapr γ }
-
-instance : is_lawful_functor (sum γ) :=
-{ id_map := by intros; casesm _ ⊕ _; refl,
-  comp_map := by intros; casesm _ ⊕ _; refl }
-
-end sum