Equivalence of data-flow analysis, abstract interpretation and type inference?

Question

@Babou's answer to a recent question reminds me that at one time I think I read a paper about the equivalence (in terms both of the facts that can be inferred or proved and the time complexity of running the inference algorithm) of data-flow analysis, abstract interpretation, and type inference.

In some sub-cases (like between forward context-sensitive interprocedural data-flow analysis and abstract interpretation) the equivalence is relatively obvious to me, but the question seems more subtle for other comparisons. For example, I can't figure out how Hindley-Milner type inference could be used to prove some of the properties that can be proved with flow-sensitive data-flow analysis.

What are the seminal references discussing the equivalences (or differences) between data-flow analysis, abstract interpretation and type inference?

Answer 1

Data flow analysis and type inference are specific instances of abstract interpretation.

Data flow analysis and abstract interpretation look similar since they are both about computing a fix point. Data flow analyses typically have finite-height abstract domains which ensures termination. In general, abstract interpretation does not assume such abstract domains; to deal with infinite height domains abstract interpretation uses techniques of widening and narrowing.

It turns out that type inference is also about fix-point computation, although that is far from obvious, imo. Here is a paper that explicitly shows that types are abstract interpretations: paper. Basically, types are seen as an abstraction of program concrete semantics. In Hindley-Milner type system, for instance, abstract domain of types is of infinite height and computing a (most general) type using unification is essentially performing a (very imprecise) widening operation.

Answer 2

I consider them as basically the same. They just had initially different goals and were coined by different computer science factions.

Data flow analysis comes from the compiler engineering faction, trying to talk about their optimization algorithms and proofing upper bounds on their complexity etc.

Abstract interpretation comes from the formal, mathematical field of computer science. This is an even more formal version with more interest in correctness and less in building real compilers.

Type inference comes from the academic field of functional programming where it was initially a tool to do cool stuff with compilers. Then the idea came up, that a type can be a lot more than just "int" or "float" but also other stuff like in classic data flow analysis.

Answer 3

A good place to learn about these three approaches and how the relate is the book Principles of Program Analysis by Nielson, Nielson and Hankin.

I don't think it's correct to say that data-flow analysis, abstract interpretation and type inference are the same thing. While there are many similarities, and maybe more than would expect, given that the three originated in different communities, there are also many differences.