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

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?

• ViewPatterns allow arbitrary expressions in patterns, you can define foo ((div 2) -> n) = n + 1. You can also define a PatternSynonym: pattern Double n <- ((div 2) -> n) where Double n = 2 * n which you can use as a pattern foo (Double n) = 1 + n or as an expression.
– Iceland_jack
Commented Nov 19, 2023 at 18:49
• Prolog comes to mind. In Prolog functions can be run "in both directions" as in your example, at least when they have a nice enough definition. Perhaps the Oz language is also relevant (but I don't really know Oz to be more specific).
– chi
Commented Nov 19, 2023 at 19:10
• @Bergi for the unification to work, yes, but what I meant is that the user could type any function. The language would then have some mechanism to deal with failure (no unification) or non-determinism (multiple unifications).
– MaiaVictor
Commented Nov 19, 2023 at 20:15
• This is a feature of term-rewriting systems such as mathematica. Commented Nov 20, 2023 at 4:43
• 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: reference.wolfram.com/language/ref/UpValues Commented Nov 22, 2023 at 10:09

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

• Wow, that's really cool. But it raises even more questions! Just read the whole tutorial and it seems to barely mention this feature.
– MaiaVictor
Commented Nov 19, 2023 at 22:30
• This feature is called functional pattern in Curry. Commented Nov 20, 2023 at 3:46

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

• This is interesting but I'm not sure I unerstand how copatterns answer my question specifically; is it possible to implement foo (as written on the question) with it?
– MaiaVictor
Commented Nov 19, 2023 at 22:31
• @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. Commented Nov 20, 2023 at 0:08
• 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. Commented Nov 28, 2023 at 1:01

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.

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.

• At first I thought you mean Lean theorem prover, but I see you are referring to a different LEAN. Commented Nov 20, 2023 at 22:19

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.

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