From 8b145d7884e2b102e3dcd59e3a2dfa30da4fe3b7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Apr 2019 13:28:08 -0700 Subject: [PATCH] chore(library/init/control/combinators): use `Applicative` instead of `Monad` in relevant combinators --- library/init/control/applicative.lean | 2 +- library/init/control/combinators.lean | 16 ++++++++-------- library/init/control/estate.lean | 7 ++++++- library/init/control/except.lean | 11 ++++++++--- library/init/control/id.lean | 5 ++++- library/init/control/reader.lean | 5 ++++- library/init/control/state.lean | 7 +++++-- 7 files changed, 36 insertions(+), 17 deletions(-) diff --git a/library/init/control/applicative.lean b/library/init/control/applicative.lean index fdc8cab991..6488ca69cb 100644 --- a/library/init/control/applicative.lean +++ b/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) diff --git a/library/init/control/combinators.lean b/library/init/control/combinators.lean index 5bc60286e6..7619b3224a 100644 --- a/library/init/control/combinators.lean +++ 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 diff --git a/library/init/control/estate.lean b/library/init/control/estate.lean index ac95e82059..3cfdeacae1 100644 --- a/library/init/control/estate.lean +++ b/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 _ _ } diff --git a/library/init/control/except.lean b/library/init/control/except.lean index 01aaf48000..06aaf5c0c7 100644 --- a/library/init/control/except.lean +++ b/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 diff --git a/library/init/control/id.lean b/library/init/control/id.lean index dae7455895..604bd3bdf0 100644 --- a/library/init/control/id.lean +++ b/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 diff --git a/library/init/control/reader.lean b/library/init/control/reader.lean index d7053cce17..ce20ae46ef 100644 --- a/library/init/control/reader.lean +++ b/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 diff --git a/library/init/control/state.lean b/library/init/control/state.lean index 48279b9da9..4c0ce33621 100644 --- a/library/init/control/state.lean +++ b/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