Idris isn't imperative (Haskell-like with dependent types), but offers features like those: http://docs.idris-lang.org/en/latest/effects/depeff.html http://doc

Idris isn't imperative (Haskell-like with dependent types), but offers features like those: http://docs.idris-lang.org/en/latest/effects/depeff.html 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 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/contrib/Control/ST.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/con... - https://github.com/idris-lang/Idris-dev/blob/master/libs/effects/Effects.idr 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).