[eyelidlessness]

The case I was trying to convey doesn’t narrow the actual type for anything outside its own function body. Any footgun that exists after the function call already existed before it. It just implies “I’m only looking at your keys not your values”.

[consilient]

> It just implies “I’m only looking at your keys not your values”.

That's what `unknown` is for. `any` behaves like `never` (in covariant positions), which is exactly the opposite.

[eyelidlessness]

I don’t think that’s how `any` behaves in any position, but I’d be happy to be corrected. Please show me how `any` is treated as `never`.

[consilient]

Here's a close to minimal example:

    const anyToNeverHelper = <T,>(t: any): number & T => t
    const absurd: never = anyToNeverHelper<never>(0)

[eyelidlessness]

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]

> 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]

> 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).

[TheCleric]

I gathered what you meant. My point is what stops the next developer working on your codebase from adding code in the body of your function that accesses the values of the object in an unsafe way?

[eyelidlessness]

A bit of trust. I’m not aware of a type system that protects my coworkers from my bad decisions, only those humans do that.