In the ML-type-system community, enforcing invariant through typing has mostly been discussed, as far as I’m aware, informally, and is part of the language communities folklore. There have been publications centered on the use of richer features (than the base ML type systems), with examples that fit into your description. So pick any advanced type-system feature X (phantom types, GADTs, polymorphic variants, private types, higher-order polymorphism) and you will find examples of “how X allows to write Y in a safer way”. Some examples:
- François Pottier and Yann Régis-Gianas used GADTs to encode the stack shape of a LR parser, getting safer, more efficient generated parsers as a result: Towards efficient, typed LR parsers
- Martin Sulzmann and Razvan Voicu added general Constraint Handling Rules to GADT in the Chameleon and were able to encode even more sophisticated invariants in the type system. Such use of constraint/logical programming at the type level was however not adopted in the mainstream ML languages. Language-Based Program Verification via Expressive Types
- Chung-chieh Shan and Oleg’s “Lightweight Static Capabilities” presents several examples of phantom types and a general design method to use them to enhance program safety: Lightweight static capabilities
- The ST monad in Haskell, initially described by Simon Peyton-Jones and John Launchbury, is a very clever use of higher-order polymorphism to make the system prove that some simple but common cases of internal use of mutable state are observably pure: State in Haskell
Fluet and Morrisett expanded this idea to represent full-fledged region types in a sufficiently expressive ML type system. See the maybe-practical examples by Oleg: Region-based resource management
- “regular types” being used to describe expressive static types about XML data CDuce
There are two other related communities discussing the use of types for program correctness. The obvious candidate is the community advocating programming with dependent types (using Coq, Agda, Epigram, Cayenne, Guru, etc.). They have plenty of literature on how you can use dependent types to get full functional correctness as a result of type-checking — the price to pay being very subtle and difficult programming. See for examples the long list of “Papers using Agda” here: Agda Wiki
The less obvious community is the fraction of the people working on retrofitting static analysis into dynamically typed languages. This is difficult because the programs that are written tend to falsify a lot of the simplifying invariants typed programmers respect and use to reason about (such as the fact that all elements of a list have the same type), and you need relatively powerful and forgiving type systems to accept that. Furthermore, people working in this area have a hard time selling the idea to their larger community, so they tend to use examples, case studies, killer applications, etc... See for example: Sam Tobin-Hochstadt work on Typed Racket
- the work on Dyalizer, a static analasys tool for Erlang, based on a kind of “optimistic typing” that only rejects programs that are provably wrong, instead of only accepting programs that are provably safe.
A part of what Dialyzer allows is to write type annotations for Erlang functions; the methodology of incrementally adding annotations/specifications to increase confidence in a program is described in the paper “Gradual Typing of Erlang Programs: A Wrangler Experience”, by Konstantinos Sagonas and Daniel Luna.
The DIALYZER: a DIscrepancy AnaLYZer for ERlang programs;
Gradual Typing of Erlang Programs: A Wrangler Experience