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.
It's more like it's hard to mix together built in and modeled notions together. Like I could hand-write some CPS and then compile that all go gotos, but if I forget to never return the invariant is broken and the compile fails. Monads in rust sort of work if you don't use any "native" control flow.
Comments
So you're saying borrow checking is the one thing that can't be modelled as a monad?
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.
It's more like it's hard to mix together built in and modeled notions together. Like I could hand-write some CPS and then compile that all go gotos, but if I forget to never return the invariant is broken and the compile fails. Monads in rust sort of work if you don't use any "native" control flow.