Design Meeting Notes, 1/3/2024

[DanielRosenwasser]

Intersections and Unions that Depend on Instantiation Order

#56906

type Union<A, B> = A | B
type UnionAny<T> = Union<T, any>
type UnionUnknown<T> = Union<unknown, T>

// these should all be the same type but are respectively: any, any, unknown 
type UA0 = Union<unknown, any>
//   ^?
//   any
type UA1 = UnionAny<unknown>
//   ^?
//   any
type UA2 = UnionUnknown<any>
//   ^?
//   unknown

• any "eats" everything.
• unknown does too, except for any.
  • Problem is that we say SomeUninstantiatedTypeVariable | unknown, we eagerly reduce that to unknown.
  • We would need to defer union reduction in the presence of generics and unknown or any.
    • That would be very annoying - you wouldn't be able to say that unioning with the top type(s) just reduces to the top type.
    • [[Editor note]]: probably also have to thread through contexts where you have to know when to reduce the type.
• It certainly is an inconsistency, but did it come up in a practical context?
  • That is unclear.
• Conclusion: we admit that it is inconsistent and undesirable, but we are not fully convinced that it needs to change.

Disallowing More Property Access Operations on never-Typed Expressions

#56780

• From a purely type-theoretic standpoint, there is no issue with accessing a property on never, the issue is arguably more that the code is unreachable.

• Could argue that you should say "this whole block is unreachable, so why do you have code?"

• That is too heavy-handed - the following doesn't deserve an error, does it?

  function foo(x: "a" | "b" | "c"): string {
    switch (x) {
      case "a":
      case "b":
      case "c":
        return "hello";
      default:
        throw Debug.fail("Wrong value " + x);
    }
  }

• Two common views of never are

  • "Consuming" a value of type never to enforce an exhaustiveness check.
  • "Probing" a value of type never to report a helpful error for a violation of the type system or usage from untyped code.

• In practice, this change actually breaks a bunch of existing code.

• Conclusion: feels like we don't have an appetite

Preserving Type Refinements Within Closures Past Their Last Assignments

#56908

• Fixes lots of issues that get duped to Trade-offs in Control Flow Analysis #9998.

• When a closure is created after all assignments to some closed-over variable, then you can effectively think of that variable as unchanging.

• Effectively safe to preserve the type-assignments so long as the closure isn't hoisted.

  • Means things like object methods, function expressions, and class expressions can observe prior type narrowing/refinment.
  • In theory, class declarations could also be made to work here.
    • We noticed that class declarations were considered "hoisted"...but they're not!

• Note that we don't quite narrow in a lexical manner within "compound statements". We use the "end" of the compound statement as the source of the last assignment.

  function f5(condition: boolean) {
      let x: number | undefined;
      if (condition) {
          x = 1;
          action(() => x /*number | undefined*/)
      }
      else {
          x = 2;
          action(() => x /*number | undefined*/)
      } // <- we consider this to be the position of the last assignment of 'x'
      action(() => x /*number*/)
  }

  • This approach lends to a fast and efficient check.
  • It would also be tricky in the case of loops, where the "last" assignment cannot truly be determined.

• Variables that are referenced in closures past the last assignment do not necessarily trigger an implicit any warning anymore.

  let x;
  
  x = 42;
  doSomething(() => x));
  //                ~
  // Implicit any error! ❌
  
  x = "hello!";
  doSomething(() => x));
  // No error! ✅

• If we limit to let and parameters, then we don't have any issues with our perf suite - but it does for var on monaco.

  • We might have other analyses we can apply.

• Function declarations in block scopes should maybe have captured variables appropriately narrowed.

  function f(x: string | number) {
      if (typeof x === "number") {
          function g() {
              x // should this be number, but is not in the PR
          }
          return g;
      }
  }

[fatcerberus]

