Зависимые типы/Параметрический полиморфизм в 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 (sic), который оценивает что-то типа V.

Конечно, этот тип не был бы точным отражением концепции вещественное векторное пространство, потому что vector-add и scalar-mult все равно должны будут удовлетворять некоторым дополнительным свойствам. Но даже превращение этой мечты в реальный код ускользает от меня.

Edit: В ответ на ответ ИКБ, позвольте мне выдвинуть следующее разъяснение моего первоначального вопроса: в двух словах, то, кажется, мне нужно иметь зависимые типы в Лиспе, который отличается от вопроса только для параметрических классов. Фактически, Haskell имеет параметрические типы, но не имеет (по крайней мере, не встроенного явным образом) зависимых типов. Например, недостаток зависимых типов в Haskell обсуждается here.

1. Может ли кто-нибудь помочь мне превратить мою мечту в код?

2. Я где-то слышал, что вам не нужны параметрические классы в Lisp из-за макросов Lisp. Если это правда, может кто-нибудь объяснить, как вы будете использовать defmacro для реализации/поддельных параметрических классов в Common Lisp?

Answer 1

Здесь мы идем: частичный ответ/решение моего вопроса (почему частичное? См. Ниже). Большое спасибо sds за то, что помогли мне понять это!

Позвольте мне начать разъяснение. Когда я задал свой вопрос изначально, я использовал термин «параметрический тип» неточно, имея в виду лишь неопределенное определение как «зависящие от типа параметры». Я в основном хотел немного гаджет позволяет мне написать следующий псевдокод (в псевдо-языке):

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

Осмысления вышеприведенного псевдокода является довольно прямо вперед (см ответа ИКБА). Однако возникает двусмысленность, если вы начинаете задумываться о том, должны ли значения выражения 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))) 

в принципе, я мог бы скопировать-н-паста решение ИКБ здесь, но есть две проблемы. Прежде всего, результат не будет функцией (побочный эффект бесплатно), например, форма

(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, представляющий семейство желаемого типа, затем создает кэшированную версию g с помощью вспомогательной функции cache-function (вставьте свою собственную реализацию), а затем определяет новую функцию в пространстве имен с помощью defun, применяя типы аргументов (defclassfamily принимает набранные аргументы, подобные defmethod, так что (defclassfamily F ((X Set) Y) ... определит семейство F of t wo, причем первый из них имеет тип 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, который представляет тип всех зависимых сумм и экземпляры которых зависят от сумм конкретных семейств. Тип безопасности обеспечивается путем подключения к вызовам типа (make-instance (depsum #'RealVectorSpaceOver) ...) через (defmethod make-instance :before ((sum-class DepSum .... К сожалению, нам кажется, что мы должны полагаться на assert для проверки этого типа (я не смог выяснить, как заставить его работать с declare). Наконец, код (defmethod sb-mop:validate-superclass ... зависит от реализации (для SBCL в этом случае) и необходим для создания экземпляров DepSum, таких как (depsum #'RealVectorSpaceOver).

Почему это только частичный ответ? Потому что я не сделал аксиомы векторного пространства частью типа RealVectorSpaceOver (или RealVectorSpace). Действительно, такая вещь потребует, чтобы дать реальное доказательство этих аксиом как часть опорной точки в вызове (make-instance (RealVectorSpaceOver X) .... Такая вещь, безусловно, возможна в таких причудливых языках, как Coq, но кажется совершенно недосягаемой в этом старом, но привлекательном беспорядке, который является Common Lisp.

Answer 2

Я сомневаюсь, что вы хотите, имеет много смысла, , но как пример макроса (аб) использование, здесь вы идете:

(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 является неизменным, из всех слотов одновременно изменяются . Первый вариант может быть выполнен разумным использованием от MOP. Я не уверен, что последнее возможно в Лиспе.

Answer 3

Вы можете прочитать о LIL, Lisp Interface Library с, описанный в LIL: CLOS reaches higher-order, sheds identity and has a transformative experience из FARE Ридо. github page имеет более подробную информацию.

В принципе, LIL пытается выразить параметрический полиморфизм с помощью дополнительного параметра (интерфейс , который похож на класс типа), который может быть сделан неявным благодаря динамическому охвату.

С другой стороны, то, что вы хотите выразить, действительно легко сделать с OCaml-модулями, поэтому в зависимости от ваших потребностей вы можете лучше следовать совету Райнера Йосвига (используйте другой язык).

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 

Что касается свойств (в соответствии с просьбой в комментариях), вам, возможно, придется использовать более сложный тип системы (Кок?). Примером того, как Common Lisp может абстрагироваться над вещами, является Gábor Melis's MGL-CUBE.