10 ms·

Unification in Elixir

186 points by weatherlight 2y ago

ReleaseCandidat 2y ago
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).
- YeGoblynQueenne 2y ago
  The one-sided pattern matching seems to be a peculiarity of Elixir. The post above discusses an implementation of full unification without that restriction. To clarify, unification is not generally restricted to one-sided matching only. Is unification unnecessary for pattern matching? I think that depends on what you meany by "pattern matching". In programming cirlces "pattern matching" usually means matching strings. Now, unification is Turing-complete pattern matching, meaning that it goes well beyond e.g. regular expressions that can only match the set of strings recognised by regular automata. For instance, in Prolog, you can unify a variable with an entire Prolog program and call the program at runtime, etc. So if you need "pattern matching" only to match strings then you probably don't need the full power of unification. If I understand correctly (not an expert) Hindley-Milner type checking, the type checking that uses unification, relies exactly on that ability of unification to match entire programs. Anyway that kind of type checking is indeed pattern matching by unification. So it's not different than pattern matching on strings with regular expressions. The difference is only in what kinds of strings can be matched.
  - troupo 2y ago
    > The one-sided pattern matching seems to be a peculiarity of Elixir. And Erlang. And Haskell. And OCaml. And F#. And... As far as I understand, only Prolog has unification (out of more-or-less used/known languages). And in languages that require (rather awkward and verbose) workarounds for this functionality, it's hard to see the immediate value of unification.
    - YeGoblynQueenne 2y ago
      >> 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 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.
  - ReleaseCandidat 2y ago
    > I think that depends on what you meany by "pattern matching" Oh, yes, that's true. "Pattern matching" as that what normally is used in "functional programming languages". This kind of pattern matching does not need unification. The IMHO best (correct, but understandable and with all needed definitions) explanation of it is in chapters 4 "STRUCTURED TYPES AND THE SEMANTICS OF PATTERN-MATCHING" and 5 "EFFICIENT COMPILATION OF PATTERN-MATCHING" of Peyton Jones et al., "The implementation of functional programming languages". https://simon.peytonjones.org/slpj-book-1987/ https://simon.peytonjones.org/slpj-book-1987/ > In programming cirlces "pattern matching" usually means matching strings. Depends on the "circle" ;) https://en.wikipedia.org/wiki/Pattern_matching https://en.wikipedia.org/wiki/Pattern_matching
    - YeGoblynQueenne 2y ago
      Thanks, I don't really know much about Functional Programming. My expertise is in logic programming which btw is a different paradigm. I've heard it said that they're similar and it seems to me the reason was the support for pattern matching in functional languages. I agree that what "pattern matching" means depends on a programmer's background. It's interesting that the wikipedia article that you link to does not mention "unification" at all and only has one reference in Prolog as one of a group of example languages with a "pattern matching construct"; which is not how I would describe the use of the unification algorithm in Prolog. To be honest, I am not sure what is meant by "pattern matching". It seems to be a loosely defined term, like "Finite State Machine" (as opposed to "Finite State Automaton"). I expect that the book you linked to has a more formal treating, perhaps, but from what I can tell from a quick look the "pattern matching" here is based on types. In Prolog, unification is used to bind values to logic variables, which do not have types. So a variable, X, in Prolog can unify, i.e. "match with" absolutely anything. A "pattern" then can be formed by constructing terms (the only data structure in Prolog) with "holes" like p(X, a, b, Y,[1,2,3|Tail], f(Z)) etc. where capital letters are variables. One use of this ability is to manipulate singly-linked lists to insert in or remove elements from their tail, where normally only the head of such a list can be accessed directly. What I mean is that in Prolog a list is denoted by the special syntax [H|T] where H is the head of a list (and can be any term, including another list) and T is the tail of the list, another list. Normally one appends to a list in Prolog using the append/3 predicate: append([], L, L). append([H|T], L, [H|R]) :- append(T, L, R). This works on ordinary lists, but it is also possible to define a "difference list" as a term, e.g. like: [a,b,c,d|T]-T Where T is a variable bound to the end of the tail of the list. Two difference lists like that one can be appended with the following predicate: append_dl(Xs-Ys, Ys-Zs, Xs-Zs). For example: ?- Xs = [a,b,c,d|T1]-T1, Ys = [e,f,g,h|T2]-T2, append_dl(Xs,Ys,Zs). Xs = [a,b,c,d,e,f,g,h|T2]-[e,f,g,h|T2], T1 = [e,f,g,h|T2], Ys = [e,f,g,h|T2]-T2, Zs = [a,b,c,d,e,f,g,h|T2]-T2. The result of appending is in Zs, but you can see the result of the intermediary unification steps in the other variables echoed in the Prolog REPL (the "listener"). Of course, because this is Prolog you can also use the same predicate to split a list: ?- Xs = [a,b,c,d|T1]-T1, Zs = [a,b,c,d,e,f,g,h|T2]-T2, append_dl(Xs,Ys,Zs). Xs = [a,b,c,d,e,f,g,h|T2]-[e,f,g,h|T2], T1 = [e,f,g,h|T2], Zs = [a,b,c,d,e,f,g,h|T2]-T2, Ys = [e,f,g,h|T2]-T2. Where Ys is what remains if we split Xs from Zs. Appending or splitting lists like this is preferred to append/3 because it appends the two lists in a single operation so it can be used to economically put a list together in a loop. The same technique is used with Prolog's Definite Clause Grammars where the "difference" in a difference list is the start and end of a string accepted by a grammar, acting as a parser. https://en.wikipedia.org/wiki/Definite_clause_grammar https://en.wikipedia.org/wiki/Definite_clause_grammar Sterling and Shapiro's "The Craft of Prolog" has a nice chapter on "Incomplete Data Structures" using difference lists and patterns with "holes" but I don't think there's a free version online, unfortunately.
  - gergo_barany 2y ago
    > Now, unification is Turing-complete pattern matching No. First-order syntactic unification is not Turing complete. The combination of unification and resolution is Turing complete. > For instance, in Prolog, you can unify a variable with an entire Prolog program and call the program at runtime, etc. Lots of languages allow you to do this. Lisp had "eval" ten years before Prolog existed. Unification is not necessary for this. Prolog is great, unification is great. Some other things are great too.
ReleaseCandidat 2y ago
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". https://github.com/norvig/paip-lisp https://github.com/norvig/paip-lisp There is also an implementation in Python, but I have never tested it, just googled it now: https://github.com/dhconnelly/paip-python/blob/master/prolog.py https://github.com/dhconnelly/paip-python/blob/master/prolog... https://dhconnelly.github.io/paip-python/docs/prolog.html https://dhconnelly.github.io/paip-python/docs/prolog.html
contificate 2y ago
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). 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 https://okmij.org/ftp/ML/generalization/sound_eager.ml) or the Warren Abstract Machine (https://github.com/a-yiorgos/wambook/blob/master/wambook.pdf 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).
- ReleaseCandidat 2y ago
  > 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.
  - contificate 2y ago
    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.
deleted 2y ago
[deleted]

186 points by weatherlight 2y ago

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).

YeGoblynQueenne 2y ago
The one-sided pattern matching seems to be a peculiarity of Elixir. The post above discusses an implementation of full unification without that restriction. To clarify, unification is not generally restricted to one-sided matching only. Is unification unnecessary for pattern matching? I think that depends on what you meany by "pattern matching". In programming cirlces "pattern matching" usually means matching strings. Now, unification is Turing-complete pattern matching, meaning that it goes well beyond e.g. regular expressions that can only match the set of strings recognised by regular automata. For instance, in Prolog, you can unify a variable with an entire Prolog program and call the program at runtime, etc. So if you need "pattern matching" only to match strings then you probably don't need the full power of unification. If I understand correctly (not an expert) Hindley-Milner type checking, the type checking that uses unification, relies exactly on that ability of unification to match entire programs. Anyway that kind of type checking is indeed pattern matching by unification. So it's not different than pattern matching on strings with regular expressions. The difference is only in what kinds of strings can be matched.
- troupo 2y ago
  > The one-sided pattern matching seems to be a peculiarity of Elixir. And Erlang. And Haskell. And OCaml. And F#. And... As far as I understand, only Prolog has unification (out of more-or-less used/known languages). And in languages that require (rather awkward and verbose) workarounds for this functionality, it's hard to see the immediate value of unification.
  - YeGoblynQueenne 2y ago
    >> 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 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.
- ReleaseCandidat 2y ago
  > I think that depends on what you meany by "pattern matching" Oh, yes, that's true. "Pattern matching" as that what normally is used in "functional programming languages". This kind of pattern matching does not need unification. The IMHO best (correct, but understandable and with all needed definitions) explanation of it is in chapters 4 "STRUCTURED TYPES AND THE SEMANTICS OF PATTERN-MATCHING" and 5 "EFFICIENT COMPILATION OF PATTERN-MATCHING" of Peyton Jones et al., "The implementation of functional programming languages". https://simon.peytonjones.org/slpj-book-1987/ https://simon.peytonjones.org/slpj-book-1987/ > In programming cirlces "pattern matching" usually means matching strings. Depends on the "circle" ;) https://en.wikipedia.org/wiki/Pattern_matching https://en.wikipedia.org/wiki/Pattern_matching
  - YeGoblynQueenne 2y ago
    Thanks, I don't really know much about Functional Programming. My expertise is in logic programming which btw is a different paradigm. I've heard it said that they're similar and it seems to me the reason was the support for pattern matching in functional languages. I agree that what "pattern matching" means depends on a programmer's background. It's interesting that the wikipedia article that you link to does not mention "unification" at all and only has one reference in Prolog as one of a group of example languages with a "pattern matching construct"; which is not how I would describe the use of the unification algorithm in Prolog. To be honest, I am not sure what is meant by "pattern matching". It seems to be a loosely defined term, like "Finite State Machine" (as opposed to "Finite State Automaton"). I expect that the book you linked to has a more formal treating, perhaps, but from what I can tell from a quick look the "pattern matching" here is based on types. In Prolog, unification is used to bind values to logic variables, which do not have types. So a variable, X, in Prolog can unify, i.e. "match with" absolutely anything. A "pattern" then can be formed by constructing terms (the only data structure in Prolog) with "holes" like p(X, a, b, Y,[1,2,3|Tail], f(Z)) etc. where capital letters are variables. One use of this ability is to manipulate singly-linked lists to insert in or remove elements from their tail, where normally only the head of such a list can be accessed directly. What I mean is that in Prolog a list is denoted by the special syntax [H|T] where H is the head of a list (and can be any term, including another list) and T is the tail of the list, another list. Normally one appends to a list in Prolog using the append/3 predicate: append([], L, L). append([H|T], L, [H|R]) :- append(T, L, R). This works on ordinary lists, but it is also possible to define a "difference list" as a term, e.g. like: [a,b,c,d|T]-T Where T is a variable bound to the end of the tail of the list. Two difference lists like that one can be appended with the following predicate: append_dl(Xs-Ys, Ys-Zs, Xs-Zs). For example: ?- Xs = [a,b,c,d|T1]-T1, Ys = [e,f,g,h|T2]-T2, append_dl(Xs,Ys,Zs). Xs = [a,b,c,d,e,f,g,h|T2]-[e,f,g,h|T2], T1 = [e,f,g,h|T2], Ys = [e,f,g,h|T2]-T2, Zs = [a,b,c,d,e,f,g,h|T2]-T2. The result of appending is in Zs, but you can see the result of the intermediary unification steps in the other variables echoed in the Prolog REPL (the "listener"). Of course, because this is Prolog you can also use the same predicate to split a list: ?- Xs = [a,b,c,d|T1]-T1, Zs = [a,b,c,d,e,f,g,h|T2]-T2, append_dl(Xs,Ys,Zs). Xs = [a,b,c,d,e,f,g,h|T2]-[e,f,g,h|T2], T1 = [e,f,g,h|T2], Zs = [a,b,c,d,e,f,g,h|T2]-T2, Ys = [e,f,g,h|T2]-T2. Where Ys is what remains if we split Xs from Zs. Appending or splitting lists like this is preferred to append/3 because it appends the two lists in a single operation so it can be used to economically put a list together in a loop. The same technique is used with Prolog's Definite Clause Grammars where the "difference" in a difference list is the start and end of a string accepted by a grammar, acting as a parser. https://en.wikipedia.org/wiki/Definite_clause_grammar https://en.wikipedia.org/wiki/Definite_clause_grammar Sterling and Shapiro's "The Craft of Prolog" has a nice chapter on "Incomplete Data Structures" using difference lists and patterns with "holes" but I don't think there's a free version online, unfortunately.
- gergo_barany 2y ago
  > Now, unification is Turing-complete pattern matching No. First-order syntactic unification is not Turing complete. The combination of unification and resolution is Turing complete. > For instance, in Prolog, you can unify a variable with an entire Prolog program and call the program at runtime, etc. Lots of languages allow you to do this. Lisp had "eval" ten years before Prolog existed. Unification is not necessary for this. Prolog is great, unification is great. Some other things are great too.

ReleaseCandidat 2y ago

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". https://github.com/norvig/paip-lisp https://github.com/norvig/paip-lisp There is also an implementation in Python, but I have never tested it, just googled it now: https://github.com/dhconnelly/paip-python/blob/master/prolog.py https://github.com/dhconnelly/paip-python/blob/master/prolog... https://dhconnelly.github.io/paip-python/docs/prolog.html https://dhconnelly.github.io/paip-python/docs/prolog.html

contificate 2y ago

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). 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 https://okmij.org/ftp/ML/generalization/sound_eager.ml) or the Warren Abstract Machine (https://github.com/a-yiorgos/wambook/blob/master/wambook.pdf 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).

ReleaseCandidat 2y ago
> 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.
- contificate 2y ago
  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.

deleted 2y ago

[deleted]