|
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 explicitly in their program or variables introduced by generalization. They appear underneath a quantifier, as in the type ∀ a. a -> a
which makes the quantification explicit. However, both SML and Haskell make the placement of quantifiers implicit by default, which is somewhat syntactically convenient, but it obscures this distinction.In HM, a bound variable only unifies with itself, so if we use `~` to mean “unifies with”, then `a ~ a` holds but neither `a ~ Bool` nor `a ~ b` do, assuming `a` and `b` are bound variables. However, bound variables do not actually get involved in typechecking unless the programmer wrote them in their program explicitly, because when a polymorphic binding is used, the typechecker instantiates it, replacing bound variables with metavariables. There is no way for the programmer to write metavariables in their types, because metavariables are, as their name suggests, a metalanguage concept introduced by the typechecking machinery, not a part of the underlying language of types. This makes writing them down in a way that clearly distinguishes them from bound type variables somewhat difficult, so I will adopt the convention of using Greek letters to represent metavariables. This means we can instantiate the above type to get α -> α
which is a very different type! In particular, while bound variables only unify with themselves, metavariables unify with anything so `α ~ α`, `α ~ Bool`, `α ~ a`, and `α ~ β` all hold. However, a metavariable can only unify with something other than itself once, because the process of unification effectively mutates the typechecking context by globally replacing the metavariable with the type it unified with. That is, if typechecking requires the unification `α ~ Bool`, then our function type `α -> α` becomes `Bool -> Bool`, since we perform the unification by globally replacing α with Bool.All of this stuff might seem a bit fiddly, since we’re explaining metavariables in terms of internal details of a typechecking algorithm. But indeed, that’s the point: metavariables are an invention of the typechecking algorithm, a mechanism used to implement type inference. They aren’t really types, they’re “holes” in types that have yet to be filled in by the type inference process. So when you ask a question like “is `Bool -> Bool` a subtype of `α -> α`”, your question is somewhat meaningless, as it depends on what α means for whatever typechecking algorithm you’re discussing, and pure HM does not really have any notion of subtyping (just instantiation and unification). If we introduce more sophisticated type systems that do have subtyping, then we have the machinery to talk about things like covariance and contravariance. But in HM, no such relation exists, so any notions of subtyping, covariance, and contravariance exist only in our heads, not in the type system itself. Still, we can informally establish a notion of subtyping by saying that if S is a subtype of T, written `S <: T`, then an expression of type S can be used wherever an expression of type T is expected. Given that, we can ask whether (∀ a. a -> a) <: (Bool -> Bool)
holds. The answer is certainly yes, as we can always instantiate the former to get the latter (which is what you refer to as specialization). But that quantifier is crucial, because it’s what allows us to do the instantiation! If we just have (a -> a) <: (Bool -> Bool)
then the relation no longer holds, as `a` is a bound variable that is only a subtype of itself, and we no longer have the freedom to instantiate it. So when reasoning about types involving variables, it’s wise to keep the quantifiers explicit, otherwise you may come to the wrong conclusions. |
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.