Hacker News new | ask | show | jobs
by afiori 699 days ago
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 any can narrow to any type) eg: https://www.typescriptlang.org/play/?#code/DYUwLgBAzg9grgOwC...

1 comments

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.

a typing of any cannot be unsound because it is always correct, narrowing any can be unsound.