That's not the correct link. Idris' ST is not the same as Haskell's ST. Haskell's ST is a way of introducing locally scoped mutability, which is indistinguishab

That's not the correct link. Idris' ST is not the same as Haskell's ST. Haskell's ST is a way of introducing locally scoped mutability, which is indistinguishable from immutability to an outside observer, but can offer better performance. Idris' ST is a way of implementing a state machine with statically checked state transitions. http://docs.idris-lang.org/en/latest/st/state.html http://docs.idris-lang.org/en/latest/st/state.html