"In computer science, an invariant is a condition that can be relied upon to be true during execution of a program, or during some portion of it. It is a logical assertion that is held to always be true during a certain phase of execution. For example, a loop invariant is a condition that is true at the beginning and end of every execution of a loop."
I didn't mean it in any more specialized sense, except that there will always exist some invariants that can't be statically enforced (Halting problem). That said, there are lots of things that types can enforce - that's what types are good for (and they are spectacularly good things).
"In computer science, an invariant is a condition that can be relied upon to be true during execution of a program, or during some portion of it. It is a logical assertion that is held to always be true during a certain phase of execution. For example, a loop invariant is a condition that is true at the beginning and end of every execution of a loop."
I didn't mean it in any more specialized sense, except that there will always exist some invariants that can't be statically enforced (Halting problem). That said, there are lots of things that types can enforce - that's what types are good for (and they are spectacularly good things).