<p>In Haskell, you can define algorithms by equations that pattern-match on left-hand side <strong>constructors</strong>. For example:</p>
<pre class="lang-hs prettyprint-override"><code>data Nat = S Nat | Z

double :: Nat -&gt; Nat
double Z     = Z
double (S x) = S (S (double x))
</code></pre>
<p>Now, for a moment, imagine that the <strong>constructor</strong> restriction was lifted, and we allowed arbitrary left-hand sides:</p>
<pre><code>foo :: Nat -&gt; Nat
foo (double x) = x + 1
</code></pre>
<p>In this case, rather than matching on the <em>successor</em> of <code>x</code>, we're matching on the <em>double</em> of <code>x</code>, where <code>double</code> is an arbitrary function, rather than a constructor. As such, to compute <code>foo 10</code>, the runtime would need to match it against <code>foo (double x)</code>, which, by unification, implies <code>x = 5</code>, thus, <code>foo (double 5) = foo 10 = 5 + 1 = 6</code>; i.e., <code>6</code> is the final result. Alternatively, one could implement the same concept without patterns, as a &quot;first-class unifier&quot;. Example:</p>
<pre class="lang-hs prettyprint-override"><code>foo :: Nat -&gt; Nat
foo = \x -&gt; (solve k in (double k) == x) + 1
</code></pre>
<p>Of course, this idea isn't practical, since:</p>
<ol>
<li><p>Computing would require unification, making the language extremely slow.</p>
</li>
<li><p>It would be possible to write absurd equations, so this must be handled somehow.</p>
</li>
</ol>
<p><strong>Yet, has this concept been explored and/or implemented in any existing language?</strong></p>

<haskell><functional-programming>
Are there Haskell-like languages where equations allow for arbitrary left-hand sides?
CC BY-SA 4.0
2023-11-19T20:13:58.443Z
"*where `double` is an arbitrary function*" - well it needs to be bijective for this to work
Bergi
CC BY-SA 4.0
2023-11-20T04:43:48.997Z
This is a feature of term-rewriting systems such as mathematica.
Moonchild
CC BY-SA 4.0
2023-11-22T10:09:12.640Z
Particularly in Mathematica this can be done with "UpValues" where the you can define a value by how it is mapped by an arbitrary function, rather than the usual opposite way: https://reference.wolfram.com/language/ref/UpValues
Sean D
<p><a href="https://dl.acm.org/doi/pdf/10.1145/3607845" rel="noreferrer">Verse Calculus</a> (<span class="math-container">$\mathcal{VC}$</span>) is a newly-proposed core to a functional logic language that offers exactly this.</p>
<p>Equations in Verse can appear with the form</p>
<p><span class="math-container">$e_1 = e_2$</span>,</p>
<p>where <span class="math-container">$e_i$</span> is an arbitrary expression. <em>Logical variables</em> (variables that must be &quot;solved for&quot;) may be introduced by <span class="math-container">$\exists$</span> and can appear in any part of an expression and on either or both sides of an equation. Simple examples include:</p>
<p><span class="math-container">$\exists x \; y \; z. x = \langle y, 3 \rangle; x = \langle 2, z \rangle; y$</span></p>
<p><span class="math-container">$\exists y. y = 3 + 4; (\lambda x. x + 1)(y)$</span></p>
<p>With more mind-bending ones solving for variables passed to function calls, like:</p>
<p><span class="math-container">$\exists x y. x = \langle y, 5 \rangle; 2 = \mathit{first} (x); y$</span></p>
<p>where</p>
<p><span class="math-container">$\mathit{first} := \lambda p. \exists a b. p = \langle a, b \rangle; a$</span></p>
<p>Indeed, functional logic programming languages like those in previous answers have included these features for some time. <a href="https://dl.acm.org/doi/10.1145/1721654.1721675" rel="noreferrer">Functional Logic Programming</a> (Antoy, Hanus) and <a href="https://link.springer.com/book/10.1007/978-3-642-37651-1" rel="noreferrer">Programming Logics</a> (Andrei Voronkov, Christoph Weidenbach, eds.) are both good for deeper reading.</p>

