4
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Note that $(q,q)$ is the same as $(a,a)$ (up to renaming variables). Unless I am missing something, $t$ generalises $u$ iff $mgu(t,u)=u$ (again, up to renaming). $\endgroup$ – Alexey Romanov Oct 26 '17 at 13:16
  • 1
    $\begingroup$ @AlexeyRomanov I think that might be the right idea, but keep in mind that the $mgu$ can never be $u$, since it is a substitution, not a term. Perhaps we need something like $u[mgu(t,u)]=_\alpha u$. $\endgroup$ – chi Oct 26 '17 at 13:29
  • $\begingroup$ @chi Of course, right. That was in a bit of a hurry. $\endgroup$ – Alexey Romanov Oct 26 '17 at 13:54
5
$\begingroup$

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}$!

$\endgroup$
1
$\begingroup$

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.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.