3 ms·

any and unknown are perfectly sound, if they were the only types then soundness would be automatic. The problem is that you can arbitrarily narrow types (and a

• price 2y ago
  That's true but misleading: if "any" and "unknown" were the only types, then "any" would be indistinguishable from "unknown" and you'd really have just the one type. Which makes the type system sound because it doesn't say anything. If your type system has at least two types that aren't the same as each other, then adding "any" makes it unsound right there. The essence of "any" is that it lets you take a value of one type and pretend it's of any other type. Which is to say that "any" is basically the purified form of unsoundness.
  • afiori 2y ago
    a typing of any cannot be unsound because it is always correct, narrowing any can be unsound.