CC BY-SA 4.0
2023-11-21T17:42:46.673Z
2023-11-21T17:42:46.673Z
list 'r
<p>Probably the simplest paradigm that allows what you want is that of <em>graph rewriting</em>. One implementation for example was <a href="https://www.researchgate.net/publication/220276855_LEAN_An_intermediate_language_based_on_graph_rewriting" rel="nofollow noreferrer">LEAN</a>, the predecessor to the <a href="https://clean-lang.org/about.html" rel="nofollow noreferrer">Clean</a> programming language.</p>
<p>The trouble with allowing arbitrary redexes like that is that the evaluation can become non-confluent and therefore non-deterministic. That is, the reduction engine may have to choose between different equations, and the final result may depend on that choice.</p>

CC BY-SA 4.0
2023-11-20T18:30:11.107Z
2023-11-20T18:30:11.107Z
Mario B.
CC BY-SA 4.0
2023-11-20T22:19:22.983Z
At first I thought you mean Lean theorem prover, but I see you are referring to a different LEAN.
The Floating Brain
<p>In theory it shouldn't be too hard to write an interpreter for a simple language that runs an arithmetic solver on expressions, so as to invert expressions and interpret</p>
<pre><code>addOne [x-1] = x
</code></pre>
<p>as</p>
<pre><code>addOne y = y+1
</code></pre>
<p>and more generally</p>
<pre><code>f [expr(x)] = something(x)
</code></pre>
<p>as</p>
<pre><code>f y | y in image(expr) = let x = expr^-1(y)
    something(x)
</code></pre>
<p>Several issues arise if the expression <code>expr</code> cannot be easily inversed.</p>
<h2>Non-injective expressions</h2>
<p>Consider:</p>
<pre><code>squareRoot [x^2] = x
</code></pre>
<p>What should <code>squareRoot 9</code> return? The solver could bind <code>x</code> to either <code>3</code> or <code>-3</code> and they would both satisfy the equation <code>9 = x^2</code>.</p>
<h2>Expressions with a non-obvious image</h2>
<p>Consider:</p>
<pre><code>nextCollatz [2 * k] = k
nextCollatz [n] = 3 * n + 1
</code></pre>
<p>Now we expect that if we call <code>nextCollatz</code> on an even integer, it should be divided by 2, but if we call it on an odd integer, then the solver should recognise that this integer cannot be written as <code>2 * k</code>, and use the second line instead.</p>
<p>This works because the solver can reasonably be expected to figure out whether an integer is even or odd.</p>
<p>Now imagine that we have two complicated functions <code>f</code> and <code>g</code> and we define:</p>
<pre><code>mystery [f(x)] = x
mystery [g(x)] = x
</code></pre>
<p>Now when we call <code>mystery 42</code>, what should the solver return? <code>f</code> and <code>g</code> are  complicated functions, and the solver cannot be expected to know whether 42 can be written as <code>f(x)</code> or must be written as <code>g(x)</code>. So the only way to find <code>x</code> such that <code>42 = f(x)</code> might be to call function <code>f</code> repeatedly and try to find an output that matches 42. However, there might be an infinity of <code>x</code> values to try, and the equation <code>42 = f(x)</code> might not have a solution, which means the interpreter needs to dovetail: it needs to start trying to solve <code>42 = g(x)</code> before it knows whether the search for <code>42 = f(x)</code> will be fruitful or will run forever. Because of this, the output of <code>mystery</code> might be non-deterministic, or at least unpredictable.</p>
<h2>Breaking the bank</h2>
<p>Consider:</p>
<pre><code>magicFactor [x*y] = (x, y)
</code></pre>
<p>Then you can call <code>magicFactor 157654575299002101047053</code> and it should return <code>(543287386049, 290186334797)</code>, breaking your bank's encryption scheme in the process.</p>
<h2>Diagonal paradox</h2>
<p>What if the expression we're trying to pattern-match on is allowed to rely on pattern-matching as well? Then we can make a diagonal argument:</p>
<pre><code>f () = case [False] of
    [f ()] -&gt; True
    _ -&gt; False

[f ()] = [False]
</code></pre>
<p>Or in the spirit of Raymond Smullyan:</p>
<pre><code>f () = case [False] of
    you pay me a million dollars -&gt; False
    [f ()] -&gt; True
    _ -&gt; False
