7
$\begingroup$

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?

Improve this question
$\endgroup$
6
  • $\begingroup$ 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. $\endgroup$
    – cody
    Feb 12, 2015 at 22:04
  • $\begingroup$ @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. $\endgroup$
    – hugomg
    Feb 13, 2015 at 3:42
  • $\begingroup$ 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. $\endgroup$
    – Dave Clarke
    Feb 15, 2015 at 12:17
  • $\begingroup$ @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." $\endgroup$
    – hugomg
    Feb 15, 2015 at 13:25
  • $\begingroup$ It' your classification. If that's the way you want to see it. $\endgroup$
    – Dave Clarke
    Feb 15, 2015 at 14:24

1 Answer 1

Reset to default
5
$\begingroup$

Perhaps an even better way to see type inference is as a specialization of a single framework: Abstract Interpretation (abbreviated AI). The hallmark of most unification-based type inference algorithms is that they generate the principal type for a term; translated into AI terms, this means that you never need to widen, nor do you need to go to power domains to find the answer. Unification turns out to be the 'join' operation -- there is also a nice categorical interpretation of unification which is even more enlightening.

Several comments shed light on this as well: all algorithms can be better understood in terms of generating then solving systems of constraints. Unification is indeed eager, and constraint-solving (and that includes control-flow based approaches) tend to be lazier.

Perhaps an even better way to see type inference is as an alternate interpreter for a program: rather than producing values, it produces types. It is very easy to see type inference as a form a partial evaluation. Perhaps an easy introduction to that circle of ideas is via Aaron Stump's A rewriting view of simple typing.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Do you have a reference for the categorical interpretation of unification? $\endgroup$
    – cody
    Feb 18, 2015 at 2:46
  • $\begingroup$ @cody: I first learned of it in Rydeheard and Burstall's computational category theory book, now available online at cs.man.ac.uk/~david/categories. $\endgroup$
    – Jacques Carette
    Feb 18, 2015 at 13:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.