Avoiding type inference false-positives with flow-sensitive conditional analysis

https://psalm.dev/articles/the-truth-matters

by muglug • 5 years ago

36 18 5 years ago

psalm.dev

ncmncm• 5 years ago

Psalm appears to be a static analyzer tool for PHP code.

UncleMeat4• 5 years ago

Lastly there's a cost to maintaining a system that doesn’t appear to exist outside of Psalm.

This seems like an odd claim to make (OP also repeats it elsewhere in the text and seems to be aware of a single exception). The analysis described in the blog post is not novel or unique. It is useful but I don't really know what to make of this claim. Abstract interpretation, symbolic execution, and even typechecking systems have all used this kind of approach for many decades. There are hundreds of papers and tools using this approach.

Usually, you'd call this "path sensitive analysis".

I love seeing static analysis show up outside of academic papers, but there is a wealth of material for people to immerse themselves in if they want to learn!

mshockwave• 5 years ago

second this, I believe there are tons of similar research of similar techniques

wwwigham• 5 years ago

Funny that the author mentions TypeScript, then complains that maintaining a system like this that "doesn't exist elsewhere" would be hard. TypeScript, in fact, does an analysis almost exactly like what is described in the article. Possibly even more expansive, since it also allows for user-defined assertions and guards, in addition to simple syntactic narrowing.

muglug6• 5 years ago

TypeScript doesn't perform this conditional analysis:

This is a false-positive:

https://www.typescriptlang.org/play?#code/GYVwdgxgLglg9mABMO...

since it also allows for user-defined assertions and guards

Psalm allows user-defined type guards:

https://psalm.dev/docs/annotating_code/adding_assertions/

muglug6• 5 years ago

Author here: I'm not aware this analysis in typechecking systems outside of Typed Racket and Psalm – if you point me to them I'll happily update the article!

I've also discussed the article with the authors of the linked paper, who didn't suggest anything else in the way of prior art.

UncleMeat4• 5 years ago

I don't really know how to answer this.

The technique is broader than type inference / type checking. Like, if you just type "symbolic execution" into google scholar you'll find piles of systems that do this sort of collection of branch predicates and narrowing. Notably, you seem to be doing this on values in addition to types (since you care about which value a string matches), which makes this more closely related to something like symbolic execution than classic type inference.

If you want something in the typing space, there are oodles of tools that use the theory of dependent types to achieve things like this.

If you want something in the abstract interpretation space, numerical analysis does this sort of path-sensitive narrowing for bounds all the time. A scholar search for "abstract interpretation numerical domain" will turn up mountains of papers.

peterkelly• 5 years ago

I get your point, but I think you're being a bit harsh on OP. Yes the material is covered in the literature, but for people who aren't already familiar with it, it can take an enormous amount of time and effort to both find and understand the right papers (I know because I've been doing exactly that for the past few months for a language I'm designing).

This blog post gives a nice and easily-understood explanation of the concept, which is more than can be said for the way that much of the literature on type theory and static analysis is written. HN isn't an academic journal or PhD defense; ideas described don't have to be new to be useful.

And making ideas more widely known is valuable; even the just-released Java 16 missed out on this exact feature in its "pattern matching" (really type narrowing) support, requiring the programmer to declare an additional variable rather than using information just established about an existing one: https://openjdk.java.net/jeps/394

UncleMeat4• 5 years ago

I think it is a useful tool. I also think that getting meaningful results on a 6% performance hit is impressive. IMO, the blog post would be a great little piece with two or three sentences removed.

My hope is that OP finds kinship in the community, not to discourage them.

ordu• 5 years ago

Doesn't Rust do the same, when I write `let a = match ... ;` and then rustc complains that return types of branches do not match?

savant_penguin• 5 years ago

Is there a reason not to disallow type inferences altogether?

ashton314• 5 years ago

I think this might fall over pretty quickly in the presence of first-class functions. In that case, you can’t determine the control graph statically. You’ll need Control-Flow Analysis for that.

Also, not surprised Racket already has occurrence typing. It’s got basically everything else.

Avoiding type inference false-positives with flow-sensitive conditional analysis

Related Stories