6 ms·

> 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 h

by 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.
- jerf 2y ago
  When you're using pattern matching to also create variables, it's just really confusing to be able to create variables with both sides of the expression. It can get confusing enough as it is. Haskell has some extensions to pattern matching that AIUI are generally considered just too "powerful" to generally use, as it makes it very difficult to read, for instance. Plus to a first approximation you can always just swap the binding from the right to the left. A deeper analysis may reveal there's some case you can't do that, there's a lot to pattern matching and I'm not going to try to sit here and construct a case where you can't, but certainly the most common cases (by far) would just require a simple swap, so it's not an onerous requirement. And if you did construct a case where you can't, you could make a very solid software engineering case that you just shouldn't do that and should do it it two parts. To the extent this doesn't apply to prolog, it would be when prolog is functioning directly as a logic language rather than a programming language, and to be honest I'd still advise against a prolog programmer binding variables on both sides of an expression unless they're forced to for some reason just because if nothing else, you may have to understand your own code a week later. Note this specifically applies to binding variables; I'm not bothered by two already-bound variables being matched against each other, that's just prolog functioning as designed.
- jpt4 2y ago
  The Curry-Howard Correspondence is more of an observation than a theorem, but insofar as it describes the general concept of relating logics and programming languages, what is the CHC for logic programming languages? If strikes me that LP directly instantiates and manipulates logical expressions, in a "self-dual" sense; or, is it that the various "proof procedures" of the logic side map to "proof search" algorithms on the computing side?
throwawaymaths 2y ago
>And Erlang. And Haskell. And OCaml. And F#. And... JavaScript (maps), Rust, Ruby, Python...
- __jonas 2y ago
  What do you mean by this? Do maps in JavaScript have some kind of pattern matching?
  - munificent 2y ago
    JavaScript supports destructuring lists and objects (sort of like maps): https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Operators/Destructuring_assignment https://developer.mozilla.org/en-US/docs/Web/JavaScript/Refe... It's not full pattern matching because as far as I know they don't support refutable patterns, but it handles destructuring and binding to variables.
    - __jonas 2y ago
      ah, it didn’t occur to me to view destructuring as pattern matching but I guess it is a bit similar.
- weatherlight 2y ago
  It's not the same. > [a, 2, 2, b] = [1, 2, 2, 3] [1, 2, 2, 3] > a 1 > b 3 > [foo, 2, bar] = [3,3,3] %MatchError{term: [3, 3, 3]} > foo %CompileError{description: "undefined function foo/0 (there is no such import)", file: "nofile", line: 1} Ruby does something similar but the variables are bound in the scope of the case block.
  - gergo_barany 2y ago
    What's not the same as what? Based on your examples it looks like you're saying that unification is not the same as pattern matching. But nobody said it was.
weatherlight 2y ago
its not quite the same. you have to write quiet a bit of OCaml or Haskell to do the following. [foo, [2, 3, bar], baz, 5] = [1,[2,3,4], 5] If there's a match, the bindings "foo", "bar", "baz" will be bound to the values on the right hand side. if not an exception will be thrown (You are right, though, Erlang and Elixir have the same semantics, both being on the BEAM)

by troupo 2y ago

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.

jerf 2y ago
When you're using pattern matching to also create variables, it's just really confusing to be able to create variables with both sides of the expression. It can get confusing enough as it is. Haskell has some extensions to pattern matching that AIUI are generally considered just too "powerful" to generally use, as it makes it very difficult to read, for instance. Plus to a first approximation you can always just swap the binding from the right to the left. A deeper analysis may reveal there's some case you can't do that, there's a lot to pattern matching and I'm not going to try to sit here and construct a case where you can't, but certainly the most common cases (by far) would just require a simple swap, so it's not an onerous requirement. And if you did construct a case where you can't, you could make a very solid software engineering case that you just shouldn't do that and should do it it two parts. To the extent this doesn't apply to prolog, it would be when prolog is functioning directly as a logic language rather than a programming language, and to be honest I'd still advise against a prolog programmer binding variables on both sides of an expression unless they're forced to for some reason just because if nothing else, you may have to understand your own code a week later. Note this specifically applies to binding variables; I'm not bothered by two already-bound variables being matched against each other, that's just prolog functioning as designed.
jpt4 2y ago
The Curry-Howard Correspondence is more of an observation than a theorem, but insofar as it describes the general concept of relating logics and programming languages, what is the CHC for logic programming languages? If strikes me that LP directly instantiates and manipulates logical expressions, in a "self-dual" sense; or, is it that the various "proof procedures" of the logic side map to "proof search" algorithms on the computing side?

throwawaymaths 2y ago

>And Erlang. And Haskell. And OCaml. And F#. And... JavaScript (maps), Rust, Ruby, Python...

__jonas 2y ago
What do you mean by this? Do maps in JavaScript have some kind of pattern matching?
- munificent 2y ago
  JavaScript supports destructuring lists and objects (sort of like maps): https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Operators/Destructuring_assignment https://developer.mozilla.org/en-US/docs/Web/JavaScript/Refe... It's not full pattern matching because as far as I know they don't support refutable patterns, but it handles destructuring and binding to variables.
  - __jonas 2y ago
    ah, it didn’t occur to me to view destructuring as pattern matching but I guess it is a bit similar.
weatherlight 2y ago
It's not the same. > [a, 2, 2, b] = [1, 2, 2, 3] [1, 2, 2, 3] > a 1 > b 3 > [foo, 2, bar] = [3,3,3] %MatchError{term: [3, 3, 3]} > foo %CompileError{description: "undefined function foo/0 (there is no such import)", file: "nofile", line: 1} Ruby does something similar but the variables are bound in the scope of the case block.
- gergo_barany 2y ago
  What's not the same as what? Based on your examples it looks like you're saying that unification is not the same as pattern matching. But nobody said it was.

weatherlight 2y ago

its not quite the same. you have to write quiet a bit of OCaml or Haskell to do the following. [foo, [2, 3, bar], baz, 5] = [1,[2,3,4], 5] If there's a match, the bindings "foo", "bar", "baz" will be bound to the values on the right hand side. if not an exception will be thrown (You are right, though, Erlang and Elixir have the same semantics, both being on the BEAM)