It seems like when it comes to never, about half of people expect any operation on never to be an error (e.g. #56952), which makes some sense because it's indicative of unreachable code (assuming that nobody's lied to the type system), while the other half would be just as surprised to see it not act like the bottom type that it actually is.

For what it's worth: If I speak with my type theory hat on, I would really prefer it to act as a proper bottom type (everything is permitted, ex falso quodlibet, etc.), but in actual practice that might make it act too much like an any for comfort, so ultimately I think TS should keep being pragmatic about it. It's a tricky issue for sure.

[rotu]

never is not the same as the bottom type, which is not the same as an empty type. I think it's a mistake to conflate these!

1. empty type = there are no values of this type. E.g. true & (()=>1). You can't expect the type system to recognize every empty type as empty. You can also have higher-order empty types, e.g. <T,>()=>T.
2. bottom type = a subtype of all types. If the subtype relation is defined by "assignability" then any value is assignable to this type this type is assignable to any other type. Such a type is not guaranteed to exist --- for example, you might have a sort of mustuse type that requires its value to be used instead of discarded.
3. never = one particular type constant. It happens to be a bottom type and happens to be empty.

I think there is room for carving up never further. For instance a type that represents "an expression which, when evaluated, results in a runtime exception" or "an expression which, when evaluated, never terminates".

There's also the possibility of an "oopsies" type - a type that actually means "if any expression is deduced to be this type, then the programmer has made a mistake". I think that's something that should be introduced instead of having so many hardcoded errors in the type checker!

[fatcerberus]

This is all off-topic, but well, you've successfully nerd-sniped me 😛

I suppose in an arbitrary category a bottom object doesn't necessarily have to be an empty one - but in Set (which models most type systems pretty well, at least from the point of view of assignability), there's really only one bottom object - the empty set. In TS, that's never, the type to which no values are assignable.

bottom type = a subtype of all types. If the subtype relation is defined by "assignability" then any value is assignable to this type.

That's the top type (unknown in TS). The bottom type is the one that's assignable to everything else (because it's a subtype of all other types).

I think there is room for carving up never further. For instance a type that represents "an expression which, when evaluated, results in a runtime exception" or "an expression which, when evaluated, never terminates".

In a language without typed exceptions, that distinction seems academic.

There's also the possibility of an "oopsies" type

This is in fact something a lot of people would like; see #23689.

P.S. don't ever try to fit any into a coherent type theory. It'll get you nowhere and give you a splitting headache 😉

[rotu]

This is all off-topic, but well, you've successfully nerd-sniped me 😛

I suppose in an arbitrary category a bottom object doesn't necessarily have to be an empty one - but in Set (which models most type systems pretty well, at least from the point of view of assignability), there's really only one bottom object - the empty set. In TS, that's never, the type to which no values are assignable.

I want to push back against the identification of types and sets. A type judgement means “if you have a value of this type, here’s what you know about it”.

In most type theories, you don’t have a unique empty type. In fact, [never], [never, never], etc. are not and should not be considered the same as never because:

1. you can have expressions which throw an error instead of evaluating.
2. due to assignability rules, these can form useful bounds on the structure of a value.

There is only one bottom value unique set of values of empty type but expressions are not values. And TS assigns types to expressions, not just values! It’s especially important when considering short-circuiting operators &&, ||, ??, ?., etc.

That's the top type (unknown in TS).

You’re right. I mistyped.

In a language without typed exceptions, that distinction seems academic.

In a language that might want to include typed exceptions in the future, it’s certainly not :-)

[fatcerberus]

Sure, types are not sets. I just meant that Set is a useful (if not 100% accurate) model for assignability of types, not for type systems in general. Set theory and type theory are separate for a reason :)

There is only one bottom value

There are no bottom values. That's the whole point of having a bottom type - if you think you have such a value, the program must have already diverged (stuck in an infinite loop, terminated abnormally, threw an exception, etc.). That's explicitly why it can act as a subtype of everything - because the program diverged, the code with the bottom "value" will never execute so it can safely do anything it wants with it with no ill effect. It's the type theoretical analogue of the principle of explosion; the contradiction from which to "prove" anything arises from assuming the unreachable code is reachable.

In most type theories, you don’t have a unique empty type. In fact, [never], [never, never], etc. should are not never because:

