Is it possible to define a recursive type in Common Lisp?

Question

A recursive type is a type which has a base and a recursive case of itself.

I wanted this to implement "typed lists", i.e., lists whose conses only allow the same element type or nil.

I tried the following definition:

(deftype list-of (a) `(or null
                          (cons ,a (list-of ,a))))

However, this signals an stack exausted problem (at least on SBCL) due to the compiler trying to recurse over list-of indefinitely. Is it possible to define such a data type?

Hashimoto

Answer 1

It's not possible. The types you define with DEFTYPE are "derived types". The derived type is expanded (like a macro) into a "real" type specifier, which can't contain derived types. All references to derived types (either the type itself or others) inside the expansion are also expanded. Thus the recursive type will go into an infite loop to try and expand.

Trivial Types provides a type for proper-lists, but that doesn't actually check the element types despite taking it as an argument. For cosmetic reasons that would be sufficient.

(ql:quickload :trivial-types)
(use-package :trivial-types)
(typep '("qwe" "asd" "zxc") '(proper-list string)) ;=> T
(typep '("qwe" "asd" "zxc" 12) '(proper-list string)) ;=> T

Otherwise, you could define a type that checks if the first couple elements are correct type. That would at least catch the most obvious violations.

(deftype list-of (a)
  `(or null (cons ,a (or null (cons ,a (or null (cons ,a list)))))))
(typep '("asd") '(list-of string)) ;=> T
(typep '("asd" 12) '(list-of string)) ;=> NIL
(typep '("asd" "qwe") '(list-of string)) ;=> T
(typep '("asd" "qwe" 12) '(list-of string)) ;=> NIL
(typep '("asd" "qwe" "zxc") '(list-of string)) ;=> T
(typep '("asd" "qwe" "zxc" 12) '(list-of string)) ;=> T

If you want it to work for lists of any length, you'll have to define a type for each different list you need.

(defun list-of-strings-p (list)
  (every #'stringp list))
(deftype list-of-strings ()
  `(or null (satisfies list-of-strings-p)))
(typep '("qwe" "asd" "zxc" "rty" "fgh") 'list-of-strings) ;=> T
(typep '("qwe" "asd" "zxc" "rty" "fgh" 12) 'list-of-strings) ;=> NIL

Marjoriemarjory

It doesn't seem too useful to set types for cosmetic reasons. For cosmetic reasons I can always (deftype whatever (a) t), can't I? – Hashimoto

@Hashimoto Using (proper-list string) does check that the list is a proper-list, and it tells people reading the code that you expect it to contain strings. Obviously your code can't rely on it really containing strings, but if it's not critical then that's better than nothing. – Marjoriemarjory

Alright, it's a compromise. So it's "good" for self-documenting code and telling straightforward mistakes, without deepening into the math behind HM types. – Hashimoto

Answer 2

Yes, but I cheated ;)

(defun satisfication (a)
  (if a
      (and (integerp (car a))
       (satisfication (cdr a)))
      T))

(deftype my-list () `(satisfies satisfication))


(typep (cons 1 (cons 2 (cons 3 nil))) 'my-list)
> T


(typep (cons 1 (cons 2 (cons 3.2 nil))) 'my-list)
> NIL

Apparently SBCL doesn't like recursive types - the reason is well explained by another answer. But if you want to stick with the standard and still define recursive types there is a light at the end of the tunnel: you may define any function to check satisfaction.

Gazetteer

You might use (every #'integerp list). You could also handle the type in a generic way and use a loop: (loop for e in list always (typep e type)) – Roseberry

Of course, it's "easy enough" to write a function to check it with monomorphic types, but the ploymorphic problem is much more interesting. – Hashimoto

I think the most relevant caveat with polymorphic types is that you can no longer define a satisfies function taking only one parameter. – Hashimoto

@Hashimoto you could define a my-deftype-macro doing that – Gazetteer

@Roseberry usually you use such recursive definitions for proofs (the only advantage of such definition I actually see). Using loop or every would defy that purpose if you do not assume correctness of them. But besides that your approach is shorter and clearer. – Gazetteer

@Gazetteer Defining a new macro for DEFTYPE wouldn't really help since it's the type checking that doesn't support recursive derived types. You could write your own run-time type checking system, but I don't think you can get that to work with declarations, or to do any static type checking or optimizing at compile-time. – Marjoriemarjory

@Marjoriemarjory I think Sim says that you can flatten a polymorphic type into all its monomorphic instances in use, i.e., generating the satisfication functions for each monomorphic type. But that does not grant true polymorphism, which is how far lisp macros can go. – Hashimoto