Flow: Array.prototype.find and refinement

[amasad]

This probably belongs as a comment on some other larger issue with refinement. I run into things like this all the time where it seems like Flow should get the refinement right but it doesn't.

/* @flow */

const arr = ['a', 'b'];
let n: ?number = null;

if (arr.find((item, index) => {
  n = index;
  return item === 'b';
})) {
  logNum(n); // Flow should know `n` is a number but it doesn't
}

function logNum(num: number) {
  console.log(num)
}

Flow output:

10:   logNum(n);
             ^ Cannot call `logNum` with `n` bound to `num` because null or undefined [1] is incompatible with number [2].
References:
4: let n: ?number = null;
          ^ [1]
13: function logNum(num: number) {
                         ^ [2]

[wchargin]

Note that find is just a normal function with a normal type signature.
Flow doesn’t know anything special about how it behaves; it just knows
that it has the following type:

https://github.com/facebook/flow/blob/47f0e86646e3e93ab6d97795f12c3a2072cb4946/lib/core.js#L206

You’ve provided find with a callback that, when invoked, sets n to a
non-null number. But Flow doesn’t know that find will invoke that
callback. Indeed, find _won’t_ invoke that callback if the array is
empty. So, to witness that your code is safe, Flow would need to
understand the contract, “if find returns a non-null result, then the
callback provided as an argument was invoked at least once”—and, in my
opinion, it’s totally reasonable that Flow doesn’t know this. (More
advanced type systems and theorem provers can express contracts like
these, but doing so isn’t currently a design goal of Flow, as far as I’m
aware. There are some internals like $Pred/$Refine that are moving
toward a richer understanding of the connections between input and
output values, but they don’t suffice for this particular case, anyway.)

As you may know, you can easily work around this by adding an explicit
assertion:

if (n == null) {
  throw new Error(String(n));
}
logNum(n);

If you’re worried about performance and have evidence to show that this
particular check is causing a significant slowdown (it’s probably not),
then you could abuse Flow’s comment syntax to convince the type
system that n will never be null without actually checking at runtime:

/*::
if (n == null) {
  throw new Error(String(n));
}
*/
logNum(n);

(More info: Abusing Flow comment syntax for great good.)

[amasad]

Thanks for the response.

So, to witness that your code is safe, Flow would need to
understand the contract, “if find returns a non-null result, then the
callback provided as an argument was invoked at least once”—and, in my
opinion, it’s totally reasonable that Flow doesn’t know this

Why shouldn't flow understand the find contract? It's in part of the standard library and if there's anything.

As you may know, you can easily work around this by adding an explicit
assertion:

We're already doing this all over the place in other refinement failures. Some of them are excusable, like calling a method, but overall I think Flow should be much better at this.

Code bloat both visually, and from a client-side bundle point-of-view really adds up with all those assertions.

[wchargin]

Why shouldn't flow understand the find contract? It's in part of the
standard library and if there's anything.

Sure, this is a fair point. Let me try to explain where I’m coming from.

I agree that Flow should be have definitions for all the contracts in
the standard library, so long as those contracts are expressible from
within Flow. But Flow doesn’t have the vocabulary to express the
concepts in this contract.

For instance, your callback has a postcondition: that after it is
invoked, the variable n will have type number (i.e., it will be
non-null). Flow doesn’t have a notion of postconditions at all, so we
don’t have a way to encode this.

But suppose that we do have a notion of postconditions. The
postcondition of find would be something like “if find returns
non-null, then the callback’s postconditions hold”. Now the
postcondition depends on the result of the function, so we need to
strengthen our theory of postconditions.

And, finally, the above postcondition of find isn’t quite strong
enough: the callback may have been invoked even if the result of find
is undefined, as in [undefined].find(() => true). The real
postcondition is more like “if the result of find is non-null _or_ the
this argument to find has length greater than 0, then the
callback’s postconditions hold”. Now we’ve taken a huge leap: Flow has
to know not just the _types_ of arguments but also their _values_, so
we’ve entered the realm of dependent types.

As a litmus test, how would we even write the types for these terms?
Maybe something like…

declare var n: ?number;
type Callback = (string, number) => boolean %post %type (n: number);

declare class $ReadOnlyArray<T> {
  find(p: (T) => boolean %post P): T | void %post (
    (%type (%result: $NonMaybeType<T> | null) => P)
    & (%exprtrue (this.length > 0) => P)
  );
}

Just seeing how much syntax needs to be added hints at the underlying
complexity.

Encoding contracts like that of find, then, requires a much stronger
type system than Flow has. This is why I believe that it’s reasonable
for Flow’s inference to be incomplete in this case: while I’d love to
see a more expressive type system, I also recognize that it would be an
enormous undertaking (dependent types totally change the game!), and
would be tricky to integrate into the rest of Flow.

We're already doing this all over the place in other refinement
failures. Some of them are excusable, like calling a method, but
overall I think Flow should be much better at this.

I feel your pain, and agree. :-) In particular, some notion of “pure”
functions would be really nice—that way, calling anArray.map needn’t
invalidate all the refinements in scope. Purity checking could be added
relatively easily (certainly much more easily than general contracts as
described above). Some other things, like that filter refines the type
of its result, can be implemented with some undocumented primitives in
Flow, but aren’t in the libdefs yet. Fingers crossed.

[mrkev]

Spot on @wchargin, thanks for your response. tldr is this refinement is more complex than it looks. Smarter scope analysis would be cool to add to flow, and likely a prerequisite to adding pure functions (#2715), but this would also involve some checks that I doubt will be added to flow, unfortunately.

[amasad]

Thanks for the explanation. While it does make sense, in my opinion, from a user perspective all this refinement pitfalls make for a lousy user experience that adds up to take away a big chunk of the utility that flow provided.