# Can type inference be classified in two groups: unification-based and control-flow-based?

I recently came across the 1995 paper Safety analysis versus type inference (pdf link) by Palsberg and Schartzbach that contrasts unification-based type inference and static analysis methods based on control-flow analysis. According to the paper:

• In unification based type inference each identifier is related to a type variable ranging over type schemes, such as $int$ and $\forall a b . a \rightarrow b$. In control-flow static analysis the identifiers get related to variables ranging over what primitive types and other values in the source program can flow into the identifier.

• Unification-based type inference is "local" and can be performed one module at a time. Control-flow analysis tends to be global and require the whole program to be analyzed at once.

• Damas-Milner unification is a linear time algorithm (for typical programs) while control-flow analysis tends to have worse case running times that are cubic or worse (and at least quadratic in practice).

• Control-flow analysis can reason about program safety more precisely than unification-based inference (for example, it can detect some instances of dead code)

My question is: is this classification complete or are there other kinds of type inference that they did not mention?

• It's not clear to me that the two inference techniques are fundamentally different: it seems that in "unification based" inference the type-constraint resolution is deferred, whereas it is performed eagerly in the "control-flow based" approach. – cody Feb 12 '15 at 22:04
• @cody: What do you mean by "eager" there? In my head deferring type checking means doing runtime tests but thats clearly not what you were talking about. – hugomg Feb 13 '15 at 3:42
• I would say that there are also constraint-based approaches (the work of Scott Smith, for instance), though again the boundary with the other types is not clear cut. – Dave Clarke Feb 15 '15 at 12:17
• @DaveClarke I think the constraint approach may fall under the "flow based" category: From the webpage of Scott's research group: "Type constraint systems are a very expressive form of type which can be given to programs. They are so expressive that they can in fact fully record flow information about a program, namely this data value could flow to that operation." – hugomg Feb 15 '15 at 13:25
• It' your classification. If that's the way you want to see it. – Dave Clarke Feb 15 '15 at 14:24