Tracking state (sort of like Typestate) is not part of the type system, but you can encode it in the type system. So far, I've found this much more usable in practice than linear types, but I expect future work on linear types will change this, especially now that they're coming to GHC.

There's a tutorial on just this sort of thing here: http://docs.idris-lang.org/en/latest/st/index.html