Unusual behaviour of findall

Question

The following looks very unusual :

?- findall(X, member(X, [1, 2, 3]), X).
X = [1, 2, 3].

The trace even more so

?- trace, findall(X, member(X, [1, 2, 3]), X).
^  Call: (11) findall(_100058, member(_100058, [1, 2, 3]), _100058) ? creep
^  Exit: (11) findall([1, 2, 3], user:member([1, 2, 3], [1, 2, 3]), [1, 2, 3]) ? creep
X = [1, 2, 3]

Thinking in terms of semantics of findall this makes little sense. What is going on?

Answer 1

To expand on my comments, maybe this might help:

?- findall(X, member(X, [1, 2, 3]), Xs).
Xs = [1, 2, 3].

If you look closely, you will see that Prolog (SWI, in this case) did not print a substitution for X. This means that X is not bound when the query succeeds. Indeed:

?- findall(X, member(X, [1, 2, 3]), Xs), var(X).
Xs = [1, 2, 3].

This does not mean that X is never bound while the query executes:

?- findall(X, ( member(X, [1, 2, 3]), writeln(X) ), Xs), var(X).
1
2
3
Xs = [1, 2, 3].

But after all solutions have been generated, X is unbound and can be bound to some other value -- such as the list of solutions. This will work in any standard conforming Prolog, as the standard says explicitly that findall only tries to unify its third argument after it has created the list of solutions. It even contains an example with sharing between the template and the list of instantiations:

findall(X, (X=1;X=2), [X, Y]).
   Succeeds, unifying X with 1, and Y with 2.

So how does this binding and unbinding work? With a failure-driven loop, as quoted in rajashekar's answer from the SWI-Prolog implementation. In general, succeeding predicates bind some variables. When at some later point something fails (or, equivalently, the user presses ; when prompted by the toplevel), backtracking takes place: It unbinds variables to allow them to take new values, then retries some goal.

What goes on inside findall is the same as goes on when you write the following:

?- ( member(X, [1, 2, 3]), writeln(X), false ; true ), var(X).
1
2
3
true.

So while findall is very impure, it is not so impure as to be completely un-Prolog-like. In fact, we can write our own:

:- dynamic my_findall_bag/1.

my_findall(Template, Goal, Instances) :-
    % initialization
    retractall(my_findall_bag(_)),
    asserta(my_findall_bag([])),
    
    % collect solutions
    (   call(Goal),
        copy_term(Template, NewSolution),
        retract(my_findall_bag(PreviousSolutions)),
        asserta(my_findall_bag([NewSolution | PreviousSolutions])),
        % failure-driven loop: after saving the solution, force Goal to
        % generate a new one
        false
    ;   true ),

    % cleanup and finish; the saved solutions are in reversed order (newest
    % first), so reverse them
    retract(my_findall_bag(AllSavedSolutions)),
    reverse(AllSavedSolutions, Instances).

This behaves as expected:

?- my_findall(X, member(X, [1, 2, 3]), Xs).
Xs = [1, 2, 3].

Or even:

?- my_findall(X, member(X, [1, 2, 3]), X).
X = [1, 2, 3].

A minor problem with this is that the instantiation of Goal should be checked. A major problem with this is that all my_findall calls share the same bag, so calling my_findall from inside a my_findall (or in parallel) will make you unhappy. This could be fixed using some sort of gensym mechanism to give each my_findall run its unique key into the database.

As for the trace output, it is an unfortunate consequence of wanting to express "your goal succeeded with such-and-such bindings" on one line. At the point of success, it is true that findall(X, ..., X) succeeded, and it is true that X = [1, 2, 3], and hence it is true that the successful instance of the goal is findall([1, 2, 3], ..., [1, 2, 3]).

Consider:

forty_two(FortyTwo) :-
    var(FortyTwo),
    FortyTwo = 42.

my_call(Goal) :-
    format('about to call ~w~n', [Goal]),
    call(Goal),
    format('success: ~w~n', [Goal]).

For example:

?- my_call(forty_two(X)).
about to call forty_two(_2320)
success: forty_two(42)
X = 42.

So forty_two(42) is a succeeding instance of forty_two(X). Even though forty_two(42) does not succeed:

?- forty_two(42).
false.

It is logical that printing the term forty_two(X) in an environment with X = 42 prints forty_two(42). I think the problem is that this logical behavior sticks out as strange among all the non-logical stuff going on here.

Answer 2

I did some code diving to try and figure out what is going on. In swi-prolog listing(findall, [source(true)]). gives the following code :

findall(Templ, Goal, List) :-
    findall(Templ, Goal, List, []).

findall(Templ, Goal, List, Tail) :-
    setup_call_cleanup(
        '$new_findall_bag',
        findall_loop(Templ, Goal, List, Tail),
        '$destroy_findall_bag').

findall_loop in the appropriate file is as follows :

findall_loop(Templ, Goal, List, Tail) :-
    (   Goal,
        '$add_findall_bag'(Templ)   % fails
    ;   '$collect_findall_bag'(List, Tail)
    ).

After consulting the C source files, I found out that findall/4 is setting up a global variable in C-source ('$new_findall_bag') and findall_loop/4 is pushing the Templ to it when the Goal succeeds (with '$add_findall_bag'(Templ)). When the Goal fails Templ is uninstantiated and hence the final clause '$collect_findall_bag'(List, Tail) succeeds even when List and Templ are the same variable.

We can see in trace that Templ is usuall uninstantiated.

?- trace, findall(X, member(X, [1, 2, 3]), Xs).
^  Call: (11) findall(_28906, member(_28906, [1, 2, 3]), _28916) ? creep
^  Exit: (11) findall(_28906, user:member(_28906, [1, 2, 3]), [1, 2, 3]) ? creep
Xs = [1, 2, 3].

So the process of finding all instantiations of Templ so that the Goal succeeds is separate from the process of collecting all those instantiations into the variable List and hence we can use the same variable without causing and error. But the semantics of writing such a clause is not making much sense to me.

EDIT: Similar situation occurs in gprolog, where the process of collecting solutions and that of retriving them are separate. Relevant Yap code also looks quite similar, but i was not able to install it to check.