是否可以在Common Lisp中定义递归类型?

ssi*_*ice 5 types type-theory common-lisp

递归类型是一种具有基础和自身递归情况的类型.

我希望这能够实现"类型列表",即其conses仅允许相同元素类型或nil的列表.

我尝试了以下定义:

(deftype list-of (a) `(or null
                          (cons ,a (list-of ,a))))
Run Code Online (Sandbox Code Playgroud)

然而,由于编译器试图无限期地在列表上进行递归,这标志着堆栈耗尽问题(至少在SBCL上).是否可以定义这样的数据类型?

Sim*_*Sim 5

是的,但我作弊了 ;)

(defun satisfication (a)
  (if a
      (and (integerp (car a))
       (satisfication (cdr a)))
      T))

(deftype my-list () `(satisfies satisfication))


(typep (cons 1 (cons 2 (cons 3 nil))) 'my-list)
> T


(typep (cons 1 (cons 2 (cons 3.2 nil))) 'my-list)
> NIL
Run Code Online (Sandbox Code Playgroud)

显然 SBCL 不喜欢递归类型 - 另一个答案很好地解释了原因。但是,如果您想坚持标准并仍然定义递归类型,那么隧道尽头有一个亮点:您可以定义任何函数来检查满意度。

  • 您可以使用`(每个#'整数列表)`。您还可以以通用方式处理类型并使用循环:`(loop for e in list always (typep e type))` (2认同)

jki*_*ski 5

这是不可能的.您定义的类型DEFTYPE是"派生类型".派生类型被扩展(如宏)到"真实"类型说明符,它不能包含派生类型.扩展中对派生类型(类型本身或其他类型)的所有引用也都会扩展.因此,递归类型将进入infite循环以尝试和扩展.

Trivial Types为正确列表提供了一种类型,但实际上并没有将它作为参数检查元素类型.出于美观的原因,这就足够了.

(ql:quickload :trivial-types)
(use-package :trivial-types)
(typep '("qwe" "asd" "zxc") '(proper-list string)) ;=> T
(typep '("qwe" "asd" "zxc" 12) '(proper-list string)) ;=> T
Run Code Online (Sandbox Code Playgroud)

否则,您可以定义一种类型,以检查前几个元素是否是正确的类型.这至少会抓住最明显的违规行为.

(deftype list-of (a)
  `(or null (cons ,a (or null (cons ,a (or null (cons ,a list)))))))
(typep '("asd") '(list-of string)) ;=> T
(typep '("asd" 12) '(list-of string)) ;=> NIL
(typep '("asd" "qwe") '(list-of string)) ;=> T
(typep '("asd" "qwe" 12) '(list-of string)) ;=> NIL
(typep '("asd" "qwe" "zxc") '(list-of string)) ;=> T
(typep '("asd" "qwe" "zxc" 12) '(list-of string)) ;=> T
Run Code Online (Sandbox Code Playgroud)

如果您希望它适用于任何长度的列表,则必须为您需要的每个不同列表定义类型.

(defun list-of-strings-p (list)
  (every #'stringp list))
(deftype list-of-strings ()
  `(or null (satisfies list-of-strings-p)))
(typep '("qwe" "asd" "zxc" "rty" "fgh") 'list-of-strings) ;=> T
(typep '("qwe" "asd" "zxc" "rty" "fgh" 12) 'list-of-strings) ;=> NIL
Run Code Online (Sandbox Code Playgroud)