Example:
if (ptr == NULL) {
... a ...
} else {
... b ...
}
In branch a and branch b, different invariants about ptr hold. But the language/compiler are not verifying any of these invariants.Instead, consider:
data Maybe a = Nothing | Just a
This defines a type "Maybe", parameterized by a type variable "a", and it defines two "data constructors" that can make a Maybe value: "Nothing" which contains nothing, and "Just" which contains a value of type "a" inside it.This is known as a "sum" type, because the possible values of the type are the sum of all data constructor values.
We could still use this sum data-type in a boolean-blind way:
if isJust mx then
.. use fromJust mx .. -- UNSAFE!
else
.. can't use content of mx ..
However, using pattern-matching, we can use it in a safe way. Assume "mx" is of type "Maybe a": case mx of
Nothing -> ... There is no value of type "a" in our scope
Just x -> ... "x" of type "a" is now available in our scope!
So when we branch on the two possible cases for the "mx" type, we gain new type information that gets put into our scope."Maybe" is of course a simple example, but this is also applicable for any sum type at all.
If your language does branching without giving you back any new type information, it means you have to manually track the invariants and conditionals your program is in. If you get it wrong, your program will die at runtime. Instead, the language can almost always provide you some kind of proof that you can pass along of the conditional's truthness, which makes it safe to rely on it.