Earlier quoted context omitted.
As I explained in https://news.ycombinator.com/item?id=31222098 , I don't think this explanation is correct. You're right that bool → bool is not a subtype of α → α, and that function types are contravariant on their argument type. But because function types are not also covariant on their return type, the same logic would tell us that α → α is neither a subtype of bool → bool nor a supertype. In fact, though, α → α…
All these explanations seem somewhat confused to me because they don’t pin down what the variables represent. In a traditional formulation of Hindley-Milner, there are two distinct notions of a “variable”: (1) a bound variable under a quantifier, or (2) a metavariable, also known as a unification variable, introduced by the type inference algorithm. Bound variables are variables that either the programmer wrote expli…
To clarify, when I wrote α, I always and only meant a bound variable under a quantifier, because I didn't know about this metavariable thing at all. I was writing α → α because that's how tuareg-font-lock-symbols renders 'a -> 'a, which does include the implicit quantifier.
It's no wonder I was never able to understand HM since I didn't know about this dual nature of variables. This will probably help me a lot next time I try to understand it! I do think I understand unification, though I've only implemented it once.
I really appreciate you being willing to engage on HN, despite the unpleasant aggressiveness and character assassination that runs rampant here.