</code></pre>
<p>The only way to get a sane evaluation of <code>f</code> is to pay the user a million dollars. But even with <code>magicFactor</code> to hack the bank, this would be a problem because haskell is supposed to be a pure functional language, and paying the user a million dollars is a side-effect.</p>
<p>Relatedly, the ruleset of the online nomic <a href="https://agoranomic.org/" rel="nofollow noreferrer">Agora</a> states:</p>
<blockquote>
<p>Definitions and prescriptions in the rules are only to be applied using direct, forward reasoning; in particular, an absurdity that can be concluded from the assumption that a statement about rule-defined concepts is false does not constitute proof that it is true.</p>
</blockquote>
<p>In other words, Agora decided that just because it's <em>possible</em> to resolve something to a truth value doesn't necessarily mean you <em>should</em>. For instance, it makes more sense for the interpreter to conclude that the function above doesn't evaluate to anything, rather than to pay you a million dollars to make it evaluable.</p>
<hr />
<p><em>Largely contributed to the content of this answer: b_jonas and ais523 from <a href="https://esolangs.org/wiki/Main_Page" rel="nofollow noreferrer">esolangs.org</a></em></p>

CC BY-SA 4.0
2023-11-27T18:02:44.973Z
2023-11-27T18:02:44.973Z
Stef
<p><a href="https://curry.pages.ps.informatik.uni-kiel.de/curry-lang.org/" rel="noreferrer">Curry</a> does exactly this kind of stuff.</p>
<pre><code>data Nat = S Nat | Z

showNat :: Nat -&gt; String
showNat Z = &quot;Z&quot;
showNat (S n) = &quot;S$ &quot;++showNat n

double :: Nat -&gt; Nat
double Z = Z
double (S n) = S $ S $ double n

foo :: Nat -&gt; Nat
foo (double x) = S x
foo (S (double x)) = x

main :: IO ()
main = do
  putStrLn . showNat . foo
        $ S$ S$ S$ Z
  putStrLn . showNat . foo
        $ S$ S$ S$ S$ Z
</code></pre>
<p><a href="https://tio.run/##lY9NCoMwEIX3c4pBXChFDyDYfaG0i@yyS7U/0jYRjdRC757OGCPSXUPC8L6Z95hUQ9e9s1bdq965WlmFB2WxRDHVD0qA/mZeLIpiYtkWhe0afV0akuYjGS06EahTZiLGaLMJWAPUZjg9zqskKgFyigwiRAiMpzdjirgY8@NnkswDozeNHooV58YI8FSNZv/uiEnqVUnpgNgOlv6115hj2DhHiqGWP7RJuPLPebY49wU" rel="noreferrer" title="Curry (PAKCS) – Try It Online">Try it online!</a> Output:</p>
<pre><code>S$ Z
S$ S$ S$ Z
</code></pre>

