Common Lisp 中的依赖类型/参数多态性

Question

我想编写一些处理反射组的通用代码，因此需要设置一些反映数学结构的类型(向量空间，仿射空间，...)。由于我真的想在类型中忠实地反映这些结构，因此我需要一种方法来定义某种参数类型。

所以特别是，我希望能够编写以下代码

(defclass RealVectorSpace ()
((V :accessor underlying-set
:type Set)
(vector-add :accessor add
:type (function ((set-as-type V) (set-as-type V)) (set-as-type V)))
(scalar-mult :accessor s-mult
:type (function (real (set-as-type V)) (set-as-type V)))

它应该指定一个新的类型RealVectorSpace，它将由三重(V向量添加标量)给出，其中V可以是任何东西，而vector-add是一个函数，采用两个类型V(原文如此)的参数，计算结果为V类型的东西。

当然，这种类型并不能忠实地反映真实向量空间的概念，因为向量加法和标量多点仍然需要满足一些进一步的属性。但是，即使将上面的"梦想"变成真正的代码，我也难以理解。

编辑：为了回应sds的回答，让我对我最初的问题提出以下澄清：简而言之，似乎我需要在Lisp中使用依赖类型，这与仅要求参数化类不同。事实上，Haskell有参数化类型，但没有(至少它没有以明显的方式内置)依赖类型。例如，这里讨论了Haskell中缺少依赖类型的问题。

1. 谁能帮我把我的梦想变成代码？

2. 我在某处听说，由于 Lisp 宏，您在 Lisp 中不需要参数化类。如果这是真的，有人可以解释一下你如何使用defmacro在Common Lisp中实现/伪造参数类吗？

Answer 1

我怀疑你想要的有多大意义， 但作为宏(滥用)使用的示例，您可以：

(defmacro define-real-vector-space (type &optional name)
`(defclass ,(or name (intern (format nil "REAL-VECTOR-SPACE-~A" type))) ()
((V :reader underlying-set :initform ',type)
(vector-add :accessor add
:type (function ((x ,type) (y ,type)) => ,type))
(scalar-mult :accessor s-mult
:type (function ((x real) (v ,type) => ,type))))))
;; sample underlying set:
(deftype 3d () (array real (3)))
;; use it:
(macroexpand-1 '(define-real-vector-space 3d))
==>
(DEFCLASS REAL-VECTOR-SPACE-3D NIL
((V :READER UNDERLYING-SET :INITFORM '|3D|)
(VECTOR-ADD :ACCESSOR ADD :TYPE (FUNCTION ((X |3D|) (Y |3D|)) => |3D|))
(SCALAR-MULT :ACCESSOR S-MULT :TYPE #'((X REAL) (V |3D|) => |3D|))))
(define-real-vector-space 3d)

回应评论：

如果你想要一个单一的real-vector-space类，你基本上是， 要求vector-add和scalar-mult插槽具有类型 取决于V槽的值。
这意味着(setf (underlying-set rvs) some-new-type)必须检查(add rvs)和(s-mult rvs)必须适当 键入some-new-type。 从本质上讲，这意味着每个类型的对象real-vector-space是不可变的，所有插槽都被修改 同时。 前一种选择可以通过明智地使用 的澳门币。 我不确定后者在 Lisp 中是否可行。

Answer 2

你可以阅读LIL的信息，Lisp接口库，在LIL中描述：CLOS达到更高阶，摆脱身份 并拥有法雷·里多的变革性经验。github页面包含更多详细信息。

基本上，LIL 尝试通过附加参数(接口，类似于类型类)来表达参数多态性，该参数可以通过动态作用域隐式进行

。另一方面，你想表达的东西用OCaml模块真的很容易做到，所以根据你的需求，你最好遵循Rainer Joswig的建议(使用另一种语言)。

module type VectorSpace =
functor (S : sig val dimension : int end)
(F : sig type scalar val zero : scalar end) ->
sig
type vector = F.scalar array
val add : vector -> vector -> vector
val mul : F.scalar -> vector -> vector
end

至于属性(如注释中要求的那样)，您可能需要使用更复杂的类型系统(Coq？ Common Lisp 如何很好地抽象事物的一个例子是 Gábor Melis 的 MGL-CUBE。

Answer 3

我们来了：我的问题的部分答案/解决方案(为什么是部分？见下文)。非常感谢sds帮助我解决这个问题！

我首先要澄清一下。当我最初提出问题时，我不精确地使用了术语"参数类型"，只有一个模糊的定义，即"取决于参数的类型"。我基本上想要一些小工具，允许我编写以下伪代码(用伪语言)：

class List<T> {
//implementation
};
l = new List<string>;
l.push("Hello World!");

理解上面的伪代码非常简单(参见 sds 的答案)。但是，如果人们开始怀疑表达List<T>和List本身是否应该具有含义，就会产生歧义。实际上，例如，在C++中，表达式将是未定义的，因为模板定义的效果

template <typename T>
class List {
public:
T car;
List<T> *cdr;
};

就好像单独定义一样，对于每个类型T，一个类型List<T>。相反，在像Java这样实现泛型类型的语言中，表达式List<T>(其中T是一个自由变量)是有意义的，并表示一种类型，即某种类型T上的列表的泛型类型，因此可以例如编写一个多态函数，例如

T car(List<T> l) {
return l.car;
}

简而言之，在C++中，我们只有所有类型的(无限)集合List<T>其中T运行在所有类型上，而在 Java 中，该集合本身作为语言中的对象存在，作为泛型类型List<T>.

现在谈谈我提出的部分解决方案，在编写实际的 Lisp 代码之前，我将简要地用文字勾勒出它。该解决方案基于类型族和此类族的依赖和，即我们将像上面List<T>的类型这样的参数类型解释为一个值为类型的参数的函数List，并且我们将 Java 风格的泛型类型List<T>伪装为依赖和类型DepSum(List)， 它仅由对组成(a,b)其中a是某种类型，b是List(b)类型。

回到在集合X上定义实向量空间的例子，我想写一些类似的东西

(defclassfamily RealVectorSpaceOver (X) ()
((add :initarg :add
:reader add
:type (function (X X) X))
(s-mult :initarg :s-mult
:reader s-mult
:type (function (real X) X)))

为我定义一个函数RealVectorSpaceOver，给定一个类A，将返回一个类，就像手动定义

一样

(defclass RealVectorSpaceOverA ()
((add :initarg :add
:reader add
:type (function (A A) A))
(s-mult :initarg :s-mult
:reader s-mult
:type (function (real A) A)))

基本上，我可以在此处复制粘贴 sds 的解决方案，但这有两个问题。首先，结果不会是一个(无副作用的)函数，例如形式

(typep (make-instance (RealVectorSpaceOver A)
:add (lambda (x y) nil)
:s-mult (lambda (x y) nil))
(RealVectorSpaceOver A))

将计算为nil，因为此处有两个要RealVectorSpaceOver调用，并且每个调用都会创建一个新的(因此不同的)类。因此，我们需要将此函数包装在一些代码中，这些代码会在第一次调用结果后缓存结果。

另一个问题是，使用defclass以编程方式创建类具有更改类命名空间的效果，可能会重新定义现有类。为了避免这种情况，可以通过实例化元类standard-class来直接创建新类。例如

(make-instance 'standard-class
:name (intern "B")
:direct-superclasses '(A)
:direct-slots '((x :initargs (:x) :readers (x))))

相当于

(defclass B (A)
((x :initarg :x :reader x)))

但不会重新定义任何预先存在的类B.请注意，:direct-slots参数的格式与定义槽的defclass格式略有不同。使用将后者转换为前者的帮助函数canonicalize-direct-slot-defs(取自"元对象协议的艺术"一书)，宏defclassfamily可以按如下方式实现：

(defmacro defclassfamily (name variables superclasses slot-defs)
(let ((stripped-variables (strip-variables variables))
(variable-types (types-of-variables variables))
(type-decls (type-decls-from-variables variables)))
`(flet ((f ,stripped-variables
(make-instance 'standard-class
:name (intern (format nil "~S<~S>" ',name (list ,@stripped-variables)))
:direct-superclasses ,superclasses 
:direct-slots ,(canonicalize-direct-slots slot-defs))))
(let ((g (cache-function #'f)))
(defun ,name ,stripped-variables
,@type-decls
(the standard-class (funcall g ,@stripped-variables)))
(defmethod argument-signature ((x (eql #',name)))
',variable-types)))))

上面的代码首先定义一个表示所需类型系列的函数f，然后使用帮助程序函数cache-function创建它的缓存版本g(插入您自己的实现)，然后使用defun在命名空间中定义一个新函数，强制执行参数的类型(defclassfamily接受类似于defmethod的类型化参数， 这样(defclassfamily F ((X Set) Y) ...将定义一个由两个参数组成的族F，第一个参数的类型为Set)和类族的返回值。此外，还有一些简单的辅助函数strip-variables、types-of-variables和type-decls-from-variables，它们在给定类型族的变量的情况下转换表达式((X Set) Y在上一个例子中)。它们定义如下：

(defun strip-variables (specialized-lambda-list)
(mapcar (lambda (x)
(if (consp x)
(car x)
x))
specialized-lambda-list))
(defun types-of-variables (var-declarations)
(mapcar (lambda (var-declaration) (if (consp var-declaration) (second var-declaration) t)) var-declarations))
(defun type-decls-from-variables (var-declarations)
(mapcar (lambda (var-declaration)
(if (consp var-declaration)
`(declare (type ,(second var-declaration) ,(first var-declaration)))
`(declare (type t ,var-declaration))))
var-declarations))

最后，我们使用方法argument-signature记录我们族采取的参数类型，以便

(argument-signature (defclassfamily F ((X Set) Y) ... ))

将评估为(Set t).

一个参数的类型族的依赖总和由以下代码实现：

(defclass DepSum (standard-class)
((family :initarg :family :reader family)
(arg-type :initarg :arg-type :reader arg-type)))
(defmethod make-instance :before ((sum-class DepSum) &key pr1 pr2)
(assert (and (typep pr1 (arg-type sum-class))
(typep pr2 (funcall (family sum-class) pr1)))))
(defmethod sb-mop:validate-superclass ((class DepSum) (super-class standard-class))
t)
(defun depsum (f)
(let ((arg-type (car (argument-signature f))))
(make-instance 'DepSum
:name (intern (format nil "DepSum_{x:~A} ~A(x)" arg-type f))
:direct-superclasses ()
:direct-slots `((:name pr1 :initargs (:pr1) :readers (pr1) :type ,arg-type)
(:name pr2 :initargs (:pr2) :readers (pr2)))
:direct-slots `((:name pr1 :initargs (:pr1) :readers (pr1)))
:family f
:arg-type arg-type)))

这样我们就RealVectorSpace可以使用

(let ((rvs-type (depsum #'RealVectorSpaceOver)))
(deftype RealVectorSpace ()
rvs-type))

并写入

(make-instance (depsum #'RealVectorSpaceOver) :pr1 X :pr2 some-rvs-over-X)

创建类型为RealVectorSpace的对象。上面的代码通过创建一个元类(即standard-class的子类)DepSum来工作，它表示所有依赖和的类型，其实例是特定族的依赖和。类型安全是通过挂接到调用(如通过(defmethod make-instance :before ((sum-class DepSum ...(make-instance (depsum #'RealVectorSpaceOver) ...))来强制执行的。不幸的是，似乎我们必须依靠assert进行此类型检查(我无法弄清楚如何使其与declare一起使用)。 最后，代码(defmethod sb-mop:validate-superclass ...依赖于实现(在本例中为 SBCL)，并且是能够实例化DepSum实例(如(depsum #'RealVectorSpaceOver))所必需的。

为什么这只是部分答案？因为我还没有使向量空间公理成为RealVectorSpaceOver类型(或RealVectorSpace)的一部分。事实上，这样的事情需要给出这些公理的实际证明，作为(make-instance (RealVectorSpaceOver X) ...调用中基准面的一部分。这样的事情在像Coq这样的花哨语言中当然是可能的，但在Common Lisp这个古老但可爱的混乱中似乎完全遥不可及。