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).
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.
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).
> Despite what another comment says, unification is a valid - and rather convenient - way to implement pattern matching
The article shows that it is a valid and rather convenient way. That's why it is important to tell people that it is not necessary to use it for the "usual" pattern matching. You do (again: for the "usual" pattern matching without "variables", as in free variables, on the right side) _not_ want to use unification but "compile" the pattern matching.
If we are talking about the context of a compiler, I agree: you should compile pattern matching to decision trees (DAGs), by way of something like Pettersson's algorithm. In my comment, I specified "in an interpreter", as I think it's the natural way to implement an SML-like match construct in that context.
EDIT: Perhaps I am missing Elixir-specific context and I apologise if this is the case. It was the unification that made me click this post.
Well, I'd do that with "real" interpreters (using bytecode) too. But on the other hand also _especially_ for "toy" tree walking interpreters, to learn how to build the pattern matching tree -- as unification is needed for the type checker anyways ;).
Although I would start by reading Wadler's version (that I linked in the other post), it's IMHO a bit more accessible than Peterson's https://www.classes.cs.uchicago.edu/archive/2011/spring/2262...
But please don't get me wrong: I'm just saying that there exist other, specialised and (well, generally) more performant algorithms for pattern matching and people should have at least heard about them. If somebody decides to use unification for pattern matching, that still could be changed if performance or better error messages or ... matters.
Ah, I thought your username was familiar: you recommended Wadler's approach on a previous HN thread concerning my blog post about Pettersson/Maranget's algorithm (https://news.ycombinator.com/item?id=39241776). Yeah, I admit that Pettersson's telling of the algorithm is a bit turgid (probably why Maranget's paper - which is the same technique as its core, at least to my understanding - is cited more often).
To this end, good coverage of decent (destructive) unification algorithms can be found in any simple resource on type inference (https://okmij.org/ftp/ML/generalization/sound_eager.ml) or the Warren Abstract Machine (https://github.com/a-yiorgos/wambook/blob/master/wambook.pdf).
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.
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).