<p>Yes, the occurs check is there so that the algorithm is guaranteed to terminate. Without it, when we deal with an equation $X = T$ in which $X$ may occur, substituting $T$ for $X$ everywhere does not get rid of $X$, and so we can run in circles, as your example shows.</p>

<p>There is a way to avoid this by allowing arbitrary recursive types. If we have an equation $X = T$ then we may replace $X$ everywhere by the type $\mathsf{fix} \,X \,.\, T$, i.e., a canonical solution to the equation $X = T$. Ocaml will do this for you if you run it with <code>-rectypes</code>:</p>

<pre><code>$ ocaml -rectypes
        OCaml version 4.01.0

# fun x -&gt; x x ;;
- : ('a -&gt; 'b as 'a) -&gt; 'b = &lt;fun&gt;
</code></pre>

<p>This says that <code>fun x -&gt; x x</code> has the type $A \to B$ where $A = A \to B$.</p>

<p>By the way, you can find an implementation of the algorithm in my PL Zoo, see <a href="https://github.com/andrejbauer/plzoo/blob/master/src/poly/type_infer.ml#L53" rel="noreferrer"><code>solve</code></a> in the language Poly.</p>

CC BY-SA 3.0
2014-04-25T22:51:45.923Z
2014-04-25T22:51:45.923Z
Andrej Bauer
<p>I'm reading about type inference in chapter 30 of <a href="http://cs.brown.edu/~sk/Publications/Books/ProgLangs/2007-04-26/plai-2007-04-26.pdf" rel="nofollow noreferrer">Programming Languages: Application and Interpretation</a> and I'm trying to understand exactly how the occurs check works in an example I came up with.</p>

<p>Constraints generation is presented in this table:</p>

<p><img src="https://i.sstatic.net/S0h1d.png" alt="Constraints generation"></p>

<p>So, given the term <code>λx.x x</code>, we get the following two constraints, as far as I can see:</p>

<ul>
<li>[λx.x x] = [x] → [x x] (from <code>λ.x x</code>)</li>
<li>[x] = [x] → [x x] (from <code>x x</code>)</li>
</ul>

<p>Ok, onto the unification algorithm, described in the following manner:</p>

<p><img src="https://i.sstatic.net/3LwhM.png" alt="Unification algorithm"></p>

<p>Apart from the use of the word “identifier”, this looks easy enough. (Apparantly the author uses “identifier” since he first assigns a name such as 1⃣  to a term like [λx.x x] – I guess these boxed numbers are identifiers...)</p>

<p>Ok, so our stack of constraints is</p>

<pre><code>{[λx.x x] = [x] → [x x], [x] = [x] → [x x]}
</code></pre>

<p>and our set of substitutions is empty. The first constraint can simply be added to the set of substitutions, which is now</p>

<pre><code>{[λx.x x] ↦ [x] → [x x]}
</code></pre>

<p>We then replace each occurrence of <code>[λx.x x]</code> with <code>[x] → [x x]</code>, but there are none, so our job in this step is done.</p>

<p>In the next step, the remaining constraint gets the same treatment: we simply add it to the set of substitutions, which then becomes</p>

<pre><code>{[λx.x x] ↦ [x] → [x x], [x] ↦ [x] → [x x]}
</code></pre>

<p>But our job in this step is not done, we also need to recursively update all occurrences of [x] with [x] → [x x], so we get</p>

<pre><code>{[λx.x x] ↦ [x] → [x x], [x] → [x x] ↦ [x] → [x x]}
</code></pre>

<p>Doing this again gives us</p>

<pre><code>{[λx.x x] ↦ [x] → [x x], [x] → [x x] → [x x] ↦ [x] → [x x]}
</code></pre>

<p>… and so on, never terminating.</p>

<p>Is this understanding of the problem the “occurs check” solves correct? Is this what would have happened in a type inference algorithm such as Hindley-Milner if there wasn't an explicit occurs check?</p>

CC BY-SA 3.0
2014-04-25T08:05:10.473Z
is this related to occurs check in gprolog (preventing infinite loops)?
seteropere
CC BY-SA 3.0
2014-04-25T13:37:31.353Z
@seteropere: I think so. As far as I know, the name comes from Prolog.
beta
CC BY-SA 3.0
2014-04-26T22:30:06.083Z
It's essentially the same unification algorithm as the one in prolog.
Andrej Bauer
<type-theory><type-systems><type-inference>
Occurs check in type inference
beta
# Occurs check in type inference

(Asked by: username_0 on 2014-04-24)

I'm reading about type inference in chapter 30 of Programming Languages: Application and Interpretation and I'm trying to understand exactly how the occurs check works in an example I came up with.
Constraints generation is presented in this table:

So, given the term λx.x x, we get the following two constraints, as far as I can see:

[λx.x x] = [x] → [x x] (from λ.x x)
[x] = [x] → [x x] (from x x)

Ok, onto the unification algorithm, described in the following manner:

Apart from the use of the word “identifier”, this looks easy enough. (Apparantly the author uses “identifier” since he first assigns a name such as 1⃣  to a term like [λx.x x] – I guess these boxed numbers are identifiers...)
Ok, so our stack of constraints is
{[λx.x x] = [x] → [x x], [x] = [x] → [x x]}

and our set of substitutions is empty. The first constraint can simply be added to the set of substitutions, which is now
{[λx.x x] ↦ [x] → [x x]}

We then replace each occurrence of [λx.x x] with [x] → [x x], but there are none, so our job in this step is done.
In the next step, the remaining constraint gets the same treatment: we simply add it to the set of substitutions, which then becomes
{[λx.x x] ↦ [x] → [x x], [x] ↦ [x] → [x x]}

But our job in this step is not done, we also need to recursively update all occurrences of [x] with [x] → [x x], so we get
{[λx.x x] ↦ [x] → [x x], [x] → [x x] ↦ [x] → [x x]}

Doing this again gives us
{[λx.x x] ↦ [x] → [x x], [x] → [x x] → [x x] ↦ [x] → [x x]}

… and so on, never terminating.
Is this understanding of the problem the “occurs check” solves correct? Is this what would have happened in a type inference algorithm such as Hindley-Milner if there wasn't an explicit occurs check?

**Tags:** type-theory, type-systems, type-inference

> **Comments:**
> **username_1**: is this related to occurs check in gprolog (preventing infinite loops)?  
> **username_0**: @username_1: I think so. As far as I know, the name comes from Prolog.  
> **username_2**: It's essentially the same unification algorithm as the one in prolog.  

---

## 1 answers

### Answer by username_2 on 2014-04-25. Score: 5 | Accepted answer

Yes, the occurs check is there so that the algorithm is guaranteed to terminate. Without it, when we deal with an equation $X = T$ in which $X$ may occur, substituting $T$ for $X$ everywhere does not get rid of $X$, and so we can run in circles, as your example shows.
There is a way to avoid this by allowing arbitrary recursive types. If we have an equation $X = T$ then we may replace $X$ everywhere by the type $\mathsf{fix} \,X \,.\, T$, i.e., a canonical solution to the equation $X = T$. Ocaml will do this for you if you run it with -rectypes:
$ ocaml -rectypes
        OCaml version 4.01.0

# fun x -> x x ;;
- : ('a -> 'b as 'a) -> 'b = 

This says that fun x -> x x has the type $A \to B$ where $A = A \to B$.
By the way, you can find an implementation of the algorithm in my PL Zoo, see solve in the language Poly.


---

