On y va: une réponse partielle/solution à ma question (pourquoi partiel? Voir ci-dessous). Merci à SD pour m'avoir aidé à comprendre cela! Permettez-moi de commencer par clarifier. Lorsque j'ai posé ma question initialement, j'ai utilisé le terme «type paramétrique» de manière imprécise, n'ayant qu'une définition vague comme «un type de paramètre dépendant». Je essentiellement voulais un gadget me permettant d'écrire le pseudo-code suivant (dans un pseudo-langue):
class List<T> {
//implementation
};
l = new List<string>;
l.push("Hello World!");
Donner un sens du pseudo-code ci-dessus est assez straight-forward (voir la réponse de sds). Cependant, l'ambiguïté se pose si l'on commence à se demander si les expressions List<T> et List devraient avoir une signification. En effet, en C++ par exemple, les expressions seraient non définies, l'effet de la définition du modèle
template <typename T>
class List {
public:
T car;
List<T> *cdr;
};
est comme définissant séparément, pour chaque type T, un type List<T>. En revanche, dans des langages comme Java qui implémentent types génériques, l'expression List<T> (où T est une variable libre) est logique et désigne un type, à savoir le type générique d'une liste sur un certain typeT, de sorte que l'on pouvait par exemple écrire une fonction polymorphes comme
T car(List<T> l) {
return l.car;
}
En bref, en C++, nous avons seulement la collection (infinie) de tous les types List<T> où T fonctionne sur tous les types, alors que dans Java cette collection elle-même existe comme un objet dans la langue, comme le type générique List<T>.
Maintenant à ma solution partielle proposée, dont je vais esquisser brièvement les mots avant d'écrire le code Lisp réel. La solution est basée sur familles de types et la somme dépendante de telles familles, à savoir nous allons interpréter un type paramétrique comme le type List<T> ci-dessus en tant que fonction List d'un argument dont les valeurs sont des types, et nous feignons le Java type générique de style List<T> comme type de somme dépendant DepSum(List), qui se compose simplement de paires (a,b) où a est un certain type et b est de type List(b).
Revenant à l'exemple de définir un véritable espace vectoriel sur un ensemble X, je voudrais écrire quelque chose comme
(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)))
déterminant pour moi une RealVectorSpaceOver de fonction qui, étant donné une classe A, renverrait une classe comme si elle est définie manuellement par
(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)))
Fondamentalement, je pourrais copier-coller-n la solution de sds ici, mais il y a deux problèmes. Tout d'abord, le résultat ne serait pas une fonction (effet secondaire sans), par exemple la forme
(typep (make-instance (RealVectorSpaceOver A)
:add (lambda (x y) nil)
:s-mult (lambda (x y) nil))
(RealVectorSpaceOver A))
évaluerait à nil parce qu'il ya deux appels à RealVectorSpaceOver ici, et chaque appel crée une nouvelle (et donc différent) classe. Ainsi, nous devons envelopper cette fonction dans un code qui met en cache le résultat une fois qu'il a été appelé pour la première fois.
L'autre problème est que l'utilisation de defclass pour créer des classes a pour effet de modifier l'espace de nom de classe, redéfinissant éventuellement les classes existantes. Pour éviter cela, on peut créer de nouvelles classes directement en instanciant la méta-classe standard-class. Par exemple
(make-instance 'standard-class
:name (intern "B")
:direct-superclasses '(A)
:direct-slots '((x :initargs (:x) :readers (x))))
est équivalent à
(defclass B (A)
((x :initarg :x :reader x)))
mais ne redéfinir une classe préexistante B. Notez que le format de l'argument :direct-slots diffère légèrement du format defclass pour la définition des emplacements. En utilisant une fonction d'assistance canonicalize-direct-slot-defs qui transforme ce dernier dans l'ancien (tiré du livre « L'art du Protocole metaObject »), la macro defclassfamily peut être mis en œuvre comme suit:
(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)))))
Le code ci-dessus d'abord définit une fonction f représentant la famille de types souhaitée, puis crée une version g en cache en utilisant une fonction d'assistance cache-function (insérez votre propre implémentation), puis définit une nouvelle fonction dans l'espace de nom en utilisant defun, en appliquant les types pour les arguments (defclassfamily accepte arguments typés similaires à defmethod, de sorte que (defclassfamily F ((X Set) Y) ... définirait une famille F de t wo paramètres, avec le premier étant de type Set) et la valeur de retour de la famille de classe. De plus, il existe une fonction d'assistance simple strip-variables, types-of-variables, et type-decls-from-variables qui transforme l'expression en fonction des variables de la famille de type ((X Set) Y dans l'exemple précédent). Ils sont définis comme suit:
(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))
Enfin, nous enregistrons les types des arguments tirés par notre famille en utilisant une méthode argument-signature, de sorte que
(argument-signature (defclassfamily F ((X Set) Y) ...))
évaluerait à (Set t).
La somme dépendante d'une famille de type d'un paramètre est mis en œuvre par le code suivant:
(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)))
afin que nous puissions définir un type RealVectorSpace utilisant
(let ((rvs-type (depsum #'RealVectorSpaceOver)))
(deftype RealVectorSpace()
rvs-type))
et écrire
(make-instance (depsum #'RealVectorSpaceOver) :pr1 X :pr2 some-rvs-over-X)
pour créer un objet de type RealVectorSpace. Le code ci-dessus fonctionne en créant une méta-classe (c'est-à-dire la sous-classe standard-class) DepSum, qui représente le type de toutes les sommes dépendantes et dont les instances sont des sommes dépendantes de familles spécifiques. La sécurité de type est renforcée par l'accrochage dans les appels comme (make-instance (depsum #'RealVectorSpaceOver) ...) via (defmethod make-instance :before ((sum-class DepSum .... Malheureusement, il semble que nous devons compter sur assert pour ce type de vérification (je n'étais pas en mesure de comprendre comment le faire fonctionner avec declare). Enfin, le code (defmethod sb-mop:validate-superclass ... est dépendant de l'implémentation (pour SBCL dans ce cas) et nécessaire pour pouvoir instancier des instances de DepSum comme (depsum #'RealVectorSpaceOver).
Pourquoi est-ce seulement une réponse partielle? Parce que je n'ai pas fait les axiomes de l'espace vectoriel du type de RealVectorSpaceOver (ou RealVectorSpace). En effet, une telle chose nécessiterait de donner une preuve réelle de ces axiomes en tant que partie de la donnée dans un appel à (make-instance (RealVectorSpaceOver X) .... Une telle chose est certainement possible dans des langages fantaisistes comme Coq, mais semble totalement hors de portée dans ce vieux désordre qui est Common Lisp.
Puisque Common Lisp n'a aucun système de type utile pour cela et en particulier les types dépendants, cela n'a pas beaucoup de sens. Je propose d'utiliser un langage de programmation avec un système de type élaboré comme Haskell ou quelque chose comme Axiom (http://fricas.github.io/api/VectorSpaceBasis.html). –
Bien sûr, Common Lisp n'a pas de système de type utile. Mais la question est: que signifie "a"? Par exemple, même sans CLOS, vous pouvez facilement créer votre propre OO à l'aide de fermetures lexicales. – BlenderBender
si vous avez une question spécifique, mieux avec le code, puis demander. Sinon, je crains qu'une large question spéculative ne convienne pas à Stackoverflow, qui se concentre sur de vrais problèmes de programmation pratique. –