This way you can encode current binding environment into state and state changing code and have operations that use existing type checking and inference facilities of current Haskell (or Agda, or something else) compiler to rule out violations.
I keep saying that what is language feature in Rust, C#, C++, Java and some other currently hot programming languages is an ordinary library in Haskell.
Comments
You have to have parametrized monad [1] - a type like M inState outState result.
[1] http://blog.sigfpe.com/2009/02/beyond-monads.html
This way you can encode current binding environment into state and state changing code and have operations that use existing type checking and inference facilities of current Haskell (or Agda, or something else) compiler to rule out violations.
[2] https://jpaykin.github.io/papers/pz_linearity_monad_2017.pdf
I keep saying that what is language feature in Rust, C#, C++, Java and some other currently hot programming languages is an ordinary library in Haskell.