How to comprehend Algorithm W in Hindley–Milner type system?

Question

I am studying the algorithm W. From my understand, algorithm W takes (Γ,expr) as input ,where Γ is the context, and expr is the expression. The output is a substitution σ. Then I can use the substitution σ to take another (Γ,expr) as σ(Γ,expr).

What confuses me is what to do next. Since expr can have cases as: variable, abstraction, application, condition, fix-point expression, and let expression.

What is the purpose of having different cases of expr? What should I do in the next step?

Answer 1

Algorithm W does not only return a substitution but also a type τ which is the type inferred from the expression that you fed in the algorithm from the beginning.

A substitution S is a map from a type variable α to a type τ and therefore a substitution does not rely on the type environment Γ as you have implied.

Each case is handled separately (e.g. application uses unification but the other that you have mentioned does not) and interconnected in a recursive manner. Here is the pseudocode for algorithm W for some expressions