chore: remove adaptState and adaptReader
This commit is contained in:
Leonardo de Moura
parent
9d741a8b3a
commit
31fd054214
3 changed files with 0 additions and 96 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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)),
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue