It is worth noting that lots of applications of unification do not reify explicit substitutions in their implementations. You often see introductory type inference articles (usually focused on Hindley-Milner) use algorithm W, which uses a unification procedure that returns substitutions (which must then be composed with other substitutions). All of this is less efficient and arguably more error-prone and more complicated than the destructive unification implied by algorithm J (using the union-find data structure, often implemented invasively into the type representation to imply a union-find forest).<p>To this end, good coverage of decent (destructive) unification algorithms can be found in any simple resource on type inference (<a href="https://okmij.org/ftp/ML/generalization/sound_eager.ml" rel="nofollow">https://okmij.org/ftp/ML/generalization/sound_eager.ml</a>) or the Warren Abstract Machine (<a href="https://github.com/a-yiorgos/wambook/blob/master/wambook.pdf">https://github.com/a-yiorgos/wambook/blob/master/wambook.pdf</a>).<p>Of course, there are times where you would want to reify substitutions as a data structure to compose and apply, but most of the time you just want to immediately apply them in a pervasive way.<p>Despite what another comment says, unification is a valid - and rather convenient - way to implement pattern matching (as in the style of ML) in an interpreter: much like how you rewrite type variables with types you are unifying them with, you can rewrite the pattern variables to refer to the parts of the (evaluated) value you are matching against (which you then use to extend the environment with when evaluating the right hand side).
While I'm at (free) books: a great example implementation of unification (in Lisp) is in chapter 11 "Logic Programming" of Peter Norvig's "Paradigms of Artificial Intelligence Programming: Case Studies in Common Lisp".<p><a href="https://github.com/norvig/paip-lisp">https://github.com/norvig/paip-lisp</a><p>There is also an implementation in Python, but I have never tested it, just googled it now: <a href="https://github.com/dhconnelly/paip-python/blob/master/prolog.py">https://github.com/dhconnelly/paip-python/blob/master/prolog...</a><p><a href="https://dhconnelly.github.io/paip-python/docs/prolog.html" rel="nofollow">https://dhconnelly.github.io/paip-python/docs/prolog.html</a>
Type checking (type inference) is the usual application of unification in programming languages (compilers or interpreters).
Pattern matching does not need unification, because, as mentioned in the beginning of post, the "matching" is done one the left side only (no variables to "match" on the right side).