Shouldn't 'and' type specifier short circuit?

Question

Working on some more complicated example with type specifiers in common lisp, I've run into the strange behavior of and + satisfies, namely it doesn't seem to short circuit in case of first typecheck failure, moving on to second. Sometimes it also calls the satisfies pred twice. Here is the simplified example:

(defun check-len (x)
  (let ((res (> (length x) 1)))
    (format t "check len: ~a : ~a~%" x res)
    res))

(typep #(1 2 3) '(and
                  list
                  (satisfies check-len)))

;;=> check len: #(1 2 3) : T
;;=> check len: #(1 2 3) : T
;; NIL

(declaim (ftype (function ((and list (satisfies check-len))))
                some-fn)) 
(defun some-fn (x) x)

(some-fn #(1 2 3))
;;=> check len: #(1 2 3) : T
;;=> check len: #(1 2 3) : T
; Debugger entered on #<TYPE-ERROR expected-type:
;              (OR (AND (SATISFIES CHECK-LEN) CONS) (AND (SATISFIES CHECK-LEN) NULL))
; 
;              datum: #<(SIMPLE-VECTOR 3) {100464796F}>>

Cannot find any specific mention of the ordering for and, though intuitively it doesn't seem correct.

What is the reason for this behavior? Is there any specification? How can one ensure that multiple checks are executed in order? (to avoid raising condition in the check like this: (typep 1 '(and list (satisfies check-len))) where I would expect the list check to resolve to nil without even moving to check-len)

I'm on sbcl 2.1.10, manjaro linux, x86-64 (Intel)

Mackintosh

Since no ordering is specified, it can be implemented in any order. Other than the name, there's no relationship with the AND macro. – Tropous

Except for SATISFIES, order of checking type specifiers makes no difference (except for performance). – Tropous

Answer 1

How the type is checked is implementation defined.

The output tells you that your implementation transformed the type expression by expanding list to (or cons null) and then bringing the entire expression into disjunctive normal form, which contains the satisfies check in two places.

It is hard to find a general rule how to most efficiently check a type expression, so I guess using a normal form makes it at least a bit predictable, and also better allows combining and comparing types, e. g. when building dispatch trees.

Redouble