When you start speaking at this level of abstraction, it's really difficult to say what things are¹. We can only really say that [never] or { x: never } or whatever are isomorphic to never, and even then only if we consider them in the context of set theory (i.e. they all map to the empty set). As types in the TS type system, they are certainly distinct; I can't argue with that.

Anyway, all this theoretical talk is fun, but we maybe should stop clogging up a thread meant for more practical discussion of how to implement things with it. I'd recommend joining the TS Discord channel if you haven't already; then you can have discussions like this all day :)

Footnotes

1. "The riddle is solved when the pillars fall." ↩

[rotu]

There is only one bottom value

There are no bottom values.

You caught me. That's what I get for not checking what I type :-). I meant "there is only one set of values of an empty type"

That's the whole point of having a bottom type - if you think you have such a value, the program must have already diverged

No. That's the point of having an empty type which is known to be empty and expressible in the type theory. A bottom type is a subtype of all types. Both never and any are bottom types.

---

Here's the practical bit. Ideally, the "intersection"/"union" should give the unique lower/upper bound of types. But the type operators &/| can't hope to satisfy this because:

1. the intersection of two callable types is intentionally construed as an overloaded function, not as an intersection of sets of callable objects
2. Intersection, Union depends on type variable instantiation order #56906. The bound of even a finite set of types is not unique when generics are involved.

Arguably:

3. Distributivity of exists over union means that a union of all sets of values is not equivalent to the upper limit of the union of all values, i.e. unknown.

[fatcerberus]

any really doesn’t count IMO because it’s more a flag to tell the type system “don’t typecheck this thing” than it is a proper type. The only way I could try to fit it into a theory is to say that it’s “deus ex machina: the type” but even that gives me a headache 😉

Is there any type system in existence where the (strongly typed) “subtype of all types” bottom type isn’t also empty? AFAICT that always must be the case because subtype hierarcheries diverge - the intersection of “the set of all cats” with “the set of all giraffes” is already necessarily empty, and that’s just two types, let alone finding the common subtype of everything in existence.

Finding abstractions is fun, but at some point you do have to ground yourself back in reality to get any work done.

[rotu]

"deus ex machina: the type"

I like to think of any as the "hold my beer" type :-).

Is there any type system in existence where the (strongly typed) “subtype of all types” bottom type isn’t also empty?

Kinda. C has void * which is assignable to any pointer type. It is the bottom type of all pointer types. And it is inhabited by the null pointer.

Most type systems don't have a bottom type e.g. you may have completely separate hierarchies for structs and for functions with no common subtype. Or e.g. there may not be a subtype relation at all!

You're right that if a type system (1) has some empty type and (2) has a bottom type, then (3) that bottom type be empty.

Finding abstractions is fun, but at some point you do have to ground yourself back in reality to get any work done.

Of course you could use that argument to say "there is no need for a never type because types describe values and there's no value you need it to describe". Or go a step further and say "types are erased at runtime, so there's no need for them!"

The big picture problem as I see it is that so much of TypeScript is defined by its current implementation, not a language spec or some categorical characterization of how it should work. If two programmers disagree about what never means, then a type annotation involving never cannot be used to effectively communicate!

[fatcerberus]

Of course you could use that argument to say "there is no need for a never type because types describe values and there's no value you need it to describe". Or go a step further and say "types are erased at runtime, so there's no need for them!"

Oh for sure, I didn't mean to imply we shouldn't have abstractions at all, just that at some point you do have to apply them, and from what I could tell the conversation was headed in the direction of pure head-in-the-clouds abstraction, so I wanted to bring things a bit more down to earth by putting it in context. Kind of a "have your head in the clouds but your feet on the ground" sort of deal.

The big picture problem as I see it is that so much of TypeScript is defined by its current implementation, not a language spec or some categorical characterization of how it should work.

Indeed, which is why I think stressing too much over abstractions like type theory, referential transparency, etc. is misguided, at least where TypeScript-the-compiler is concerned. TS used to have a specification, a long time ago, but has since outgrown it and the direction of the project is now primarily guided by pragmatism. In the (probably paraphrased) words of @RyanCavanaugh, "consistency is a proxy measure, not an end goal" for TypeScript.

