When does a type generalise another type?

Question

In languages like Haskell, with a Hindley-Milner type system, when does a type $t$ generalise a type $u$? I use the definition: $t$ generalises $u$ iff $\forall\ v: v \text{ unifies with } u \rightarrow v \text{ unifies with } t$.

I have an algorithm that given these types returns a unifier if one exist. The unifier is an ordered list of assignments $v_1 \mapsto t_1, v_2 \mapsto t_2, \dots, v_n \mapsto t_n$ such that applying $v_i := t_i$ to both types for ascending $i$ results in two identical types.

For instance, the types $(a,a)$ and $(p,q)$ unify with the unifier $a \mapsto p, p \mapsto q$: after applying these assignments both types are $(q,q)$.

It should be possible to use the unifier to see if a type generalises another type, but I can't figure it out at the moment. I couldn't find an existing algorithm either.

Note: if there is an easier way, without using the unifier, that would be appreciated as well.

Answer 1

A pretty easy way to see if $t$ generalizes $u$ if $u$ matches $t$:

replace all variables in $u$ by (fresh) constants, written $u_c$, and check if $u_c$ unifies with $t$.

If so, then there is a substitution $\sigma$ such that $t\sigma\equiv u$ which means by definition that $t$ is more general than $u$.

As mentioned in the comments, if $\mathrm{mgu}(t,u)$ succeeds and returns a substitution $\tau$, then $u$ matches $t$ iff $u\tau\equiv u$ up to variable renaming.

Note: Pattern matching is usually best implemented independently from unification, as it is simpler in general. In particular it isn't necessary to actually replace variables with constants in $u$. Beware of non-linearities in $t$ though: $\alpha\rightarrow \alpha$ does not match $\mathrm{int}\rightarrow\mathrm{bool}$!

Answer 2

The accepted answer is very good, but the below is easier to implement and, I believe, correct as well:

• Make groups of the assigned variables such that variables that will be rewritten to the same type are in the same group.

• For all groups, verify:

  • There is at most one variable from the right-hand type in the group.
  • If there is a variable from the left-hand type in the group, there may not be any non-variables in the group.