This is a good example of how `never` is treated as `never`. Everything is assignable to the bottom type and intersecting with it will always be the bottom type, by definition. It’s also a good example of how the top type `any` casts to whatever you choose, because that’s also by design. Both types are vacant, the bottom type is infectious. That’s a good thing. And it works the same way with `unknown`, which it also should because once something is known to be part of the null set it should stay known as the null set.
Other way around: everything is assignable to the top type (`unknown`), and the bottom type (`never`) is assignable to everything.
> It’s also a good example of how the top type `any` casts to whatever you choose
Which is precisely why `any` isn't the top type: if you allow `any`, then types no longer form a lattice, and there is no bottom or top.
If you restrict yourself to a sound fragment, then `unknown` is the top type. Compare `(x: unknown) => boolean` (two inhabitants up to function extensionality) to `(x: any) => boolean` (infinitely many inhabitants).
> And it works the same way with `unknown`, which it also should because once something is known to be part of the null set it should stay known as the null set.
But `unknown` isn't the null set: it's the "set" (insofar as we're pretending that types are sets of values, which isn't quite true) of all terms.
> Other way around: everything is assignable to the top type (`unknown`), and the bottom type (`never`) is assignable to everything.
Yep, sorry that’s what I meant.
> Which is precisely why `any` isn't the top type: if you allow `any`, then types no longer form a lattice, and there is no bottom or top.
I’m not sure I understand.
> If you restrict yourself to a sound fragment, then `unknown` is the top type. Compare `(x: unknown) => boolean` (two inhabitants up to function extensionality) to `(x: any) => boolean` (infinitely many inhabitants).
Sure, but I was referring to an exception I make for ignored parts of a type, in a type param. This example would be more analogous as:
Which I hope makes my exception more clear, even if you don’t agree with it. It hopefully communicates that x is of interest and rest is not.
> But `unknown` isn't the null set: it's the "set" (insofar as we're pretending that types are sets of values, which isn't quite true) of all terms.
I was referring to never as the null set. Once you narrow anything—any, unknown, etc—to never, you can’t widen it to anything (without an unsafe cast of course).
