patternMinor
Equivalence of data-flow analysis, abstract interpretation and type inference?
Viewed 0 times
abstractflowanalysisinferencetypeanddatainterpretationequivalence
Problem
@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?
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?
Solution
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.
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.
Context
StackExchange Computer Science Q#30746, answer score: 7
Revisions (0)
No revisions yet.