Hindley-Milner and the lambda calculus

(written by lawrence krubner, however indented passages are often quotes). You can contact lawrence at: lawrence@krubner.com

A nice attempt to explain the crazy syntax of the math that formalizes the idea that the type of an expression can be deduced from the expression itself:

Okay, so we want to talk about expressions. Arbitrary expressions. In an arbitrary language. And we want to talk about inferring types of these expressions. And we want to figure out rules for how we can infer types. And then we’re going to want to make an algorithm that uses these rules to infer types. So we’re going to need a meta-language. A language to talk about expressions in an arbitrary programming language. This meta-language should:

Be abstract and generic, so that it allows us to reason about statements of type inference purely based on their form (hence, formalization), without having to worry about their content.
Give a precise, unambiguous, yet intuitive definition for what an expression is.
Give those definitions in terms of a small number of uncontroversial primitive concepts.
Similarly give definitions for types, the idea that an expression has a type, and the idea that we can infer that a given expression has a given type.
Lend itself to a simple, terse symbolic representation, e.g. rather than saying “the expression formed by applying the first expression to the second expression has the type of a function from strings to some type we don’t care to specify in the current context” we could simply say “e1(e2):String→te1(e2):String→t”.
Be easily translated to something a computer can understand and implement, so we can ultimately automate type inference.