Flow: Libdefs (core): Array#filter(Boolean) and truthiness

[FireyFly]

The current Array#filter libdef defines the case of arr.filter(Boolean) to return Array<$NonMaybeType<T>>. Of course, filtering with Boolean (or an identity function, for that matter) as the predicate filters out only truthy values.

The current definition is sufficient for using .filter(Boolean) as an idiom for filtering out undefined/null, but it doesn't cover the reasonably common [..., (some condition) && value, ...].filter(Boolean) case, where the condition is a boolean expression.

I think it'd be really neat if this example typechecked (contrived example):

const fn = (a: string, b: string): string[] => [a, b.length > 0 && b].filter(Boolean);

My line of thinking is that this could be solved with primitives $Truthy<T> and $Falsy<T> to restrict a type T to truthy (resp. falsy) values in T, if possible to represent in the type system. The libdef for Array#filter(Boolean) would be changed to return Array<$Truthy<T>>. I'm not sure what changes would be necessary to && and || to support this, but my line of thinking is that (x: a) && (y: b) would be assigned type $Falsy<a> | b. The flow implementation would have to hardcode a table such that $Truthy<boolean> is true, $Falsy<boolean> is false, $Falsy<number> is 0 | NaN, etc.

Ideally, then, [a, b.length > 0 && b] would be typed as Array<string | $Falsy<boolean>> <=> Array<string | false>, and [a, b.length > 0 && b].filter(Boolean) as Array<$Truthy<string | false>> <=> Array<$Truthy<string> | $Truthy<false>> <=> Array<$Truthy<string>> <=> Array<string>.

I'm assuming it wouldn't be possible to represent "non-empty string" or "non-zero-nor-NaN number" "natively" in the type system.

[Diggsey]

I've been meaning to report this issue for a while...

[wchargin]

I appreciate the intention, but I would like to register a moderate
degree of skepticism.

The underlying issue is that filter really returns something like
“Array<U> where U is the greatest subtype of T such that the
predicate returns true for every value of U”. With the currently
documented operations in Flow, it is not possible to express this type.
We can add special cases like $NonMaybeType, $Truthy, and $Falsy,
but these only solve the simple cases. Common use cases like
options.filter((o) => o.type === "SOME") will still fail.

Flow has some partially completed work on $Pred and $Refine types,
which solve this problem in the general case. I posit that it would be a
much better use of developer time to polish these features such that
they’re ready for general consumption than to add more special cases.

There‛s a valid argument that “handling some of the common(?) special
cases is better than handling none of them at all”, which is why I’m not
dead-set against this suggestion. But I do think that handling just a
few special cases is hacky and ad hoc, and will make it harder for
beginners to understand what is actually going on.

[FireyFly]

Hmm, I wasn't aware of $Pred and $Refine, and I agree that handling it in a more general case makes more sense for sure.

I guess I should explain what led to the earlier suggestion (which isn't necessarily perfect, and it did occur to me that $Truthy and $Falsy would be special cases of something more general). As far as I can tell, any system for handling predicates is going to have to compromise somewhere (halting problem and all that, since a predicate could be arbitrarily complex and JS is Turing-complete). Since the refinement to only truthy or only falsy values is relevant to the && operator as well, I felt it was a "special" enough case that it'd be worth to back it by special types like that.

That said, definitely if there's already work on supporting refinement more generally, that would probably be a better use of development effort. I'll take a look at how $Pred and $Refine works, and check out #34 as well, thanks for the pointers! :)

[wchargin]

Appreciate your open-mindedness. :-)

As far as I can tell, any system for handling predicates is going to
have to compromise somewhere (halting problem and all that, since a
predicate could be arbitrarily complex and JS is Turing-complete).

Yes, but this is nothing new: it’s equivalent to type-checking in
general. Suppose that we want to define semantics for $Check<T, U>,
which is a subtype of (T) => boolean that returns true only when the
argument has type U. We may simply require: any return true; must be
preceded by an assertion that (x: U), where x is the argument to the
function, and all other return paths must return false.

This omits some high-level sugar that would be desirable—e.g., you want
to be able to do things like return x.type === "SOME". However, I
think that it demonstrates that the core functionality is feasible to
implement, and the sugar can probably be added on top of that. For
instance, the aforementioned statement can be desugared to

if (x.type === "SOME") return true; else return false;

at which point the core semantics suffice.

We therefore reduce the predicate satisfaction problem to the more
familiar problem of using type refinements to prove to Flow that an
expression has a certain type. As a consequence, Flow programmers will
be accustomed to the semantics, and won’t have to learn a new set of
arcana.

Since the refinement to only truthy or only falsy values is relevant
to the && operator as well

Interesting point: you’re suggesting, I suppose, that x && y could
have type something like $Falsy<typeof x> | typeof y instead of simply
typeof x | typeof y. That definitely makes sense, and I can imagine
how it might be useful. For instance, some APIs take Array<T | false>
with the semantics that false entries are ignored, so that you can
write [a, b, condition && c] to conditionally include items. This
proposed extension would, I believe, enable stronger invariants on such
inputs.

I also agree that if $Truthy and $Falsy are added for their own
virtue, _and_ we’re already specializing for $NonMaybeType, then we
might as well specialize for $Truthy and $Falsy, too.

thanks for the pointers! :)

You’re welcome.

[FireyFly]

[...]
We therefore reduce the predicate satisfaction problem to the more
familiar problem of using type refinements to prove to Flow that an
expression has a certain type. As a consequence, Flow programmers will
be accustomed to the semantics, and won’t have to learn a new set of
arcana.

Nod, makes plenty of sense.

Interesting point: you’re suggesting, I suppose, that x && y could
have type something like $Falsy<typeof x> | typeof y instead of simply
typeof x | typeof y.

Yep, exactly. I might not have put it very clearly. Of course the same applies to x || y as well, in that it'd have type $Truthy<typeof x> | typeof y--might be useful for the "default value" idiom as well.