CC BY-SA 4.0
2023-11-19T22:18:55.870Z
2023-11-19T22:18:55.870Z
leftaroundabout
CC BY-SA 4.0
2023-11-20T03:46:21.920Z
This feature is called [functional pattern](https://en.wikipedia.org/wiki/Curry_(programming_language)#Functional_patterns) in Curry.
alephalpha
<p>Yes, this is a feature of Agda, in the form of <a href="https://agda.readthedocs.io/en/v2.6.1/language/copatterns.html" rel="noreferrer">copatterns</a>, and more generally in <a href="https://mercurylang.org/" rel="noreferrer">Mercury</a> which is a functional logic language.</p>
<p>A data type is defined by its <em>injections</em>, or constructors, and eliminated by pattern matching. A codata type is defined by its <em>projections</em>, or observations, and introduced by copattern matching. And a copattern is a pattern that describes a way of consuming a value.</p>
<p>For example, in a hypothetical Haskell with codata types, a pair could be defined as:</p>
<pre><code>codata Pair a b where
  fst :: Pair a b -&gt; a
  snd :: Pair a b -&gt; b

p :: Pair Int Int
fst p = 1
snd p = 2

-- or: p = cocase { fst _ -&gt; 1; snd _ -&gt; 2 }
</code></pre>
<p>So if <code>foo</code> is written as a codata type, and <code>double</code> constructs a value of that type, then you can translate your example:</p>
<pre><code>codata Foo where
  foo :: Foo -&gt; Nat

double :: Nat -&gt; Foo
foo (double x) = x + 1
</code></pre>
<p>However, <code>double</code> is no longer an ordinary function on naturals.</p>
<p>In Mercury, the append operator <code>++</code> as in <code>L1 ++ L2</code> is defined as a synonym of the function <code>append(L1, L2)</code>. Using this function in the head of a definition is equivalent to specifying some variable <code>L</code> and unifying <code>L = append(L1, L2)</code>. In general this may be nondeterministic, and backtrack over several ways of splitting an input list. Likewise, you can match on <code>double(X)</code> in the head of a definition; however, this also implies that <code>double</code> is a constructor of a data type.</p>
<pre><code>:- type double ---&gt; double(uint).

:- func foo(double) = uint.
foo(double(X)) = X + 1.
</code></pre>
<p>The situation is similar in other functional logic languages, even if they don’t require data type definitions. In particular, this is <em>not</em> functional inversion: the argument of <code>foo</code> must be exactly a call to <code>double(X)</code> for some <code>X</code>, not just any natural number divisible by two. For that, you’d need something more like Haskell’s <code>ViewPatterns</code>:</p>
<pre><code>λ :{
| pattern Double :: Word -&gt; Word
| pattern Double x &lt;- ((`divMod` 2) -&gt; (x, 0))
|   where
|     Double x = x * 2
| :}
λ foo (Double x) = x + 1

λ foo 20
11

λ Double 10
20

λ foo 1
*** Exception: &lt;interactive&gt;:7:1-22: Non-exhaustive patterns in function foo
</code></pre>

CC BY-SA 4.0
2023-11-19T22:29:31.753Z
2023-11-24T16:56:57.340Z
2023-11-24T16:56:57.340Z
Jon Purdy
CC BY-SA 4.0
2023-11-20T00:08:45.260Z
@MaiaVictor: In Agda or my pseudo-Haskell, I think you can’t translate `foo` directly without a wrapper type. Mercury is more like what you’re asking for. I wanted to mention both since they’re closely related. A definition like `k(f(x)) = …`, in a functional logic language, defines the continuation part `k`; in a functional language with copattern matching, it defines the function `f`. To use a function as a pattern, we need to be able to invert it in a certain sense; in a logic language, we can always invert a term by turning it into a goal—of course, the search might not be productive.
Jon Purdy
CC BY-SA 4.0
2023-11-28T01:01:27.343Z
Since you mentioned a logic language, it's also worth mentioning that constraint logic languages allow even more generality in pattern matching, at the cost of a loss of static guarantees.
Pseudonym
# Are there Haskell-like languages where equations allow for arbitrary left-hand sides?
Posted by: username_0 on 2023-11-19
In Haskell, you can define algorithms by equations that pattern-match on left-hand side constructors. For example:
data Nat = S Nat | Z

double :: Nat -> Nat
double Z     = Z
double (S x) = S (S (double x))

Now, for a moment, imagine that the constructor restriction was lifted, and we allowed arbitrary left-hand sides:
foo :: Nat -> Nat
foo (double x) = x + 1

In this case, rather than matching on the successor of x, we're matching on the double of x, where double is an arbitrary function, rather than a constructor. As such, to compute foo 10, the runtime would need to match it against foo (double x), which, by unification, implies x = 5, thus, foo (double 5) = foo 10 = 5 + 1 = 6; i.e., 6 is the final result. Alternatively, one could implement the same concept without patterns, as a "first-class unifier". Example:
foo :: Nat -> Nat
foo = \x -> (solve k in (double k) == x) + 1

Of course, this idea isn't practical, since:

Computing would require unification, making the language extremely slow.

It would be possible to write absurd equations, so this must be handled somehow.


Yet, has this concept been explored and/or implemented in any existing language?
**Tags:** haskell functional-programming
> **Comments:**
> **username_1**: "*where `double` is an arbitrary function*" - well it needs to be bijective for this to work  
> **username_2**: This is a feature of term-rewriting systems such as mathematica.  
> **username_3**: Particularly in Mathematica this can be done with "UpValues" where the you can define a value by how it is mapped by an arbitrary function, rather than the usual opposite way: https://reference.wolfram.com/language/ref/UpValues  
---
## 5 answers
### Answer by username_8 on 2023-11-19. Score: 27
Curry does exactly this kind of stuff.
data Nat = S Nat | Z

showNat :: Nat -> String
showNat Z = "Z"
showNat (S n) = "S$ "++showNat n

double :: Nat -> Nat
double Z = Z
double (S n) = S $ S $ double n

foo :: Nat -> Nat
foo (double x) = S x
foo (S (double x)) = x

main :: IO ()
main = do
  putStrLn . showNat . foo
        $ S$ S$ S$ Z
  putStrLn . showNat . foo
        $ S$ S$ S$ S$ Z

Try it online! Output:
S$ Z
S$ S$ S$ Z
> **Comments:**
> **username_9** (2023-11-20): This feature is called [functional pattern](https://en.wikipedia.org/wiki/Curry_(programming_language)#Functional_patterns) in Curry.  
---
### Answer by username_10 on 2023-11-19. Score: 18
Yes, this is a feature of Agda, in the form of copatterns, and more generally in Mercury which is a functional logic language.
A data type is defined by its injections, or constructors, and eliminated by pattern matching. A codata type is defined by its projections, or observations, and introduced by copattern matching. And a copattern is a pattern that describes a way of consuming a value.
For example, in a hypothetical Haskell with codata types, a pair could be defined as:
codata Pair a b where
  fst :: Pair a b -> a
  snd :: Pair a b -> b

p :: Pair Int Int
fst p = 1
snd p = 2

-- or: p = cocase { fst _ -> 1; snd _ -> 2 }

So if foo is written as a codata type, and double constructs a value of that type, then you can translate your example:
codata Foo where
  foo :: Foo -> Nat

double :: Nat -> Foo
foo (double x) = x + 1

However, double is no longer an ordinary function on naturals.
In Mercury, the append operator ++ as in L1 ++ L2 is defined as a synonym of the function append(L1, L2). Using this function in the head of a definition is equivalent to specifying some variable L and unifying L = append(L1, L2). In general this may be nondeterministic, and backtrack over several ways of splitting an input list. Likewise, you can match on double(X) in the head of a definition; however, this also implies that double is a constructor of a data type.
:- type double ---> double(uint).

:- func foo(double) = uint.
foo(double(X)) = X + 1.

The situation is similar in other functional logic languages, even if they don’t require data type definitions. In particular, this is not functional inversion: the argument of foo must be exactly a call to double(X) for some X, not just any natural number divisible by two. For that, you’d need something more like Haskell’s ViewPatterns:
λ :{
| pattern Double :: Word -> Word
| pattern Double x <- ((`divMod` 2) -> (x, 0))
|   where
|     Double x = x * 2
| :}
λ foo (Double x) = x + 1

λ foo 20
11

λ Double 10
20

λ foo 1
*** Exception: :7:1-22: Non-exhaustive patterns in function foo
> **Comments:**
> **username_10** (2023-11-20): @MaiaVictor: In Agda or my pseudo-Haskell, I think you can’t translate `foo` directly without a wrapper type. Mercury is more like what you’re asking for. I wanted to mention both since they’re closely related. A definition like `k(f(x)) = …`, in a functional logic language, defines the continuation part `k`; in a functional language with copattern matching, it defines the function `f`. To use a function as a pattern, we need to be able to invert it in a certain sense; in a logic language, we can always invert a term by turning it into a goal—of course, the search might not be productive.  
> **username_11** (2023-11-28): Since you mentioned a logic language, it's also worth mentioning that constraint logic languages allow even more generality in pattern matching, at the cost of a loss of static guarantees.  
---
### Answer by username_4 on 2023-11-21. Score: 6
[Verse Calculus](https://dl.acm.org/doi/pdf/10.1145/3607845) ($\mathcal{VC}$) is a newly-proposed core to a functional logic language that offers exactly this.

Equations in Verse can appear with the form

$e\_1 = e\_2$,

where $e\_i$ is an arbitrary expression. *Logical variables* (variables that must be "solved for") may be introduced by $\exists$ and can appear in any part of an expression and on either or both sides of an equation. Simple examples include:

$\exists x \; y \; z. x = \langle y, 3 \rangle; x = \langle 2, z \rangle; y$

$\exists y. y = 3 + 4; (\lambda x. x + 1)(y)$

With more mind-bending ones solving for variables passed to function calls, like:

$\exists x y. x = \langle y, 5 \rangle; 2 = \mathit{first} (x); y$

where

$\mathit{first} := \lambda p. \exists a b. p = \langle a, b \rangle; a$

Indeed, functional logic programming languages like those in previous answers have included these features for some time. [Functional Logic Programming](https://dl.acm.org/doi/10.1145/1721654.1721675) (Antoy, Hanus) and [Programming Logics](https://link.springer.com/book/10.1007/978-3-642-37651-1) (Andrei Voronkov, Christoph Weidenbach, eds.) are both good for deeper reading.
---
### Answer by username_5 on 2023-11-20. Score: 4
Probably the simplest paradigm that allows what you want is that of *graph rewriting*. One implementation for example was [LEAN](https://www.researchgate.net/publication/220276855_LEAN_An_intermediate_language_based_on_graph_rewriting), the predecessor to the [Clean](https://clean-lang.org/about.html) programming language.

The trouble with allowing arbitrary redexes like that is that the evaluation can become non-confluent and therefore non-deterministic. That is, the reduction engine may have to choose between different equations, and the final result may depend on that choice.
> **Comments:**
> **username_6** (2023-11-20): At first I thought you mean Lean theorem prover, but I see you are referring to a different LEAN.  
---
### Answer by username_7 on 2023-11-27. Score: 2
In theory it shouldn't be too hard to write an interpreter for a simple language that runs an arithmetic solver on expressions, so as to invert expressions and interpret
addOne [x-1] = x

as
addOne y = y+1

and more generally
f [expr(x)] = something(x)

as
f y | y in image(expr) = let x = expr^-1(y)
    something(x)

Several issues arise if the expression expr cannot be easily inversed.
Non-injective expressions
Consider:
squareRoot [x^2] = x

What should squareRoot 9 return? The solver could bind x to either 3 or -3 and they would both satisfy the equation 9 = x^2.
Expressions with a non-obvious image
Consider:
nextCollatz [2 * k] = k
nextCollatz [n] = 3 * n + 1

Now we expect that if we call nextCollatz on an even integer, it should be divided by 2, but if we call it on an odd integer, then the solver should recognise that this integer cannot be written as 2 * k, and use the second line instead.
This works because the solver can reasonably be expected to figure out whether an integer is even or odd.
Now imagine that we have two complicated functions f and g and we define:
mystery [f(x)] = x
mystery [g(x)] = x

Now when we call mystery 42, what should the solver return? f and g are  complicated functions, and the solver cannot be expected to know whether 42 can be written as f(x) or must be written as g(x). So the only way to find x such that 42 = f(x) might be to call function f repeatedly and try to find an output that matches 42. However, there might be an infinity of x values to try, and the equation 42 = f(x) might not have a solution, which means the interpreter needs to dovetail: it needs to start trying to solve 42 = g(x) before it knows whether the search for 42 = f(x) will be fruitful or will run forever. Because of this, the output of mystery might be non-deterministic, or at least unpredictable.
Breaking the bank
Consider:
magicFactor [x*y] = (x, y)

Then you can call magicFactor 157654575299002101047053 and it should return (543287386049, 290186334797), breaking your bank's encryption scheme in the process.
Diagonal paradox
What if the expression we're trying to pattern-match on is allowed to rely on pattern-matching as well? Then we can make a diagonal argument:
f () = case [False] of
    [f ()] -> True
    _ -> False

[f ()] = [False]

Or in the spirit of Raymond Smullyan:
f () = case [False] of
    you pay me a million dollars -> False
    [f ()] -> True
    _ -> False

The only way to get a sane evaluation of f is to pay the user a million dollars. But even with magicFactor to hack the bank, this would be a problem because haskell is supposed to be a pure functional language, and paying the user a million dollars is a side-effect.
Relatedly, the ruleset of the online nomic Agora states:

Definitions and prescriptions in the rules are only to be applied using direct, forward reasoning; in particular, an absurdity that can be concluded from the assumption that a statement about rule-defined concepts is false does not constitute proof that it is true.

In other words, Agora decided that just because it's possible to resolve something to a truth value doesn't necessarily mean you should. For instance, it makes more sense for the interpreter to conclude that the function above doesn't evaluate to anything, rather than to pay you a million dollars to make it evaluable.

Largely contributed to the content of this answer: b_jonas and ais523 from esolangs.org
---
