Comment by YeGoblynQueenne | Hacker News Reader

Comment by YeGoblynQueenne | Hacker News Reader

Parent Full thread

YeGoblynQueenne

That sounds right. I guess then "pattern matching" as in Elixir et al. is really just one-sided unification. Which makes me wonder- why don't those languages go all the way?

At a guess, that's something to do with the difficulty to implement unification efficiently. The first description of Unification, by J. Alan Robinson (who first described Resolution) had exponential time complexity and it took a while to find efficient unification algorithms. Perhaps the designers of functional languages simply don't need the hassle and can make do with something more efficient, less complete. That would make good, practical sense in languages that do not use Resolution as an interpreter- it's Resolution that absolutely needs unification (there's ground Resolution, without the need for unification, but it's restricted to propositional terms without first-order variables).

Pattern matching as is in Erlang, or how it is in most modern languages, was not there at some point and was considered novel and exotic. Now most everyone can do [X, Y | _] = [1, [2], 3, 4] and it's not a seen as something advanced.

I am not sure if it was ever called "unification" in Erlang, it was always called "pattern matching". But the equal sign did retain its name as the "match" operator: https://www.erlang.org/doc/system/expressions.html#the-match.... And that is a legacy of Prolog. I never read X=1 as "make X equal to 1", in my head I always read it as "match X to 1".

At some point, I also wondered: why didn't they go all the way and just bring in Prolog's full unification. They obviously liked Prolog; Erlang was developed in Prolog initially, even. Well, it turns out with unification we'd have to carry the match "hole" around until we might a match. But Erlang has lightweight processes with isolated heaps which communicate via messages, so now we'd need to pass these "holes" around from process to process until say one of the processes somewhere manages to unify the value, and then have it propagate across the system to original query. That breaks isolation. So you see how the two neat features came into a conflict and they picked one over the other, and rightly so it seems.

YeGoblynQueene, would you be amenable to discussing certain questions of logic programming via e-mail? I am reading about Jean-Yves Girard's "Stellar Resolution" model of computation, and would greatly appreciate a knowledgeable counterpart in the investigation.

Reply on news.ycombinator.com