[BoingBoomTschak]

> Some Lisp compilers like SBCL are already capable of more extensive compile-time type-checking, but its information that the programmer is up to supply

Which is nice and all, but very much gimped by the glaring holes in CL's typing tooling: you can't create actual types, only derived types (deftype) and struct/class types. The two consequences of that is that you can't type cons-based lists/trees (arguably THE Lisp data structure) because deftype can't be recursive and you can't create parametric types, it's an internal thing only used for https://www.lispworks.com/documentation/HyperSpec/Body/t_arr... (and not even hash-tables, these are completely untyped!).

[dokyun]

> you can't type cons-based lists/trees (arguably THE Lisp data structure) because deftype can't be recursive and you can't create parametric types

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

  (typep '(1 2 3 4) '(list-of integer))
  => T

Most of the standard types from which derived types can be made are parametric types, which specialize on their arguments in different ways. They work the same way as macros. One upon a time I wrote a type specifier that allows you to specialize on a lambda expression, using the ordinary 'satisfies' type that only lets you provide named functions:

  (deftype satisfiesp (function)
    (let (predicate)
      (cond ((symbolp function)
             (setq predicate function))
            ((functionp function)
             (setq predicate (gensym))
             (setf (symbol-function predicate) function))
            ((and (consp function) (eq (car function) 'lambda))
             (setq predicate (gensym))
             (compile predicate function))
            (t (error "~S is neither a lambda expression, function or symbol." function)))
      `(satisfies ,predicate)))

Now you can even type-check on lambda expressions, and quasiquotation can sidestep the issue of capturing variables.

  (defvar foo 'bar)
  (typep 'bar `(satisfiesp (lambda (x) (eq x ',foo))))
  => T

https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node44.html

[BoingBoomTschak]

The CLHS sez "Recursive expansion of the type specifier returned as the expansion must terminate, including the expansion of type specifiers which are nested within the expansion." though. As expected, here on SBCL, your typep blows the stack.

> Most of the standard types from which derived types can be made are parametric types

I meant "parametric with a type parameter", but yeah.

> satisfies

I was (obviously, I hope) talking about static, not runtime typing.

[dokyun]

> The CLHS sez "Recursive expansion of the type specifier returned as the expansion must terminate, including the expansion of type specifiers which are nested within the expansion." though. As expected, here on SBCL, your typep blows the stack.

Weird, I tried it in CLISP and ECL and it worked fine. It looks like this issue was considered during the standard: https://www.lispworks.com/documentation/HyperSpec/Issues/iss... If you ask me that's a misfeature and not the Right Thing, but I was able to work around it by using a helper function and the type I wrote earlier, although it does lose more in comparison:

  (defun list-of-p (list type)
    (and (consp list)
         (typep (car list) type)
         (or (null (cdr list))
             (list-of-p (cdr list) type))))

  (deftype list-of (type)
    `(satisfiesp (lambda (x) (list-of-p x ',type))))

I will admit one of the double-edged swords of Common Lisp is that some of these rough edges are ultimately left up to the implementation, so there are a lot of very powerful features that are only `de-facto' standard or come with a lot of portability glue. However, many programs are also not designed with portability in mind. It would be nice if SBCL in particular could be made to adopt this use of types.

> I was (obviously, I hope) talking about static, not runtime typing.

The only difference between static and runtime typing would be the stage at which the types are evaluated, and being the same as macros they might be more interesting in that regard since they might have to consider what it means to run at both stages of evaluation.

[BoingBoomTschak]

> It would be nice if SBCL in particular could be made to adopt this use of types.

I agree, that would be an easy extension (at least from the user-facing API PoV) and would tremendously improve the language!

> The only difference between static and runtime typing would be the stage at which the types are evaluated, and being the same as macros they might be more interesting in that regard since they might have to consider what it means to run at both stages of evaluation.

That is the only difference, but that difference has important consequences on optimization.