Dependent types/Parametric polymorphism in Common Lisp?

Question

I want to write some generic code dealing with reflection groups, and therefore need to set up some types which reflect mathematical structures (vector space, affine space, ...). As I really want to reflect those structures faithfully in types, I need a way to define some kind of parametric type.

So in particular, I'd want to be able to write the following code

(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)))

which should specify a new type RealVectorSpace which would be given by a triple (V vector-add scalar) where V can be anything, and vector-add is a function taking two parameters of type V (sic) that evaluates to something of type V.

Of course, this type wouldn't be quite a faithful reflection of the concept of a real vector space, because vector-add and scalar-mult would still need to satisfy some further properties. But even turning that 'dream' above into real code eludes me.

Edit: In response to sds's answer, let me put forward the following clarification of my original question: in a nutshell, it seems I need to have dependent types in Lisp, which is different from asking just for parametric classes. In fact, Haskell has parametric types but does not have (at least it's not built-in in an obvious way) dependent types. The lack of dependent types in Haskell is for instance discussed here.

1. Can anyone help me turn my dream into code?

2. I've heard somewhere that you don't need parametric classes in Lisp because of Lisp macros. If that's true, can someone explain how you'd use defmacro to implement/fake parametric classes in Common Lisp?

Answer 1

Here we go: a partial answer/solution to my question (why partial? see below). Many thanks to sds for helping me figure this out!

Let me begin by making a clarification. When I posed my question initially, I used the term 'parametric type' imprecisely, having only a vague definition as 'a type depending parameters' in mind. I basically wanted some gadget allowing me to write the following pseudo-code (in a pseudo-language):

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

Making sense of the above pseudo-code is pretty straight-forward (see sds's answer). However, ambiguity arises if one starts to wonder whether the expressions List<T> and List themselves should have a meaning. Indeed, in C++ for example, the expressions would be undefined, for the effect of the template definition

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

is as if defining separately, for each type T, a type List<T>. In contrast, in languages like Java that implement generic types, the expression List<T> (where T is a free variable) makes sense and denotes a type, namely the generic type of a list over some type T, so that one could e.g. write a polymorphic function like

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

In short, in C++ we only have the (infinite) collection of all types List<T> where T runs over all types, whereas in Java this collection itself exists as an object in the language, as the generic type List<T>.

Now to my proposed partial solution, which I will briefly sketch in words before writing the actual Lisp code. The solution is based on type families and the dependent sum of such families, i.e. we are going to interpret a parametric type like the type List<T> above as a function List of one argument whose values are types, and we fake the Java-style generic type List<T> as the dependent sum type DepSum(List), which simply consists of pairs (a,b) where a is some type and b is of type List(b).

Returning to the example of defining a real vector space over a set X, I would like to write something like

(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)))

defining for me a function RealVectorSpaceOver that, given a class A, would return a class as if defined manually by

(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)))

Basically, I could copy-n-paste the solution of sds here, but there are two problems with this. First of all, the result would not be a (side-effect-free) function, for example the form

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

would evaluate to nil because there are two calls to RealVectorSpaceOver here, and each call creates a new (and therefore different) class. Thus, we need to wrap this function in some code that caches the result once it has been called for the first time.

The other problem is that using defclass to create classes programmatically has the effect of changing the class name space, possibly redefining existing classes. To avoid this, one can instead create new classes directly by instantiating the meta class standard-class. For example

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

is equivalent to

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

but wouldn't redefine any pre-existing class B. Note that the format for the :direct-slots argument differs slightly from the defclass format for defining slots. Using a helper function canonicalize-direct-slot-defs that transforms the latter into the former (taken from the book 'The Art of the Metaobject Protocol'), the macro defclassfamily can be implemented as follows:

(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)))))

The above code first defines a function f representing the desired type family, then creates a cached-version g of it using a helper function cache-function (insert your own implementation), and then defines a new function in the name space using defun, enforcing the types for the arguments (defclassfamily accepts typed arguments similar to defmethod, so that (defclassfamily F ((X Set) Y) ... would define a family F of two parameters, with the first one being of type Set) and the return value of the class family. Moreover, there are some simple helper function strip-variables, types-of-variables, and type-decls-from-variables that transform the expression given the variables of the type family ((X Set) Y in the previous example). They are defined as follows:

(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))

Finally, we record the types of the arguments taken by our family using a method argument-signature, so that

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

would evaluate to (Set t).

The dependent sum of a type family of one parameter is implemented by the following code:

(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)))

so that we could define a type RealVectorSpace using

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

and write

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

to create an object of type RealVectorSpace. The above code works by creating a meta-class (i.e. subclass of standard-class) DepSum, which represents the type of all dependent sums and whose instances are dependent sums of specific families. Type safety is enforced by hooking into calls like (make-instance (depsum #'RealVectorSpaceOver) ...) via (defmethod make-instance :before ((sum-class DepSum .... Unfortunately, it seems we have to rely on assert for this type check (I wasn't able to figure out how to make it work with declare). Lastly, the code (defmethod sb-mop:validate-superclass ... is implementation-dependent (for SBCL in this case) and necessary in order to be able to instantiate instances of DepSum like (depsum #'RealVectorSpaceOver).

Why is this only a partial answer? Because I have not made the vector space axioms part of the type of RealVectorSpaceOver (or RealVectorSpace). Indeed, such a thing would require to give an actual proof of these axioms as part of the datum in a call to (make-instance (RealVectorSpaceOver X) .... Such a thing is certainly possible in fancy languages like Coq, but seems totally out-of-reach in that old, yet lovable mess that is Common Lisp.

Answer 2

I doubt that what you want makes much sense, but as an example of macro (ab)use, here you go:

(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)

Responding to the comment:

If you want a single real-vector-space class, you are, essentially, asking for the vector-add and scalar-mult slots to have type which depends on the value of the V slot.
This would imply that (setf (underlying-set rvs) some-new-type) would have to check that (add rvs) and (s-mult rvs) have to appropriate type for some-new-type. Essentially, this means that either every object of type real-vector-space is immutable, of all slots are modified simultaneously. The former option can be accomplished by a judicious use of MOP. I am not sure if the latter is possible in Lisp.

Answer 3

You can read about LIL, the Lisp Interface Library, described in LIL: CLOS reaches higher-order, sheds identity and has a transformative experience from Faré Rideau. The github page has more details.

Basically, LIL tries to express parametric polymorphism through an additional parameter (the interface, which is like a type class) that can be made implicit thanks to dynamic scoping.

On the other hand, what you want to express is really easy to do with OCaml modules, so depending on your needs you may better follow Rainer Joswig's advice (use another language).

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

As for properties (as requested in comments), you might need to use a more complex type system (Coq?). An example of how Common Lisp can abstract over things nicely is Gábor Melis's MGL-CUBE.