TYPEP signals a dubious error combining MEMBER and SATISFIES

Bug #1717472 reported by Jim Newton
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
SBCL
Won't Fix
Undecided
Unassigned

Bug Description

SBCL signals an TYPE-ERROR evaluating the following expression

 (typep 0.3 '(and integer (satisfies evenp) (member 1 2 3)))

but not on

 (typep 0.3 '(and integer (satisfies evenp)))

There is a discussion on comp.lang.lisp as to whether this behavior is conforming.
The spec says that (and integer (satisfies evenp)) is a valid type specifier, but
it does so in an example. One interpretation might be that the example is
not binding, so (and integer (satisfies evenp)) can be treated as non-conforming,
thus allowing any behavior to (typep 0.3 '(and integer (satisfies evenp))
Nevertheless, SBCL, evaluates that expression to nil.

It is when adding the (member 1 2 3) as the 3rd operand of the and where the
error is encountered.

The SBCL developers might well decide to mark this issue as WONT-FIX. But
I'm filing the bug report in case you believe the SBCL behavior to be
inconsistent.

The relevant pages in the spec are
http://www.lispworks.com/documentation/lw60/CLHS/Body/t_satisf.htm
http://www.lispworks.com/documentation/lw51/CLHS/Body/t_and.htm

The latter specifies that (and A B) is the intersection of A and B, implying
that it is the same as (and B A). However, the former gives the example of
(and integer (satisfies evenp)) which violates this supposed principle.

There is a discussion about a conflict between cltl2 and the cl spec
https://stackoverflow.com/questions/29768959/using-satisfies-with-and-in-common-lisp

Apparently section 4.4 of cltl2 forbids an implementation for changing the order
of the operands of the AND type specifier, but the CL specification omits this
restriction.

The comp.lang.lisp discussion:
https://groups.google.com/forum/#!topic/comp.lang.lisp/dzJfkOulkJ0

Here is the version information.

uname -a
Darwin johan.lrde.epita.fr 15.6.0 Darwin Kernel Version 15.6.0: Sun Jun 4 21:43:07 PDT 2017; root:xnu-3248.70.3~1/RELEASE_X86_64 x86_64

sbcl --version
SBCL 1.3.14

CL-USER> *features*
(:LISP-UNIT :BORDEAUX-THREADS :CLOSER-MOP :THREAD-SUPPORT :SWANK :QUICKLISP
 :ASDF-PACKAGE-SYSTEM :ASDF3.1 :ASDF3 :ASDF2 :ASDF :OS-MACOSX :OS-UNIX
 :NON-BASE-CHARS-EXIST-P :ASDF-UNICODE :64-BIT :64-BIT-REGISTERS
 :ALIEN-CALLBACKS :ANSI-CL :ASH-RIGHT-VOPS :BSD :C-STACK-IS-CONTROL-STACK
 :COMMON-LISP :COMPACT-INSTANCE-HEADER :COMPARE-AND-SWAP-VOPS
 :COMPLEX-FLOAT-VOPS :CYCLE-COUNTER :DARWIN :DARWIN9-OR-BETTER :FLOAT-EQL-VOPS
 :FP-AND-PC-STANDARD-SAVE :GENCGC :IEEE-FLOATING-POINT :IMMOBILE-CODE
 :IMMOBILE-SPACE :INLINE-CONSTANTS :INODE64 :INTEGER-EQL-VOP :LINKAGE-TABLE
 :LITTLE-ENDIAN :MACH-EXCEPTION-HANDLER :MACH-O :MEMORY-BARRIER-VOPS
 :MULTIPLY-HIGH-VOPS :OS-PROVIDES-BLKSIZE-T :OS-PROVIDES-DLADDR
 :OS-PROVIDES-DLOPEN :OS-PROVIDES-PUTWC :OS-PROVIDES-SUSECONDS-T
 :PACKAGE-LOCAL-NICKNAMES :PRECISE-ARG-COUNT-ERROR :RAW-INSTANCE-INIT-VOPS
 :RAW-SIGNED-WORD :SB-DOC :SB-EVAL :SB-LDB :SB-PACKAGE-LOCKS :SB-SIMD-PACK
 :SB-SOURCE-LOCATIONS :SB-TEST :SB-THREAD :SB-UNICODE :SBCL
 :STACK-ALLOCATABLE-CLOSURES :STACK-ALLOCATABLE-FIXED-OBJECTS
 :STACK-ALLOCATABLE-LISTS :STACK-ALLOCATABLE-VECTORS
 :STACK-GROWS-DOWNWARD-NOT-UPWARD :SYMBOL-INFO-VOPS :UD2-BREAKPOINTS
 :UNBIND-N-VOP :UNIX :UNWIND-TO-FRAME-AND-CALL-VOP :X86-64)
CL-USER>

Revision history for this message
Douglas Katzman (dougk) wrote :

I may or may not reply to that group discussion, but I will say that to my reading, the spec nowhere claims that AND specifiers treat terms appearing earlier as guard conditions on terms to their right.

The simplification that we're making is that (MEMBER 1 2 3) *implies* INTEGERP.

Therefore we needn't test both. So it's actually the INTEGER term that drops out, and what remains is (AND (SATISFIES EVENP) (MEMBER 1 2 3))

While it's true that writing terms in a certain order could "fix" this error checking issue, we only make a best effort to preserve order of terms in the first place.

It is generally understood - in my belief anyway - that SATISFIES predicates must be written to accept any object. The example of (AND INTEGER (SATISFIES EVENP)) is foolish.

Changed in sbcl:
status: New → Won't Fix
To post a comment you must log in.
This report contains Public information  
Everyone can see this information.

Other bug subscribers

Remote bug watches

Bug watches keep track of this bug in other bug trackers.