But what if we use predicate-based typing? Then your "type" will be something like `(x) ↦ (0 < x < ∞)`, holding true only if the value matches it. Then, given t

But what if we use predicate-based typing? Then your "type" will be something like `(x) ↦ (0 < x < ∞)`, holding true only if the value matches it. Then, given the type function is pure, the hypothetical compiler may somehow optimize them out most of the production code that can be statically analyzed...