facebook / flow

Adds static typing to JavaScript to improve developer productivity and code quality.
https://flow.org/
MIT License
22.08k stars 1.85k forks source link

Intersection type doesn't refine unions inside matching properties #5018

Open qm3ster opened 6 years ago

qm3ster commented 6 years ago

Reproducing using https://flow.org/try/

type Message = MessageEvent & {data: {
  file: {file: File}
}}
onmessage = function (e: Message) {
  if (e.data.file) {
    // do stuff with File
  }
}

Expected

:grinning:

Actual

property file Property not found in mixed

asolove commented 6 years ago

Have you tried using the type object spread operator, lik {...MessageEvent, data: whatever } ? When you want to combine two object types, that will work much better than intersection. Intersection of object types has a complex and unintuitive meaning that is rarely what you mean.

qm3ster commented 6 years ago

This works, thank you very much @asolove.

Why it is not as good

  1. It is less semantical, in my opinion, to say "object that contains everything MessageEvent instances contain, but data is a different type now" versus "object is a MessageEvent instance, and also is an object having a more specific data property value"(that is &-ed with mixed, not silently replaces it)
  2. It silently overwrites MessageEvent types!
  3. It does not check the class nominally, only taking its structure! ( :scroll: detailed experiment)

In conclusion, the Intersection method is often preferable, and it's just mixed that breaks it. (In my case, used in core dom.js defs) As such, this should probably be fixed.

Bug tl;dr

const a:{b: mixed} & {b: number} = {b: 1}
1: const a:{b: mixed} & {b: number} = {b: 1}
                                      ^ object literal. This type is incompatible with
1: const a:{b: mixed} & {b: number} = {b: 1}
                        ^ object type

  Property `b` is incompatible:
    1: const a:{b: mixed} & {b: number} = {b: 1}
                   ^ mixed. This type is incompatible with
    1: const a:{b: mixed} & {b: number} = {b: 1}
                                ^ number

:warning: Generalized to "union type in property breaks object intersection"

const c:{b: number | string} & {b: number} = {b: 1}
1: const c:{b: number | string} & {b: number} = {b: 1}
                                                ^ object literal. This type is incompatible with
1: const c:{b: number | string} & {b: number} = {b: 1}
                                  ^ object type
  Property `b` is incompatible:
    1: const c:{b: number | string} & {b: number} = {b: 1}
                            ^ string. This type is incompatible with
    1: const c:{b: number | string} & {b: number} = {b: 1}
                                          ^ number

Without object is fine

const a: mixed & number = 1
const c: number | string & number = 1
No errors!
asolove-stripe commented 6 years ago

Type intersection is a very tricky thing, and a number of the assumptions you make in here are not right if we were to write down the formal semantics of it. I don't know the details well enough to go that deep, but I will just say: if what you want is an object that contains the same properties as another object type, plus some more, use the type object spread. Intersection will occasionally work for simple cases, but you will eventually hit a very confusing problem. (And when you do, Flow will likely be right to complain, just for reasons that are pretty inscrutable.)

Now that I see that what you want is to narrow one property of the object type, rather than just add other properties, I'd advise against using intersection for that too. {foo: mixed} & {foo: number} is not the same as {foo: mixed & number }, even though it might seem that way intuitively. Also, because of variance, I think it won't be a subtype of either, so you can't pass it in to functions that want one or the other.

On the other hand, saying { ...{foo: mixed, bar: number}, ...{foo: number} } seems like what you want. It has the same type as the original, but just with the foo property's type replaced with a new, more specific one.

Maybe you can explain why you have an object type where you want to narrow one field, and we can try to find a solution to that. Because I don't think intersection is what you want. So if type spread doesn't do what you want, let's see if we can find another way.

qm3ster commented 6 years ago

Completely offtopic, but your "site" on your GitHub profile is http://Stripe (without .com or anything) @asolove-stripe

qm3ster commented 6 years ago

If I understand correctly, A & B means "all constraints of A and all constraints of B".

And it matches the intersection name perfectly:

