@Kha: the new `ST` (and `EST`) are escapable like the Haskell ST monad.
It makes `StateRefT` much more useful because we can now run it from pure
code.
@Kha I am calling it `ST` for lack of a better name. It makes some
sense since only the `IO.Ref` operations are in `EIO Empty` :)
That being said, it may confuse Haskell users.
BTW, I had to give the name to avoid a nontermination in the TC
procedure when using
```lean
instance EIOEmpty.monadLift {ε} : HasMonadLift (EIO Empty) (EIO ε) :=
{ monadLift := fun α => fromEmptyEIO }
```
@Kha I tried to remove `MonadExceptOf` by adding `HasThrow` and
`HasCatch`, but this change impacts our ability to define polymorphic
methods such as `finally` which is parametrized by `[MonadExcept]`.
If we remove the `outParam` from `[MonadExcept]`, then we will need to
know the exception at `finally`, or add two instances `[HasCatch]` and
`[HasThrow]`. So, it seems it is more convenient to have
`[MonadExceptOf]` and `[MonadExcept]`. Thus, I applied this approach
to `[MonadState]`
We add helper classes with `outParam`.
@Kha This is similar to the `MonadExceptOf` modification.
Motivation: the new `StateRefT` (state monad implemented using
`IO.Ref`) makes is it quite cheap to have multiple states on the
stack. But, we need a mechanism for accessing the different states in
a convenient way.
Note that, I did not add a `MonadStateOf` class, but helper classes
such as `HasGet` which uses `outParam`. I will do the same for `MonadExcept`.
Summary:
- `get` gets the state on the top of the Monad stack
- `getThe σ` gets the state with type `σ`
- `modify f` modifies the state on the top of the Monad stack.
We use `modify fun s => { s with ... }` quite often, and we cannot
infer type of `s` here.
- `modifyThe σ f` allows us to select which state on the stack we are modifying.
- I didn't add `setThe`, since we usually can infer the state type at
`set s`. In the whole codebase, we have only one instance where this
is not true.
