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
ViewPatterns
allow arbitrary expressions in patterns, you can definefoo ((`div` 2) -> n) = n + 1
. You can also define aPatternSynonym
:pattern Double n <- ((`div` 2) -> n) where Double n = 2 * n
which you can use as a patternfoo (Double n) = 1 + n
or as an expression. $\endgroup$