I am trying to understand the constraints-based Hindley–Milner type inference algorithm described in the Generalizing Hindley-Milner paper. The function $\text{S}\small{\text{OLVE}}$ is defined as follows:

$$ \begin{array}{l} \text{S}\small{\text{OLVE}} :: Constraints → Substitution \\ \text{S}\small{\text{OLVE}} (\emptyset) = [\ ] \\ \text{S}\small{\text{OLVE}} (\{ \tau_1 \equiv \tau_2 \} \cup C) = \text{S}\small{\text{OLVE}} (\mathcal{S} C) \circ \mathcal{S} \\ \quad \quad \quad \text{where}\ \mathcal{S} = \text{mgu}(\tau_1, \tau_2) \\ \text{S}\small{\text{OLVE}} (\{ \tau_1 \leq_M \tau_2 \} \cup C) = \text{S}\small{\text{OLVE}} (\{ \tau_1 \preceq \text{generalize}(M, \tau_2) \} \cup C) \\ \quad \quad \quad \text{if}\ (\text{freevars}(\tau_2) − M) \cap \text{activevars}(C) = \emptyset \\ \text{S}\small{\text{OLVE}} (\{ \tau \preceq \sigma \} \cup C) = \text{S}\small{\text{OLVE}} (\{\tau \equiv \text{instantiate}(\sigma)\} \cup C) \\ \end{array} $$

Most of this is clear, but where I am confused is around how substitution is defined for the monomorphic set $M$. The paper explains that

For implicit instance constraints, we make note of the fact that the substitution also has to be applied to the sets of monomorphic type variables.

$$ S(\tau_1 \leq_M \tau_2) =_{def} \mathcal{S} \tau_1 \leq_{\mathcal{S} M} \mathcal{S} \tau_2 $$

but I don't find any details of how $\mathcal{S} M$ is defined. Based on Example 3, I think we should get something like:

$$ \text{S}\small{\text{OLVE}} (\{\tau_4 \leq_{\{ \tau_1 \}} \tau_3, \text{Bool} \rightarrow \tau_3 \equiv \tau_1 \}) \\ = \text{S}\small{\text{OLVE}} (\{\tau_4 \leq_{\{ \tau_3 \}} \tau_3 \}) \circ[\tau_1 := \text{Bool} \rightarrow \tau_3] $$

In this step, unifying $ \text{Bool} \rightarrow \tau_3 $ and $ \tau_1 $ gives a substitution $ \mathcal{S} = [ \tau_1 := \text{Bool} \rightarrow \tau_3 ] $, and $ M = \{ \tau_1 \} $, and so apparently $ \mathcal{S} \{ \tau_1 \} = \{ \tau_3 \} $, but how do we arrive at that? Maybe there is something obvious I have overlooked here.

  • 1
    $\begingroup$ Could it be that $\mathcal{S}M$ in $\mathcal{S}\tau_1\leq_{\mathcal{S}M}\mathcal{S}\tau_2$ is not a different relation, but means the set of type variables that the substitution $\mathcal{S}$ brings in scope? $\endgroup$
    – frabala
    Jun 9 '20 at 22:37

Your Answer

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

Browse other questions tagged or ask your own question.