'and'类型说明符不应该短路吗？答案

【问题标题】：Shouldn't 'and' type specifier short circuit?'and'类型说明符不应该短路吗？
【发布时间】：2021-12-17 08:39:13
【问题描述】：

处理一些更复杂的例子，在普通 lisp 中使用类型说明符，我遇到了 and + satisfies 的奇怪行为，即在第一次类型检查失败的情况下它似乎不会短路，移动到第二个。有时它还会调用satisfies pred 两次。这是简化的示例：

(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}>>

找不到任何关于and 排序的具体说明，但直觉上它似乎不正确。

这种行为的原因是什么？有规范吗？如何确保按顺序执行多项检查？（为了避免像这样在支票中引发条件：(typep 1 '(and list (satisfies check-len))) 我希望list 支票可以解析为nil，甚至无需移动到check-len）

我使用的是 sbcl 2.1.10、manjaro linux、x86-64（英特尔）

【问题讨论】：

由于没有指定顺序，所以可以任意顺序实现。除了名称之外，与AND 宏没有任何关系。
除了SATISFIES，检查类型说明符的顺序没有区别（性能除外）。

标签： types common-lisp

【解决方案1】：

如何检查类型由实现定义。

输出告诉您，您的实现通过将list 扩展为(or cons null)，然后将整个表达式转换为析取范式，其中在两个位置包含satisfies 检查来转换类型表达式。

很难找到一个如何最有效地检查类型表达式的一般规则，所以我猜使用标准形式至少可以使其具有一定的可预测性，并且还可以更好地组合和比较类型, 即G。在构建调度树时。

【讨论】：