5 ms·

Here's a close to minimal example: const anyToNeverHelper = <T,>(t: any): number & T => t const absurd: never = anyToNeverHelper<never>(0)

eyelidlessness 4y ago
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.
- consilient 4y ago
  > Everything is assignable to the bottom type 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.
  - eyelidlessness 4y ago
    > 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: <T extends (x: unknown, ...rest: any[]) => boolean> 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).

eyelidlessness 4y ago

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.

consilient 4y ago
> Everything is assignable to the bottom type 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.
- eyelidlessness 4y ago
  > 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: <T extends (x: unknown, ...rest: any[]) => boolean> 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).