I want my values to belong to both the set of MessageEvents and the set of { data: { file: File } }s (objects(1) that contain at least a property data(2) the value of which is an object(3) that contains at least a property file(4) the value of which is an instance of the File class(5))

To see examples of where destructuring the class type and overwriting a property is less safe than if union worked correctly, see my link in point 3. It comes down to the following looseness:

  1. Loosening/breaking types

    • By overwriting, you can assign an incompatible type or a less specific type.
    • By intersection, you can assign only an identical or more specific class.
  2. Not comparing class types nominally

    • By overwriting, you can assign any object that implements the class's mandatory properties.
    • By intersection, you can assign only real instances of the class.

More fun examples

const c: number & 1 = 1

Is 1 a number? Yes. Is 1 a 1? Yes. 1 is both.

const c: {a: 1} & {b: 2} = {a: 1, b: 2}

Is {a: 1, b: 2} an object with property a which contains a 1? Yes. Is {a: 1, b: 2} an object with property b which contains a 2? Yes. {a: 1, b: 2} is both.

const c: {a: 1} & {a: 1 } = {a: 1}

Is {a: 1} an object with property a which contains a 1? Yes. Is {a: 1} an object with property a which contains a 1? Yes. {a: 1} is both.

const c: {a: number } & {a: 1} = {a: 1}

Is {a: 1} an object with property a which contains a number? Yes. Is {a: 1} an object with property a which contains a 1? Yes. {a: 1} is ~both~ a dirty impostor. :warning:

asolove-stripe commented 6 years ago

Your intuitive understanding of what you want intersection to do isn't what it formally means. I don't want to go much further because it really is not worth trying to think this through informally. We can all go read type theory proofs of what intersection means, or we can accept that it's very rarely what we want, and basically never what we want for objects, and just go from there. (As someone who's used flow on several big projects, that strategy has worked well for me.)

(Based on my totally incomplete understanding: Formally, intersection is the dual of union. A union is a value that can be one of several types, at the choice of the code providing the value. An intersection is a value that can be one of several types, at the choice of the code consuming it. For objects, the intersection of two object types with the same property is not the same as an object type with the key-wise intersection. That is to say: {a: string} & {a: number} != {a: string & number}. Also, the subtyping rules don't work the way you'd expect because of variance and especially because non-exact object types are allowed to have other properties.)

qm3ster commented 6 years ago

I just wanted to narrow down MessageEvent in a WebWorker to valid incoming commands, so the payloads are defined at command surface and not deeper into the WebWorker script. Of course, I can change the definition of MessageEvent for my case, or just cast .data, but the point was that I revealed a bug, essentially, and in the best, most straightforward way of doing it as well.

At one point I thought that I really misunderstand Intersect Types, but enter flow-runtime, an independent implementation of the flow language for generating runtime typecheckers.

So, I invite you to:

  1. Open flow-runtime/try
  2. Disable annotations (we only need assertions)
  3. Paste the following:
    
    class A{
    data: number
    constructor(x){
    this.data = x
    }
    }
    class B{
    data: number
    constructor(x){
    this.data = x
    }
    }

type Intersect = A & {data: 1}

const a: Intersect = new A(1) // Passes :D const b: Intersect = new B(1) // Fails nominally const a2: Intersect = new A(2) // Fails structurally


