5

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?

repeat
  • 18,496
  • 4
  • 54
  • 166
Fatalize
  • 3,513
  • 15
  • 25

1 Answers1

6

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.

repeat
  • 18,496
  • 4
  • 54
  • 166
mat
  • 40,498
  • 3
  • 51
  • 78
  • 3
    But `must_be(list, non_list)` produces a type error when a simple failure might be more appropriate. Maybe [`itype`](http://stackoverflow.com/a/30600104/772868) is a solution. – false Jul 01 '16 at 22:21
  • 1
    Yes, either this, or maybe a flag that turns type errors into silent failures? – mat Jul 02 '16 at 05:57
  • 1
    The actual problem comes with goals that succeed as a result of some silent failure. This is why even the idea of "silent failure" gives me the creeps—it's just begging for troubles... it would necessitate some way of making sure silent failure was **not** used when proving some goal. – repeat Jul 02 '16 at 10:58
  • How about using the word "legacy" instead of "hereditary" when speaking about predicates, code, etc.? – repeat Jul 02 '16 at 11:02
  • 1
    Flags are the lowest technology solution. A `call_silent_failure/1` or similar may be more appropriate. – false Jul 02 '16 at 15:07
  • For occurs check, we also have: `unify_with_occurs_check/2` *and* the flag `occurs_check`, which I think is OK! – mat Jul 03 '16 at 11:59
  • Well, better than nothing. – false Jul 04 '16 at 15:24