<p>Perhaps an even better way to see type inference is as a specialization of a single framework: <a href="http://en.wikipedia.org/wiki/Abstract_interpretation" rel="noreferrer">Abstract Interpretation</a> (abbreviated AI).  The hallmark of most unification-based type inference algorithms is that they generate the <a href="http://en.wikipedia.org/wiki/Principal_type" rel="noreferrer">principal type</a> for a term; translated into AI terms, this means that you never need to <strong>widen</strong>, nor do you need to go to <em>power domains</em> 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.</p>

<p>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.</p>

<p>Perhaps an even better way to see type inference is as an alternate <em>interpreter</em> for a program: rather than producing values, it produces types.  It is very easy to see type inference as a form a <em>partial evaluation</em>.  Perhaps an easy introduction to that circle of ideas is via Aaron Stump's <a href="http://homepage.cs.uiowa.edu/~astump/papers/lmcs12-rewriting-view.pdf" rel="noreferrer">A rewriting view of simple typing</a>.</p>

CC BY-SA 3.0
2015-02-18T02:46:08.253Z
Do you have a reference for the categorical interpretation of unification?
cody
CC BY-SA 3.0
2015-02-18T13:28:54.707Z
@cody: I first learned of it in Rydeheard and Burstall's *computational category theory* book, now available online at http://www.cs.man.ac.uk/~david/categories/.
Jacques Carette
CC BY-SA 3.0
2015-02-17T01:14:11.393Z
2015-02-17T01:14:11.393Z
Jacques Carette
<p>I recently came across the 1995 paper <a href="http://www.cs.ucla.edu/~palsberg/paper/ic95-ps.pdf" rel="noreferrer">Safety analysis versus type inference</a> (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:</p>

<ul>
<li><p>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.</p></li>
<li><p>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.</p></li>
<li><p>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).</p></li>
<li><p>Control-flow analysis can reason about program safety more precisely than unification-based inference (for example, it can detect some instances of dead code)</p></li>
</ul>

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

CC BY-SA 3.0
2015-02-12T22:04:30.513Z
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
CC BY-SA 3.0
2015-02-13T03:42:39.997Z
@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
CC BY-SA 3.0
2015-02-15T12:17:10.430Z
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
CC BY-SA 3.0
2015-02-15T13:25:35.913Z
@DaveClarke I think the constraint approach may fall under the "flow based" category: From the [webpage of Scott's research group](http://pl.cs.jhu.edu/constraints.shtml): "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
CC BY-SA 3.0
2015-02-15T14:24:58.637Z
It' your classification. If that's the way you want to see it.
Dave Clarke
CC BY-SA 3.0
2015-02-18T02:47:42.247Z
"Eager" in this context means that each constraint is solved (as much as possible) as soon as it is created.
cody
<pl.programming-languages><type-theory><type-systems><type-inference>
Can type inference be classified in two groups: unification-based and control-flow-based?
hugomg
# Can type inference be classified in two groups: unification-based and control-flow-based?

(Asked by: username_0 on 2015-02-12)

I recently came across the 1995 paper [Safety analysis versus type inference](http://www.cs.ucla.edu/~palsberg/paper/ic95-ps.pdf) (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?

**Tags:** pl.programming-languages, type-theory, type-systems, type-inference

> **Comments:**
> **username_1**: 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.  
> **username_0**: @username_1: 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.  
> **username_2**: 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.  
> **username_0**: @DaveClarke I think the constraint approach may fall under the "flow based" category: From the [webpage of Scott's research group](http://pl.cs.jhu.edu/constraints.shtml): "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."  
> **username_2**: It' your classification. If that's the way you want to see it.  
> **username_1**: "Eager" in this context means that each constraint is solved (as much as possible) as soon as it is created.  

---

## 1 answers

### Answer by username_3 on 2015-02-17. Score: 5 | Accepted answer

Perhaps an even better way to see type inference is as a specialization of a single framework: [Abstract Interpretation](http://en.wikipedia.org/wiki/Abstract_interpretation) (abbreviated AI). The hallmark of most unification-based type inference algorithms is that they generate the [principal type](http://en.wikipedia.org/wiki/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](http://homepage.cs.uiowa.edu/~astump/papers/lmcs12-rewriting-view.pdf).

> **Comments:**
> **username_1**: Do you have a reference for the categorical interpretation of unification?  
> **username_3**: @username_1: I first learned of it in Rydeheard and Burstall's *computational category theory* book, now available online at http://www.cs.man.ac.uk/~david/categories/.  

---

