3
$\begingroup$

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:

Constraints generation

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:

Unification algorithm

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?

$\endgroup$
  • $\begingroup$ is this related to occurs check in gprolog (preventing infinite loops)? $\endgroup$ – seteropere Apr 25 '14 at 8:05
  • $\begingroup$ @seteropere: I think so. As far as I know, the name comes from Prolog. $\endgroup$ – beta Apr 25 '14 at 13:37
  • $\begingroup$ It's essentially the same unification algorithm as the one in prolog. $\endgroup$ – Andrej Bauer Apr 26 '14 at 22:30
5
$\begingroup$

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 = <fun>

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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