4. [![Run](https://user-images.githubusercontent.com/10551234/31139460-4c7c808c-a87a-11e7-8d99-f011d9fce374.png)](#issuecomment-333920950) like hell
asolove-stripe commented 6 years ago

Frankly, I think the independent implementation got it wrong. The const a line ought to fail. Type intersection A & B means you can treat the item as either an A or a B. So in this case I could take your const a, safely pass it to a function expecting an A, and that function could set data to 2, which is something you are allowed to do to an A. If Flow allowed the const a line, it would have no way of preventing this from happening, but allowing it would mean that a is no longer a member of the intersection type.

In any event, I think this is the end of my contribution to this topic. You're welcome to keep thinking about it, but I've given the advice that I have, and I think neither of us understand the formal semantics of intersection well enough to be calling these things bugs.

qm3ster commented 6 years ago

Correction, I never intersected A & B, I intersected A & {data: 1} (A and an open object) A & B indeed is an empty set, like number & string And, as per documentation, these useless types complain when you try to use them, not when they are defined. In any case, thank you for your time.

asolove-stripe commented 6 years ago

But I'm saying that A & {data: 1} is an uninhabitable type. Because any instance of it could then be safely treated as an A, which would allow you to set data to any number, breaking type safety.

qm3ster commented 6 years ago

It would be an empty set if:

class A {
  data: string | boolean | {} | null | void
}

it would NOT be an empty set if:

class A {
  data: any | mixed | ( string | number ) | ( 1 | 2 | 3 )
}

In the latter cases it would be equivalent to

class A {
  data: 1
}

(Which is not useless at all, since the class can have countless other properties)

asolove-stripe commented 6 years ago

No, the intersection doesn't mean what you think it is equivalent to. Consider that if it behaved that way, you could do the following:

type A = {data: number};
type B = A & {data:1};

let b: B = {data: 1};

function setData(a: A){
  a.data = 2;
}
setData(b); // this is allowed since A & anything can be treated as an A

// now `b` is not a valid member of type `B`!
qm3ster commented 6 years ago

Just because something satisfies the constraints of A doesn't mean it doesn't have more constraints. It does. It is an intersect.

type A = {a: number}
type C = {a: number | string, d: boolean}
type B = A & C

function increment (a: A): void{
 a.a++
}

function incrementString (c: C): void{
 c.a++ // FAIL: must be a number 
}

function incrementAlthoughString (b: B): void{
 b.a++ // property refined through intersect
}

function murder (a: A): void{
 a.d=0 // FAIL: `A` doesn't have a `.d`
}

function murder (b: B): void{
 b.d=0 // FAIL: `.d` of intersection has to be `boolean`
}

function murder (c: C): void{
 c.d=0 // FAIL: `.d` of C has to be `boolean`
}

const b: B = {a: 1, d: true}
increment(b)
incrementAlthoughString(b)
popham commented 6 years ago

Swapping the order in your intersection eliminates the error, i.e.

declare class MessageEvent {
  data: mixed
}
declare class File {}

type Message1 = {data: {
  file: {file: File}
}} & MessageEvent;
const om1 = function (e: Message1) {
  (e.data.file.file: File); // No error
}

// versus

type Message2 = MessageEvent & {data: {
  file: {file: File}
}};
const om2 = function (e: Message2) {
  (e.data.file.file: File); // Error
}

If the intersection operation has a commutative property, i.e. A&B is equivalent to B&A for all types A and B, then there's a bug lurking in here.

Myself, I believe that the intersection operator should ban name collisions. I blame your problem on poor modelling of MessageEvent. It should probably be generic:

declare class MessageEvent<DataT> extends Event {
  data: DataT;
  origin: string;
  lastEventId: string;
  source: WindowProxy;
}

type WSDataT = string | Blob | ArrayBuffer;
type WSSendT = string | Blob | ArrayBuffer | $ArrayBufferView;
declare class WebSocket<RecDataT: WSDataT, SendT: WSSendT> extends EventTarget {
  // ...
  onmessage: (ev: MessageEvent<RecDataT>) => any;
  send(data: SendT): void;
  // ...
}

declare class Worker<RecDataT, PostT> extends EventTarget {
  // ...
  onmessage: (ev: MessageEvent<RecDataT>) => any;
  postMessage(message: PostT, ports?: any): void;
  // ...
}

declare class DedicatedWorkerGlobalScope<RecDataT, PostT> extends WorkerGlobalScope {
  onmessage(): (ev: MessageEvent<RecDataT>) => any;
  postMessage(message: PostT, transfer?: Iterable<Object>): void;
}

declare class SharedWorkerGlobalScope extends WorkerGlobalScope {
  // Oops. `onconnect` looks mismodelled in `lib/bom.js`
}

declare function onmessage(ev: MessageEvent<mixed>): any;
peter-leonov commented 6 years ago

Is this correct that the documentation on Intersections of object types contradicts a bit what is discussed in this issue. It states that types of colliding properties will also be intersected. Do I understand correctly, that it means recursive intersecting?

For me recursion does not work:

type A = {
  a: string
}
type B = {
  b: string
}

// works :)
let x1: A & B = {a: '', b: ''}

type PropA = {
  prop: A
}
type PropB = {
  prop: B
}

// works :)
let x2: { prop: A & B } = { prop: {a: '', b: ''} }

// breaks :(
let x3: PropA & PropB = { prop: {a: '', b: ''} }

flow.org/try

k commented 6 years ago

This does seem like a bug considering that

let x0: B = { a: '', b: '' };

does not error. That's the only way I could see this checking out.

sompylasar commented 4 years ago

Looks like what's confusing is the word "Intersection" in the "Intersection Types" concept name.

What is usually considered an intersection of two sets is the middle american-football-ball-shaped section. https://en.wikipedia.org/wiki/Intersection_(set_theory)

But according to the Flow Intersection Types documentation it's not that for Flow types. https://flow.org/en/docs/types/intersections/

excalidraw-202018205128

For example, flow.org/try

type A = { a: number };
type B = { b: boolean };
type C = { c: string, b: number };

// This one works as expected with set intersection:
(({}): (A & B));
// Expected no error (no fields in the intersection of A and B sets of fields),
// got no error.

// But the following ones do not!

(({ a: 1 }): (A & B));
// Expected error about extra property `a`,
// got error about missing property `b`.

(({ b: true }): (B & C));
// Expected no error (`b: boolean` is in the intersection of B and C sets of fields),
// got error about missing property `c`,
// and error about incompatibility of `b: boolean` and `b: number`.

(({ b: 1 }): (B & C));
// Expected no error (`b: number` is in the intersection of B and C sets of fields),
// got error about missing property `c`,
// got error about incompatibility of `b: boolean` and `b: number`.

(({ a: 1, b: true }): (A & B));
// Expected error about extra property `a`,
// got no error.

(({ b: true, c: 'c' }): (B & C));
// Expected error about extra property `c`,
// got error about incompatibility of `b: boolean` and `b: number`.

(({ a: 1, b: true, c: 'c' }): (A & B & C));
// Expected error about extra property `a`,
// got error about incompatibility of `b: boolean` and `b: number`.
dwelle commented 4 years ago

@sompylasar saw this on twitter, so just want to help clear this up to show that set theory still holds.

Not familiar with Flow, but in this case it seems pretty close to TypeScript.

The main misunderstanding (and something that both Flow & TypeScript docs don't explain for whatever reason) is thinking that { a: number } and { b: boolean } don't share values (and hence set-theoretical intersection should result in an empty set). But they do.

They are subsets (or subtypes) of a {} set, which is a set of all possible values (note, this is not the empty set, it's the exact opposite. An empty set, e.g. in TypeScript, would be denoted by never type).

In other words, the { a: number } is a subset of a set {} which implicitly contains a value of unknown (or something like top type/existential type -- not sure of the exact implementation here. We're getting into pretty abstract, type-theoretical waters here) type with a label of b (as it does contain any other possible values). So A & B basically does (for all intents and purposes, though implementation-wise, this is almost certainly not what's going on) an intersection of { a: number, b: unknown } & { a: unknown, b: boolean }, which results in { a: number, b: boolean }.

So, to reiterate again, the A, B types are subtypes/subsets of {} type, and that's why an intersection of them doesn't violate set theory principles.

image

(PS: I'm not an expert, and bet I've made many inaccurate statements here, so I'm happy to be corrected by anyone who actually knows what they're talking about!)

(PPS: as for why in Flow (({}): (A & B)); type-checks is beyond me --- it shouldn't, as {} is a superset of A & B, and supersets aren't assignable to subsets. Some Flow-specific quirk that goes against set theory in this case, I presume).