For those interested in pursuing this idea even firther, may I recommend Type Driven Development with Idris by Edwin Brady.
Idris uses dependent types that allow the state types to carry additional information. I implemented a system for handling files where the open file state type conveys in what mode the file was opened. This prevents code that tries to write to read-only files from even compiling.
It also prevents duplicate code as the read function is automatically available for any file that’s opened in a mode that allows reading.
F* also supports dependent and refinement types, if you like F# but also want to take it a little deeper down the functional rabbit hole.
You don’t necessarily need to use dependent types for that. In Rust, you can use tagging through generics for that.
Some state machine libraries rely on that.
Not to take away the point, dependent types make that a lot easier. The strategy can (and should) be followed in other languages, though.
This is my favorite aspect of strict, static typing. Let the computer do the thing it’s really good at: doing repetitive tasks quickly and reliably. The compiler literally won’t let you make certain mistakes. That’s an amazing tool! Use it to your advantage!