Зависимые типы / Параметрический полиморфизм в Common Lisp?
Я хочу написать некоторый общий код, имеющий дело с группами отражений, и поэтому мне нужно настроить некоторые типы, которые отражают математические структуры (векторное пространство, аффинное пространство,...). Поскольку я действительно хочу точно отражать эти структуры в типах, мне нужен способ определить некоторый параметрический тип.
Так что, в частности, я хотел бы иметь возможность написать следующий код
(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 может быть чем угодно, а вектор-сложение является функцией, принимающей два параметра типа V (sic), которая оценивает что-то типа V,
Конечно, этот тип не будет достаточно точным отражением концепции реального векторного пространства, потому что vector-add и scalar-mult все равно должны будут удовлетворять некоторым дополнительным свойствам. Но даже превращение этого "сна" выше в настоящий код ускользает от меня.
Изменить: В ответ на ответ sds, позвольте мне предложить следующее разъяснение моего первоначального вопроса: в двух словах, мне кажется, мне нужны зависимые типы в Лиспе, который отличается от запроса только для параметрических классов. Фактически, Haskell имеет параметрические типы, но не имеет (по крайней мере, не встроенным очевидным образом) зависимых типов. Отсутствие зависимых типов в Haskell, например, обсуждается здесь.
1. Может ли кто-нибудь помочь мне превратить мою мечту в код?
2. Я где-то слышал, что вам не нужны параметрические классы в Lisp из-за макросов Lisp. Если это правда, может кто-нибудь объяснить, как бы вы использовали defmacro для реализации / подделки параметрических классов в Common Lisp?
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>,
Теперь к моему предложенному частичному решению, которое я кратко нарисую словами, прежде чем писать настоящий код на Лиспе. Решение основано на семействах типов и зависимой сумме таких семейств, т.е. мы собираемся интерпретировать параметрический тип как тип 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)))
В принципе, я мог бы скопировать-n-вставить решение 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 представляет желаемое семейство типов, затем создает cached-версию g об этом с помощью вспомогательной функции cache-function (вставьте свою собственную реализацию), а затем определите новую функцию в пространстве имен, используя 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, который представляет тип всех зависимых сумм и экземпляры которых являются зависимыми суммами определенных семейств. Безопасность типов обеспечивается подключением к таким вызовам, как (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.
Я сомневаюсь, что то, что вы хотите, имеет большой смысл, но в качестве примера использования макроса (ab), здесь вы идете:
(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. Я не уверен, возможно ли последнее в Лиспе.
Вы можете прочитать о LIL, Библиотеке интерфейса Lisp, описанной в LIL: CLOS достигает высшего порядка, отбрасывает идентичность и имеет опыт преобразования от Фаре Ридо. Страница GitHub имеет больше деталей.
По сути, 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
Что касается свойств (как требуется в комментариях), вам может потребоваться использовать более сложную систему типов (Coq?). Примером того, как Common Lisp может хорошо абстрагироваться, является MGL-CUBE Габора Мелиса.