[cinnamonheart]

Idris isn't imperative (Haskell-like with dependent types), but offers features like those:

http://docs.idris-lang.org/en/latest/effects/depeff.html

    readInt : Eff Bool [STATE (Vect n Int), STDIO]
                       [STATE (Vect (S n) Int), STDIO]

http://docs.idris-lang.org/en/latest/st/machines.html

    logout : (store : Var) -> ST m () [store ::: Store LoggedIn :-> Store LoggedOut]

They're both implemented within Idris, as libraries/modules, rather than being compiler magic:

- https://github.com/idris-lang/Idris-dev/blob/master/libs/con...

- https://github.com/idris-lang/Idris-dev/blob/master/libs/eff...

I think it'd be possible to write similar effect systems in other dependently typed languages like ATS, which is a relatively imperative language (C+ML-like).