chore(library/init/control/combinators): use Applicative instead of Monad in relevant combinators

library/init/control/applicative.lean

@@ -29,6 +29,6 @@ class HasSeqRight (f : Type u → Type v) : Type (max (u+1) v) :=
 infixl ` *> `:60  := HasSeqRight.seqRight
 
 class Applicative (f : Type u → Type v) extends Functor f, HasPure f, HasSeq f, HasSeqLeft f, HasSeqRight f :=
-(map       := λ _ _ x y, pure x <*> y)
+(map      := λ _ _ x y, pure x <*> y)
 (seqLeft  := λ α β a b, const β <$> a <*> b)
 (seqRight := λ α β a b, const α id <$> a <*> b)

library/init/control/combinators.lean

@@ -15,11 +15,11 @@ def mjoin {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α
 bind a id
 
 @[macroInline]
-def when {m : Type → Type u} [Monad m] (c : Prop) [h : Decidable c] (t : m Unit) : m Unit :=
+def when {m : Type → Type u} [Applicative m] (c : Prop) [h : Decidable c] (t : m Unit) : m Unit :=
 if c then t else pure ()
 
 @[macroInline]
-def unless {m : Type → Type u} [Monad m] (c : Prop) [h : Decidable c] (e : m Unit) : m Unit :=
+def unless {m : Type → Type u} [Applicative m] (c : Prop) [h : Decidable c] (e : m Unit) : m Unit :=
 if c then pure () else e
 
 @[macroInline]
@@ -32,11 +32,11 @@ mcond c t (pure ())
 
 namespace Nat
 
-@[specialize] def mforAux {m} [Monad m] (f : Nat → m Unit) : Nat → m Unit
+@[specialize] def mforAux {m} [Applicative m] (f : Nat → m Unit) : Nat → m Unit
 | 0     := pure ()
 | (i+1) := f i *> mforAux i
 
-@[inline] def mfor {m} [Monad m] (n : Nat) (f : Nat → m Unit) : m Unit :=
+@[inline] def mfor {m} [Applicative m] (n : Nat) (f : Nat → m Unit) : m Unit :=
 mforAux f n
 
 -- TODO: enable after we have support for marking arguments that should be considered for specialization.
@@ -51,12 +51,12 @@ end Nat
 namespace List
 
 @[specialize]
-def mmap {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
-| []       := pure []
-| (h :: t) := do h' ← f h, t' ← mmap t, pure (h' :: t')
+def mmap {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
+| []      := pure []
+| (a::as) := (::) <$> (f a) <*> mmap as
 
 @[specialize]
-def mfor {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
+def mfor {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
 | []       := pure ⟨⟩
 | (h :: t) := f h *> mfor t
 

library/init/control/estate.lean

@@ -117,8 +117,13 @@ instance [Inhabited ε] : Inhabited (EState ε σ α) :=
      | Result.ok a s    := Result.ok (f a) s
      | Result.error e s := Result.error e s
 
+@[inline] protected def seqRight (x : EState ε σ α) (y : EState ε σ β) : EState ε σ β :=
+λ r, match x r with
+     | Result.ok _ s    := y (resultOk.mk ⟨⟩ s)
+     | Result.error e s := Result.error e s
+
 instance : Monad (EState ε σ) :=
-{ bind := @EState.bind _ _, pure := @EState.pure _ _, map := @EState.map _ _ }
+{ bind := @EState.bind _ _, pure := @EState.pure _ _, map := @EState.map _ _, seqRight := @EState.seqRight _ _ }
 
 instance : HasOrelse (EState ε σ) :=
 { orelse := @EState.orelse _ _ }

library/init/control/except.lean

@@ -68,7 +68,7 @@ match ma with
 | Except.error e := handle e
 
 instance : Monad (Except ε) :=
-{ pure := @Except.return _, bind := @Except.bind _ }
+{ pure := @Except.return _, bind := @Except.bind _, map := @Except.map _ }
 end Except
 
 def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
@@ -83,7 +83,7 @@ x
 namespace ExceptT
 variables {ε : Type u} {m : Type u → Type v} [Monad m]
 
-@[inline] protected def return {α : Type u} (a : α) : ExceptT ε m α :=
+@[inline] protected def pure {α : Type u} (a : α) : ExceptT ε m α :=
 ExceptT.mk $ pure (Except.ok a)
 
 @[inline] protected def bindCont {α β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β)
@@ -93,6 +93,11 @@ ExceptT.mk $ pure (Except.ok a)
 @[inline] protected def bind {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m β :=
 ExceptT.mk $ ma >>= ExceptT.bindCont f
 
+@[inline] protected def map {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β :=
+ExceptT.mk $ x >>= λ a, match a with
+  | (Except.ok a)    := pure $ Except.ok (f a)
+  | (Except.error e) := pure $ Except.error e
+
 @[inline] protected def lift {α : Type u} (t : m α) : ExceptT ε m α :=
 ExceptT.mk $ Except.ok <$> t
 
@@ -111,7 +116,7 @@ instance (m') [Monad m'] : MonadFunctor m m' (ExceptT ε m) (ExceptT ε m') :=
 ⟨λ _ f x, f x⟩
 
 instance : Monad (ExceptT ε m) :=
-{ pure := @ExceptT.return _ _ _, bind := @ExceptT.bind _ _ _ }
+{ pure := @ExceptT.pure _ _ _, bind := @ExceptT.bind _ _ _, map := @ExceptT.map _ _ _ }
 
 @[inline] protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → ExceptT ε' m α :=
 λ x, ExceptT.mk $ Except.mapError f <$> x

library/init/control/id.lean

@@ -17,8 +17,11 @@ x
 @[inline] def Id.bind {α β : Type u} (x : Id α) (f : α → Id β) : Id β :=
 f x
 
+@[inline] def Id.map {α β : Type u} (f : α → β) (x : Id α) : Id β :=
+f x
+
 @[inline] instance : Monad Id :=
-{ pure := @Id.pure, bind := @Id.bind }
+{ pure := @Id.pure, bind := @Id.bind, map := @Id.map }
 
 @[inline] def Id.run {α : Type u} (x : Id α) : α :=
 x

library/init/control/reader.lean

@@ -32,8 +32,11 @@ pure
 @[inline] protected def bind (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) : ReaderT ρ m β :=
 λ r, do a ← x r, f a r
 
+@[inline] protected def map (f : α → β) (x : ReaderT ρ m α) : ReaderT ρ m β :=
+λ r, f <$> x r
+
 instance : Monad (ReaderT ρ m) :=
-{ pure := @ReaderT.pure _ _ _, bind := @ReaderT.bind _ _ _ }
+{ pure := @ReaderT.pure _ _ _, bind := @ReaderT.bind _ _ _, map := @ReaderT.map _ _ _ }
 
 @[inline] protected def lift (a : m α) : ReaderT ρ m α :=
 λ r, a

library/init/control/state.lean

@@ -30,10 +30,13 @@ variables [Monad m] {α β : Type u}
 λ s, pure (a, s)
 
 @[inline] protected def bind (x : StateT σ m α) (f : α → StateT σ m β) : StateT σ m β :=
-λ s, do (a, s') ← x s, f a s'
+λ s, do (a, s) ← x s, f a s
+
+@[inline] protected def map (f : α → β) (x : StateT σ m α) : StateT σ m β :=
+λ s, do (a, s) ← x s, pure (f a, s)
 
 instance : Monad (StateT σ m) :=
-{ pure := @StateT.pure _ _ _, bind := @StateT.bind _ _ _ }
+{ pure := @StateT.pure _ _ _, bind := @StateT.bind _ _ _, map := @StateT.map _ _ _ }
 
 @[inline] protected def orelse [Alternative m] {α : Type u} (x₁ x₂ : StateT σ m α) : StateT σ m α :=
 λ s, x₁ s <|> x₂ s