4
$\begingroup$

I'm looking at implementing type inference for a Hindley-Milner type system, and before I have even started to implement the Damas-Milner algorithm, while working through some examples, I hit some stumbling blocks.

I'm trying to follow some notes on the algorithm. Given the following program:

let id x = x
  in id id

I first use the pseudo code for the letfn case:

  1. Create a new type variable for the function type: funType := α
  2. Create a new type variable for the argument type: argType := β
  3. Infer the return type:
    1. Extend the (empty) type environment for the function body to be functionBodyTypeEnv := ['x' → β, 'id' → α]
    2. Look up the return type and find it to be β: returnType := β
  4. Note down the constraint that the function type and (argument → result) type must be the same: α = β → β

Okay. So far so good. We now have a type for the function (α) and also have found one constraint: α = β → β. Now let's infer the type of the let's body (which will be the type of the full program):

  1. Extend the (empty again) type environment with the generalized type of the function so we get letBodyTypeEnv := ['id' → ∀α.α] ⚠️
  2. Infer the type of the let body, which is a call with of 'id' (function) with 'id' (argument):
    1. Find the type of the variable 'id' (function) to be ∀α.α and instantiate/specialize this to be γ: funType := γ (there are no free type variables, so it's a monotype) ⚠️
    2. Same as above: Find the type of the variable 'id' (argument) to be ∀α.α and instantiate this to be δ: argType := δ ⚠️
    3. Create a new type variable for the return type: returnType:= ε
    4. Note down the constraint that the function type and the (argument → result) type must be equal: γ = δ → ε
    5. Return the result type as the type of the let body: return ε

So at this point we have the type ε for the full program and have recorded the constraints [α = β → β, γ = δ → ε]. However, this is (obviously) wrong and I suspect that the problem is with step 4, 5.1 and 5.2.

In step 4 we have the type of the function 'id' as α and generalize it to be ∀α.α before inferring the type of the let body. However, if instead of just “noting down” that α = β → β we replaced α by β → β in the type environment of the let body, we would have inferred the type β → β in step 5.1 and 5.2 – and that would have been the (correct) type of the program.

Are my observations correct? If so, should I always replace a type variable with the type it's equal to when finding such a constraint?

$\endgroup$

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.