is_list/1 and free variables

Question

Here is a first observation:

?- is_list([]), is_list([_,_,_]).
true.

Here is another observation:

?- [] = _, [_,_,_] = _.
true.

Therefore, why would is_list/1 be implemented such that

?- is_list(_).
false.

or

?- is_list([_|_]).
false.

when _ can clearly be unified with a list? Wouldn't that be logically sounder that it be true?

In SWI-Prolog's documentation for is_list/1, a note says: 

In versions before 5.0.1, is_list/1 just checked for [] or [_|_] and proper_list/1 had the role of the current is_list/1. The current definition conforms to the de facto standard.

Why is that the de facto standard?

Answer 1

As you correctly observe, is_list/1 is unsound, or rather incomplete, because it incorrectly says that there are no solutions whatsoever when the most general query is posed.

?- is_list(Ls).
false.

No list exists? Come on!

This unfortunate trait is shared by all hereditary type checking predicates like atom/1, integer/1 etc., whose incorrectness was obvious already when these predicates were conceived yet pushed through after labeling those who correctly opposed their suggested semantics as "purists" (which, at that time, lacked the complimentary character the word has since acquired).

Cases like:

?- is_list(Ls), Ls = [].
false.

?- Ls = [], is_list(Ls).
Ls = [].

clearly illustrate that something is fundamentally broken from a logical point of view with such non-monotonic tests. "Prolog's (,)/2 is not logical conjunction", yes, if you use illogical predicates in the first place in your code. Otherwise, (,)/2 is always a logical conjunction of goals.

A clean and logically correct way out is to throw instantiation errors in cases that cannot yet be determined.

library(error) and in particular must_be/2 go into a sound direction after the incorrectness of inherited illogical predicates has become unbearable even for casual users of Prolog:

?- must_be(list, X).
Arguments are not sufficiently instantiated

?- must_be(list, [_|_]).
Arguments are not sufficiently instantiated

?- must_be(list, [a,b,c]).
true.

must_be/2 is easy to use and a good first step towards more correct logic programs. Other constructs also appear on the horizon, and I hope others comment on the current status.

And now for the actual wording: Putting aside the fundamental problem outlined above, the contention alluded to in the SWI documentation is whether checking the outermost functor suffices to regard a term as a list, or whether the list must actually conform to the inductive definition of a list, which is:

• the atom [] is a list.
• if Ls is a list, then '.'(_, Ls) is a list.

Note that in recent SWI versions, [] is not even an atom, so it again breaks with this notion.