Haskell's type system is very powerful. I already provided an example of the linearly-typed monadic code, but there are examples of how to implement Rust-like borrow checking, etc.
Linear typing and borrow checking are all about environment manipulation. Introduction of linearly-typed object creates a unique (through the code) reference to that object in the environment and use of linearly-typed object removes that reference from the environment. Borrow checking can work similarly.
So abstract interpretation of the program implicitly uses state of environment and implicitly modifies it.
Such state monad with typed environment was possible in Haskell as early as 2009: https://blog.sigfpe.com/2009/02/beyond-monads.html
Sets of types (generalized records) were available in Haskell from 2004: https://okmij.org/ftp/Haskell/dependent-types.html#HList
Basically, it was possible to embed Rust-like language into Haskell from 2009 on, the ideas were all there.
The thesis that I continue to read is about dependencies. These dependencies control effects of the different parts of the program and one of the first more or less successful and practical way to control effects was monads in Haskell and, after that, monad transformers.
From my experience with Haskell, I more than love Software Transactional Memory, implemented as a monad without access to general I/O. You just cannot delete file before reaching consensus between different parts of program on which file to delete. Or, you can match on the state of different channels, where matching requirements may include the presence and/or absence of specific kinds of data, not only in the heads, but also in the channel as a whole. When I read about Go channels and their matching semantics I was greatly disappointed with them.
Linear typing and borrow checking are all about environment manipulation. Introduction of linearly-typed object creates a unique (through the code) reference to that object in the environment and use of linearly-typed object removes that reference from the environment. Borrow checking can work similarly.
So abstract interpretation of the program implicitly uses state of environment and implicitly modifies it.
Such state monad with typed environment was possible in Haskell as early as 2009: https://blog.sigfpe.com/2009/02/beyond-monads.html
Sets of types (generalized records) were available in Haskell from 2004: https://okmij.org/ftp/Haskell/dependent-types.html#HList
Basically, it was possible to embed Rust-like language into Haskell from 2009 on, the ideas were all there.
The thesis that I continue to read is about dependencies. These dependencies control effects of the different parts of the program and one of the first more or less successful and practical way to control effects was monads in Haskell and, after that, monad transformers.
From my experience with Haskell, I more than love Software Transactional Memory, implemented as a monad without access to general I/O. You just cannot delete file before reaching consensus between different parts of program on which file to delete. Or, you can match on the state of different channels, where matching requirements may include the presence and/or absence of specific kinds of data, not only in the heads, but also in the channel as a whole. When I read about Go channels and their matching semantics I was greatly disappointed with them.