Итак, начнем: частичный ответ/решение на мой вопрос (почему частичный? см. ниже). Большое спасибо 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 — свободная переменная) имеет смысл и обозначает тип, а именно общий тип списка по некоторым< /em> введите T, чтобы можно было, например, написать полиморфную функцию, например
T car(List<T> l) {
return l.car;
}
Короче говоря, в C++ у нас есть только (бесконечная) коллекция всех типов List<T>, где T работает со всеми типами, тогда как в Java эта коллекция сама существует как объект в языке, как общий тип List<T>.
Теперь перейдем к предложенному мной частичному решению, которое я кратко набросаю словами, прежде чем писать фактический код на Лиспе. Решение основано на семействах типов и зависимой сумме таких семейств, т.е. мы собираемся интерпретировать параметрический тип, такой как тип List<T> выше, как функцию List одного аргумента. чьи значения являются типами, и мы подделываем универсальный тип List<T> в стиле Java как зависимый тип суммы 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, представляющую желаемое семейство типов, затем создает ее кэшированную версию 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.
person
BlenderBender
schedule
22.01.2017