By the way, you might find this interesting (or distressing, depending on your disposition w.r.t. applicability of type theory):

• TypeScripts Type System is Turing Complete #14833

[DanielRosenwasser]

In fact, [never], [never, never], etc. are not and should not be considered the same as never because:

1. you can have expressions which throw an error instead of evaluating.
2. due to assignability rules, these can form useful bounds on the structure of a value.

I don't know if I feel like a distinction around (1) has weight as much as (2). It feels like I've definitely encountered the latter, but can't immediately come up with an example. Maybe "I promise never to call this constructor" sort of stuff with abstract classes

I'm coming back to this point because I've written lots of design meeting notes where we end up claiming that "object types containing never should produce nevers", but we only avoid doing so because it might break other assumptions in the type system (e.g. instantiation of type variables in an object type always produces an object type), or it might be expensive/unreasonable in practice (e.g. discovering nevers produced by intersection types requires eager exploration of each constituent's properties, which might require unbounded exploration to discover conflicts).

[fatcerberus]

Oh great, we nerd-sniped one of the maintainers now 😅

[DanielRosenwasser]

Oh, also the UX is worse if you collapse a type containing never to never. We had to special-case stuff like the following:

declare function merge<const T, const U>(a: T, b: U):
  { kind: T } & { kind: U };

merge("hello", "world").kind
//                      ~~~~
// Property 'kind' does not exist on type 'never'.
//  The intersection '{ kind: "hello"; } & { kind: "world"; }'
//  was reduced to 'never' because property 'kind' has conflicting types in some constituents.

[DanielRosenwasser]

^ and actually, I think that's a great example of why we should give an error on never usage in some capacity - something went wrong upstream and you really need to know about it.

[rotu]

Indeed, which is why I think stressing too much over abstractions like type theory, referential transparency, etc. is misguided, at least where TypeScript-the-compiler is concerned.

Theory vs praxis is definitely a balancing act, I'll give you that!

I do think referential transparency is critically important, not just academic. I don't expect the JavaScript to be referentially transparent, but I do expect generics to result in equivalent types, given equivalent input types and context. #56906 for example seems like unreasonable behavior because of this.

Here's an example where extends is not referentially transparent. As you can see, Z1 and Z2 both wind up calling E the same way, but resolve to different types. This makes it hard to reason about what E "means" and means that I have zero confidence my program will work the same way in future versions!:

type E<X> = X extends 0 ? true : false // type E<X> = X extends 0 ? true : false
//   ^?
type EU<X, Y> = E<X|Y>   // type E<X, Y> = E<X> | E<Y>
//   ^?
type Z1 = EU<unknown, 0> // type Z1 = boolean
//   ^?
type Z2 = E<unknown | 0> // type Z2 = false
//   ^?

playground

[fatcerberus]

I don’t know what more I can say re: referential transparency other than to repeat what I’ve heard from maintainers in the past (again, paraphrasing): “it’s expected that writing different code yields different results”. While RT would be nice to have, it’s probably not a fruitful pursuit, given that.

[rotu]

it’s expected that writing different code yields different results

No, it's expecting four + 1 == 5 whether you got the value as four = 2+2 or four = 3+1. Different code can yield different results, but the same code operating on equal inputs should give equal results.

[fatcerberus]

Here's a good example of what I'm talking about: #51551

Quoth @RyanCavanaugh:

When specifying expected behavior, "the same" isn't really actionable. "These two slightly different things should behave identically" quickly runs into transitivity problems -- A1 is close to A2 is close to A3 is close to A4 so each step should be "the same", but if A1 and A4 have manifestly different desirable behaviors, then something has to give somewhere.

[rotu]

Here's a good example of what I'm talking about: #51551

That doesn't bother me so much. An implied type attributed to an untyped expression is subject to fuzzy judgement.

That's very different from a generic type expression. I do expect equational reasoning and compositionality to hold for closed-form type expressions, just as I expect for algebraic expressions.

I would maybe expect some wiggle room for infer (which makes no promises about maximality).

[Conaclos]

typo: s/2023/2024/