microsoft / TypeScript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
https://www.typescriptlang.org
Apache License 2.0
100.75k stars 12.46k forks source link

Design Meeting Notes, 9/8/2017 #18339

Closed DanielRosenwasser closed 7 years ago

DanielRosenwasser commented 7 years ago

Reduce vacuous intersections

Export assignment

https://github.com/Microsoft/TypeScript/issues/17991 https://github.com/Microsoft/TypeScript/issues/16769

Revision to tagged template string emit

https://github.com/Microsoft/TypeScript/pull/18300

emit options:

Merge contextual types from overloads

https://github.com/Microsoft/TypeScript/pull/17819

Out of time

masaeedu commented 7 years ago

@DanielRosenwasser I don't know if TypeScript has warnings, but probably assigning never to anything should be a warning. The legitimate use case for it arises usually when you're exploding with an error where a value is expected, and seeing those places called out in some way has value in itself.

This kind of thing is also an issue in #4183

mihailik commented 7 years ago

Let's get back down on Earth for a second. This is a duck!

Playground sample below

type Circle = { radius: number };
type Square = { side: number };
var c: Circle & Square;
c. | <-- ctrl+space

The completion here shows both radius and side properties, which I find absolutely normal and expected.

This operation is represented by AND sign, the operation acts like an AND operation — stop calling it 'intersection' in public, and don't bend it towards being intersection. It's an AND. Read it out loud: Circle & Square

  variable c is both Circle and Square

The idea of collapsing non-overlapping types into never does not appear to carry a practical benefit. Neither of the referenced issues show a case where a likely bug would be eliminated by the collapsing to never.

On the other hand, keeping the current behaviour and building upon it does have benefits in expressiveness. Consider code like this (real life example):

function formatDate(date: Date): JSX.Element | string {
  var result = <span>  fancy date format with colours and whistles  </span>;
  result.toString = result.valueOf = () => plain text date format
  return result as any;
}

This is meant to produce 'a thing' that can be used both as React element, as well as string.

It would really help to have a simple mental model for this level of set/category theory expressions.

masaeedu commented 7 years ago

@mihailik The reason these things are called intersection/union has its roots in set theory. If you think of types as sets that are inhabited by values, an intersection of two types can accommodate values from the intersection of the sets of values each type can accommodate.

You may not personally have encountered a use case for collapsing these types, but it is a sound thing to do from the type system perspective and has practical uses. See for example this question where a user became confused precisely because a string & number intersection arose in a non-obvious way.

The reason it is sound to do is again easy to see if you think of intersections as actual intersections. An intersection of two disjoint sets (two types with mutually exclusive sets of values) is identical to the null set (the never type).

For the circle/square example you gave, the proposal doesn't cause any issues. Only if there is an identical property on both with mutually exclusive types (e.g. { kind: "circle" } & { kind: "square" }) does the vacuous type reduction produce { kind: never }.

mihailik commented 7 years ago

@masaeedu readability is a value in itself, set theory is only a tool. Besides, to satisfy set theory we can just stop calling & intersection, and instead call it Liskov-principle operator.

But great point bringing up the StackOverflow question!

However it doesn't look like the problem there is with &, unless the suggestion is to completely change the meaning of it. The same disconcerting typing behaviour applies without primitive types:

Playground link

interface Thing {
    name: string;
    age: HTMLElement;
}
var oldThing: Thing;

let newThing: Thing = Object.assign({}, oldThing, {
    age: XMLHttpRequest  <-- no problem???
});
RyanCavanaugh commented 7 years ago

We're talking about non-intersecting unit types here; the non-unit-type Circle & Square remains fine and we continue to assume the possible existence of a Squircle. Critically, the types you have defined there don't have a discriminating unit type key that would prevent the existence of Squircle.

This is about types like (0 | 1) & (1 | 2) -- the sole constituent of that set is unambiguously 1 and it makes perfect sense to collapse this type.

mihailik commented 7 years ago

@RyanCavanaugh helpful distinction! Within narrow use case of & over non-empty intersection of unit types it makes sense.

Empty intersection and & with non-unit types should never be collapsed.

Playground link

type A: 0 | 1;
type B: 2 | 3;

// . . . much later in different area of code

var quirk: A & B;
quirk = 1;
~~~
Type '1' is not assignable to type '(0 | 1) & (2 | 3)'.   <-- much easier to track and fix than:
Type '1' is not assignable to type 'never'.

Note that the current TS compiler produces muddy error message: Type '1' is not assignable to type '(0 & 2) | (0 & 3) | (1 & 2) | (1 & 3)'.

Don't replace the mess with never, replace it with the original notation: if collapse produces empty, abort collapsing and use type notation from the actual source.

RyanCavanaugh commented 7 years ago

We agree. This logic will simply reduce (but never eliminate to 0 / create a top-level never) the number of output constituents when performing the expansion rules over union types.

masaeedu commented 7 years ago

