Are there Haskell-like languages where equations allow for arbitrary left-hand sides?

Question

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:

1. Computing would require unification, making the language extremely slow.

2. 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?

Answer 1

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

Answer 2

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: <interactive>:7:1-22: Non-exhaustive patterns in function foo

Answer 3

Verse Calculus ($\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 (Antoy, Hanus) and Programming Logics (Andrei Voronkov, Christoph Weidenbach, eds.) are both good for deeper reading.

Answer 4

Probably the simplest paradigm that allows what you want is that of graph rewriting. One implementation for example was LEAN, the predecessor to the Clean 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.

Answer 5

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