3 ms·
So you're saying borrow checking is the one thing that can't be modelled as a monad?
by klipt 7y ago
So you're saying borrow checking is the one thing that can't be modelled as a monad?
- Ericson2314 7y agoIt'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.
- thesz 7y agoYou have to have parametrized monad [1] - a type like M inState outState result. [1] http://blog.sigfpe.com/2009/02/beyond-monads.html 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 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.