From 31fd054214a13858bc4ed81509ff74152cd3dbe9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Oct 2020 16:32:58 -0700 Subject: [PATCH] chore: remove `adaptState` and `adaptReader` --- src/Init/Control/EState.lean | 10 ------- src/Init/Control/Reader.lean | 35 ------------------------- src/Init/Control/State.lean | 51 ------------------------------------ 3 files changed, 96 deletions(-) diff --git a/src/Init/Control/EState.lean b/src/Init/Control/EState.lean index 551eb9f722..a4cb381c3f 100644 --- a/src/Init/Control/EState.lean +++ b/src/Init/Control/EState.lean @@ -133,16 +133,6 @@ instance : MonadFinally (EStateM ε σ) := | Result.ok _ s => Result.error e₁ s | Result.error e₂ s => Result.error e₂ s } -@[inline] def adaptState {σ₁ σ₂} (split : σ → σ₁ × σ₂) (merge : σ₁ → σ₂ → σ) (x : EStateM ε σ₁ α) : EStateM ε σ α := -fun s => - let (s₁, s₂) := split s; - match x s₁ with - | Result.ok a s₁ => Result.ok a (merge s₁ s₂) - | Result.error e s₁ => Result.error e (merge s₁ s₂) - -instance {ε σ σ'} : MonadStateAdapter σ σ' (EStateM ε σ) (EStateM ε σ') := -⟨fun σ'' α => EStateM.adaptState⟩ - @[inline] def fromStateM {ε σ α : Type} (x : StateM σ α) : EStateM ε σ α := fun s => match x.run s with diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean index 771d96fda7..e9b4d82a3d 100644 --- a/src/Init/Control/Reader.lean +++ b/src/Init/Control/Reader.lean @@ -112,41 +112,6 @@ instance monadReaderTrans {ρ : Type u} {m : Type u → Type v} {n : Type u → instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadReaderOf ρ (ReaderT ρ m) := ⟨ReaderT.read⟩ -/-- Adapt a Monad stack, changing the Type of its top-most environment. - - This class is comparable to [Control.Lens.Magnify](https://hackage.haskell.org/package/lens-4.15.4/docs/Control-Lens-Zoom.html#t:Magnify), but does not use lenses (why would it), and is derived automatically for any transformer implementing `MonadFunctor`. - - Note: This class can be seen as a simplification of the more "principled" definition - ``` - class MonadReaderFunctor (ρ ρ' : outParam (Type u)) (n n' : Type u → Type u) := - (map {α : Type u} : (∀ {m : Type u → Type u} [Monad m], ReaderT ρ m α → ReaderT ρ' m α) → n α → n' α) - ``` - -/ -class MonadReaderAdapterOf (ρ : outParam (Type u)) (ρ' : Type u) (m m' : Type u → Type v) := -(adaptReader {α : Type u} : (ρ' → ρ) → m α → m' α) - -@[inline] def adaptTheReader {ρ : Type u} (ρ' : Type u) {m m' : Type u → Type v} [MonadReaderAdapterOf ρ ρ' m m'] {α} : (ρ' → ρ) → m α → m' α := -MonadReaderAdapterOf.adaptReader - -/-- Similar to `MonadReaderAdapterOf`, but `ρ'` is an `outParam` for convenience -/ -class MonadReaderAdapter (ρ ρ' : outParam (Type u)) (m m' : Type u → Type v) := -(adaptReader {α : Type u} : (ρ' → ρ) → m α → m' α) - -export MonadReaderAdapter (adaptReader) - -instance MonadReaderAdapterOf.isMonadReaderAdapter (ρ ρ' : Type u) (m m' : Type u → Type v) [MonadReaderAdapterOf ρ ρ' m m'] : MonadReaderAdapter ρ ρ' m m' := -⟨fun α => adaptTheReader ρ'⟩ - -section -variables {ρ ρ' : Type u} {m m' : Type u → Type v} - -instance monadReaderAdapterTrans {n n' : Type u → Type v} [MonadReaderAdapterOf ρ ρ' m m'] [MonadFunctor m m' n n'] : MonadReaderAdapterOf ρ ρ' n n' := -⟨fun α f => monadMap (fun α => (adaptReader f : m α → m' α))⟩ - -instance [Monad m] : MonadReaderAdapterOf ρ ρ' (ReaderT ρ m) (ReaderT ρ' m) := -⟨fun α => ReaderT.adapt⟩ -end - instance ReaderT.monadControl (ρ : Type u) (m : Type u → Type v) : MonadControl m (ReaderT ρ m) := { stM := fun α => α, liftWith := fun α f ctx => f fun β x => x ctx, diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean index decc47889f..7eacb7773b 100644 --- a/src/Init/Control/State.lean +++ b/src/Init/Control/State.lean @@ -148,57 +148,6 @@ instance [Monad m] : MonadStateOf σ (StateT σ m) := end -/-- Adapt a Monad stack, changing the Type of its top-most State. - - This class is comparable to [Control.Lens.Zoom](https://hackage.haskell.org/package/lens-4.15.4/docs/Control-Lens-Zoom.html#t:Zoom), but does not use lenses (yet?), and is derived automatically for any transformer implementing `MonadFunctor`. - - For zooming into a part of the State, the `split` Function should split σ into the part σ' and the "context" σ'' so that the potentially modified σ' and the context can be rejoined by `join` in the end. - In the simplest case, the context can be chosen as the full outer State (ie. `σ'' = σ`), which makes `split` and `join` simpler to define. However, note that the State will not be used linearly in this case. - - Example: - ``` - def zoomFst {α σ σ' : Type} : State σ α → State (σ × σ') α := - adaptState id Prod.mk - ``` - - The Function can also zoom out into a "larger" State, where the new parts are supplied by `split` and discarded by `join` in the end. The State is therefore not used linearly anymore but merely affinely, which is not a practically relevant distinction in Lean. - - Example: - ``` - def withSnd {α σ σ' : Type} (snd : σ') : State (σ × σ') α → State σ α := - adaptState (fun st => ((st, snd), ())) (fun ⟨st,snd⟩ _ => st) - ``` - - Note: This class can be seen as a simplification of the more "principled" definition - ``` - class MonadStateFunctor (σ σ' : outParam (Type u)) (n n' : Type u → Type u) := - (map {α : Type u} : (∀ {m : Type u → Type u} [Monad m], StateT σ m α → StateT σ' m α) → n α → n' α) - ``` - which better describes the intent of "we can map a `StateT` anywhere in the Monad stack". - If we look at the unfolded Type of the first argument `∀ m [Monad m], (σ → m (α × σ)) → σ' → m (α × σ')`, we see that it has the lens Type `∀ f [Functor f], (α → f α) → β → f β` with `f` specialized to `fun σ => m (α × σ)` (exercise: show that this is a lawful Functor). We can build all lenses we are insterested in from the functions `split` and `join` as - ``` - fun f _ st => let (st, ctx) := split st in - (fun st' => join st' ctx) <$> f st - ``` - -/ -class MonadStateAdapter (σ σ' : outParam (Type u)) (m m' : Type u → Type v) := -(adaptState {σ'' α : Type u} (split : σ' → σ × σ'') (join : σ → σ'' → σ') : m α → m' α) -export MonadStateAdapter (adaptState) - -section -variables {σ σ' : Type u} {m m' : Type u → Type v} - -@[inline] def MonadStateAdapter.adaptState' [MonadStateAdapter σ σ' m m'] {α : Type u} (toSigma : σ' → σ) (fromSigma : σ → σ') : m α → m' α := -adaptState (fun st => (toSigma st, PUnit.unit)) (fun st _ => fromSigma st) -export MonadStateAdapter (adaptState') - -instance monadStateAdapterTrans {n n' : Type u → Type v} [MonadStateAdapter σ σ' m m'] [MonadFunctor m m' n n'] : MonadStateAdapter σ σ' n n' := -⟨fun σ'' α split join => monadMap (fun α => (adaptState split join : m α → m' α))⟩ - -instance [Monad m] : MonadStateAdapter σ σ' (StateT σ m) (StateT σ' m) := -⟨fun σ'' α => StateT.adapt⟩ -end - instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (StateT σ m) := { stM := fun α => α × σ, liftWith := fun α f => do s ← get; liftM (f (fun β x => x.run s)),