The overall idea of using your type system to enforce invariants is called typeful programming [1]. The first few sentences of that paper are: "There exists a

The overall idea of using your type system to enforce invariants is called typeful programming [1]. The first few sentences of that paper are: "There exists an identifiable programming style based on the widespread use of type information handled through mechanical typechecking techniques. This typeful programming style is in a sense independent of the language it is embedded in; it adapts equally well to functional, imperative, object-oriented, and algebraic programming, and it is not incompatible with relational and concurrent programming." [1] Luca Cardelli, Typeful Programming, 1991. http://www.lucacardelli.name/Papers/TypefulProg.pdf http://www.lucacardelli.name/Papers/TypefulProg.pdf [2] https://news.ycombinator.com/item?id=18872535 https://news.ycombinator.com/item?id=18872535