By the way, SMT solvers are (sometimes) able to do this in a non-brute-force way. That is, they will actually make logical deductions to avoid exploring impossible parts of the space. I think logic programming languages will also commonly implement efficient searches for satisfying assignments so that you're not exploring the literal Cartesian product of the variable's domains in every case.
I've heard repeatedly about the interesting discovery that Boolean satisfiability is "hard in theory, but not in practice" because most constraint solving that we want to do inspired by real-world problems apparently has structure that software can identify.
But I also think this is an interesting challenge in its own right for thinking about polymorphism, even without getting into how to find opportunities to make the search non-exhaustive.
I am not sure this really is "amb" in all its glory. The incredible power of amb comes from the fact that some of the computations involved may be crashing or diverging. Crashes or non-termination are avoided by amb in favour of the successful computations. Otherwise is just the nondeterminism monad.
C/POSIX permits a simple (albeit wildly inefficient) implementation that handles crashing:
#include <stdlib.h>
#include <unistd.h>
#include <sys/types.h>
#include <sys/wait.h>
// Return an integer in the range [0, n) which
// causes execution to succeed.
unsigned amb(const unsigned n)
{
if (n == 0) _exit(42);
for (unsigned i = 0; i < n - 1; ++i)
{
const pid_t child = fork();
if (child < 0) abort();
if (child == 0) return i;
int wstatus;
if (waitpid(child, &wstatus, 0) < 0) abort();
if (WIFEXITED(wstatus) && WEXITSTATUS(wstatus) == 0) _exit(0);
}
return n - 1;
}
You could of course parallelize this to handle nontermination, at the expensive of potentially many concurrent processes for a high n.
You can make other fun time-traveling functions following the above pattern. My favorite I call the "Groundhog Day" function, or "Cause and Effect" for Star Trek fans: when first called, it returns zero; if the program later fails, it is restarted from that function call, which returns the exit code. (I'm not really sure how useful this is.)
This is analogous to the shift and reset operators from delimited continuations. It's also analogous to branching and cancelation from Chu spaces or the idea of adjoint and norm.
I've been thinking about this a bunch. I put together a brain dump that I improve over time
It took me a good 15 minutes trying to figure out what this was but it looks like a really neat way to solve certain problems. The example provided makes it appear that Amb is a way to build a solver of a defined problem. Is the efficiency of this totally up to the language?
It reminds me of riddles "what ends the first and starts the next for each"
It’s just a declarative way of solving a problem, like a SQL query or my C# .csx implementation.
I’m actually quite surprised that there isn’t any SQL implementation...
The pattern of some code calling a function (amb) causing the original code to get called again later with the function returning different values makes me think of React hooks. It's a very convenient pattern for some use-cases.
The C# solutions while solving the problem in a generic way creating an Amb class are far too verbose for me...
I just added a .csx version that uses LINQ query syntax that it’s quite more compact (and probably readable).
Your solution is more concise and I like the way it reads, but I'm not sure it actually fulfills the problem definition:
As the page explains:
The goal of this task isn't to simply process the four lists of words with explicit, deterministic program flow such as nested iteration, to trivially demonstrate the correct output. The goal is to implement the Amb operator, or a facsimile thereof that is possible within the language limitations.
I completely agree, but it’s an almost generic way of solving that problem in C#.
It’s pretty much equivalent to the F#, Haskell and python list comprehension solution listed in that page.
The only difference is that the F# and Haskell solutions are kind of cheating creating an amb function that is just id (the identity function) while the python solution is more honest because you don’t really need amb to solve that problem with list comprehension (or the list monad).
My solution is not completely generic just because of the limitations in C# LINQ query syntax that requires you to use the equals keyword and you can have the second argument appear only after the equals keyword, so for example I had to cheat using b / 8 in the solution (instead of the more obvious a*b == 8) to find the number that multiplied by themselves give 8. So in that case it will explode if 0 is an element of the second array, and it’s easily solved just by adding a where clause in the definition of the second array, but I didn’t want to overcomplicate the solution because it doesn’t add anything useful about the general problem. If I wanted to cheat like the F# and Haskell solutions I could have added just this line:
T[] Amb(params T[] l) => l;
and I would have defined the arrays in this way:
var w1 = Amb("the", "that", "a");
But i thought that it was an unnecessary gimmick just to have the Amb operator appear there even if it’s not needed (0 lines of code Amb definition as some comments in here suggest).
About last year, this [1] article on the Amb operator was featured in HN, so back then, I grabbed the Rosettacode Go example and wrote a blogpost[2], going through such an example. Feel free to check it out!
Not exactly. I had to use SelectMany (flatmap) in my .csx solution, but the core of the solution is the join (or the for-if in the python list comprehension solution and the if-guard over the list monad in the F#/Haskell solutions)
The PureBasic and Rust versions don't seem valid to me. They each have a so-called "Amb" function that can only process lists of words that start and end with the same letters. And if they can't even get the prompt right, I wouldn't trust how well they act as examples of their respective languages.
The F# version... it's okay, I guess, but the fully-functional "declare all variables at the start, then filter" style is definitely easy mode. It's not really comparable to an 'Amb' that properly supports imperative code, letting you declare ambiguous variables, compute things with them, then use those computations to declare more ambiguous variables.
The F# version doesn't really implement Amb either. It's similar to the PureBasic and Rust versions in that it can only work on sequences by checking that the last item in sequence #1 is the same as the first thing in sequence #2.
If I'm reading the page correctly, the task is to create a general Amb implementation and merely demonstrate it using the data provided, and not to create a solution that only works on data similar to the sample data.
So I don't believe any of the PureBasic, Rust, or F# solutions meet the requirements. Though since it's a wiki, someone might have gone in and edited/added to the solutions after I wrote this. :)
In comparison, the class-based C# solutions are a lot more verbose but appear to actually solve the problem that was defined.
The F# version isn't that limited. You can replace the 'if' with arbitrary logic, and that 'if' is outside of the amb 'implementation'. It can do lots of different computations with that structure. But there's no straightforward way to do things more complicated than a series of amb declarations followed by a series of amb asserts.
It’s because you don’t actually need the Amb operator to solve that problem with list comprehension and the list monad. Adding it it’s just superfluous. The C# classes solution may meet the requirements but I still think that my csx solution (kind of similar to the Haskell, F# and python list comprehension) is more compact and readable.
The first two C# solutions come closer to actually implementing Amb, though.
The Purebasic solution depends on the operands being strings, and the F# solution depends on them being sequences. And the way that the 'Ambassert' works in both of them is hardcoded, too.
Since the problem was 'create an Amb implementation and demonstrate it using the data below' and not 'create an Amb-like thing that can only solve for cases where the operands are strings/sequence and the last item in operand 1 must match the first item in operand 2', I believe that the C# solutions actually solve the problem, while the Purebasic and F# solutions do not.
The C# classes solutions are doing the same thing as the F# solution, but in a more complicated way.
You don’t really need the Amb operator to solve that problem using the list monad or list comprehension or doing a join.
I’ve never seen anyone complain that you should have an Amb operator in SQL when you are doing a JOIN.
Which ones? The ones that are returning an invalid result or the ones where an Amb operator is not really needed and just don’t use it (or just cheat defining it as the id function)?
Take, for example, Tcl brutforce, Clojure and Wolfram which is written to only solve an example with words.
Implementation in D does not seem to be right: they just define a function that takes list of lists and a function, which is not exactly what is required in problem statement.
I've heard repeatedly about the interesting discovery that Boolean satisfiability is "hard in theory, but not in practice" because most constraint solving that we want to do inspired by real-world problems apparently has structure that software can identify.
But I also think this is an interesting challenge in its own right for thinking about polymorphism, even without getting into how to find opportunities to make the search non-exhaustive.