Re:TypeScripting the Technical Interview
by eyelidlessness on Monday March 13, 2023 @12:47PM
(#35138368)
> 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).
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).