>> And Erlang. And Haskell. And OCaml. And F#. And..
Thanks, I didn't know that. I took the article to mean that this kind of one-sided pattern matching is unique in Elixir. My misreading.
From what I've seen it's true that most languages that have support for pattern matching have special constructs for it, whereas in Prolog it's baked in to the only data structure in the language, the term, which can be a single variable (a logic variable that can unify with ... anything).
I don't know how useful or not unification would be in a language other than Prolog to be honest. In Prolog it's an integral component of the Resolution-based theorem prover used as an interpreter of Prolog programs: resolution proceeds by unifying Horn goals to the heads of definite clauses, to produce new goals, recursively. More over, when one runs a Prolog "query" the result of the query itself is the substitution of the variables in the query, i.e. the substitution that makes the query true [1]; a substitution derived and propagated by unification.
I like how George W. Lloyd describes the use of unification in Prolog. Apologies in advance for the long-form quote:
The idea that first order logic, or at least substantial subsets of it, could be used as a programming language was revolutionary, because, until 1972, logic had only ever been used as a specification or declarative language in computer science. However, what [R. Kowalski, Predicate Logic as a Programming Language, 1974] shows is that logic has a procedural interpretation, which makes it very effective as a programming language. Briefly, a program clause A <- B1, ..., Bn is regarded as a procedure definition. If <- C1, ..., Ck is a goal, then each Cj is regarded as a procedure call. A program is run by giving it an initial goal. If the current goal is <- C1, ..., Ck, a step in the computation involves unifying some Cj with the head A of a program clause A <- B1, ... Bn and thus reducing the current goal to the goal <-(C1, ..., Cj-1, B1, ..., Bn, Cj+1, ..., Ck)θ, where θ is the unifying substitution. Unification thus becomes a uniform mechanism for parameter passing, data selection and data construction. The computation terminates when the empty goal is produced.
And that's first-order SLD-Resolution, with unification, in a nutshell! From George Lloyd: Foundations of Logic Programming, second Ed. 1993.
There's a copy of the book here:
https://archive.org/details/foundationsoflog0000lloy_o7l2
But it's a limited preview :/
________
[1] ... well, the substitution that makes the Horn goal that we call a "query" false, in reality, because Prolog proves things by refutation but we fudge it a bit.