@RyanCavanaugh For the type { kind: 1 } & { kind: 2 }, will the resulting type be { kind: 1 & 2 } or { kind: never }? Will it be different from the result of declare const x: 1 & 2; const obj = { kind: x }?

RyanCavanaugh commented 7 years ago

For all intersections of non-union types, the behavior is unchanged. This is only about removing "impossible" intersections that appear when applying the intersection distributive rule over union types. In the simplest form, the change is that A & (B | C) will become A & B, rather than (A & B) | (A & C), when the type A & C is known to be the empty set of values (e.g. 1 & 2)

masaeedu commented 7 years ago

@RyanCavanaugh The notes say:

So for certain types (e.g. number & string or "foo" & "bar"), it makes sense to collapse them down to never.

You seem to be saying this is not what you will do. So in your example, when both A & B and A & C are known to be the empty set of values, what is the result? Will you keep allowing people to assign 1 to a reference of type 1 & 2, instead of flagging a problem?

DanielRosenwasser commented 7 years ago

@masaeedu a few lines below:

So maybe we don't want to go all the way there. But for unit types, we certainly care.

masaeedu commented 7 years ago

I was assuming by "unit types" you meant primitive types like 1, 2, number etc. Is "unit types" actually unions?

DanielRosenwasser commented 7 years ago

Nope, it doesn't include unions. A unit type is a literal type (string literals, numeric literals, true, false, undefined, null) or an enum member type.

mihailik commented 7 years ago

The way I understand the edge case algebra here,

var oneAndTwo: 1 & 2;

oneAndTwo = 1; // fail, '1' is incompatible with '2' in '1 & 2'

takeOne(oneAndTwo); // OK, '1 & 2' is both '1' and '2' at the same time, satisfies '1'

function takeOne(x: 1) { }
masaeedu commented 7 years ago

@mihailik Thanks, that's a good example. So @DanielRosenwasser given that 1 and 2 are unit types here, and we care about unit types, shouldn't we be getting a warning or never type or something when we declare var oneAndTwo: 1 & 2? It isn't just an error to assign 1 to oneAndTwo, it's an error to assign any kind of value whatsoever, and yet you're able to pass it where a concrete 1 is expected.

RyanCavanaugh commented 7 years ago

It's not a useful road to go down.

If you go with the simpler form of "Don't allow those types to be written", you're not really helping anyone who needs help -- no one has shown up here with a mistake caused by accidently writing an uninstantiable intersection type.

If you go with the harder form of "Don't allow an instantiation of an uninstantiable type", you quickly find yourself in bad cases. What if someone has something like this?

type One = { x: 1 };
type Alpha = { a: string; z?: One };
type Two = { x: 2 };
type Beta = { b: string; z?: Two };
type AB = Alpha & Beta;

Well now the property AB.z has the impossible type One & Two because One & Two's x property has the impossible type 1 & 2. So we should just forbid the declaration of AB...? But the property is optional, so maybe the intent here is that z actually must always be undefined. And now we have to have some crazy logic that tracks whether or not any given type is necessarily instantiated in the context in which it was created. And since generics mean these types can come out of anywhere, you get into cases where function calls are erroring because they inferred an uninstantiable type, which is going to be extremely difficult to diagnose.

masaeedu commented 7 years ago

You're asking whether ((One | undefined) & (Two | undefined))["x"] should be never. This is the very case you were originally talking about, i.e. distributing over unions. The special casing would be required to preserve One & Two, i.e. to preserve at least one out of a number of impossible intersections.

In the case here it very straightforwardly reduces via distribution to:

Hence the intuitive sense that "z actually must always be undefined".

And no, you shouldn't be able to access AB.z.x, because there is never any valid way to construct a value for Alpha & Beta that will have an x property.

Anyway, I feel like I'm hijacking the thread here so maybe I'll open an issue about it later or write it in my diary or something.

EDIT: Messed up the algebra the first time, fixed.

masaeedu commented 7 years ago

Re: rules above, pretty sure it is appropriate for T | never to be T, since never is the empty type; happy to be corrected.

mihailik commented 7 years ago

@masaeedu collapsing nonsensical type to never is a bad idea primarily because it reduces useful error messages to triviality, with little clue where that never came from.

masaeedu commented 7 years ago

@mihailik If you get a warning wherever absurd types arise (One & Two) is ({ x: 1 } & { x: 2 }) is { x: 1 & 2 } is { x: never }, you're not left in the dark.

mihailik commented 7 years ago

I think RyanCavanaugh already went through that question above.

Here: https://github.com/Microsoft/TypeScript/issues/18339#issuecomment-333948799

It's not a useful road to go down...
masaeedu commented 6 years ago

@mihailik I responded to that comment above. The argument that reducing impossible intersections to never leads you to bad cases is so far unsubstantiated by example. On the contrary, his example shows that very straightforward never-reduction actually leads to good results, catching subtle bugs like accessing z.x in the example above.

Coupled with good error reporting that reflects the steps it walked through in the reduction, this is a useful tool in many scenarios.