Types – how to specify the element type in the vector of SbCl (or common LISP)?

I tried in SbCl 1.1 14, but it seems that type checking ignores the declaration of the vector element

(defun test (vec)
  (declare (type (vector integer) vec))
  (format nil "~a~&" (elt vec 0)))

Any tips? thank you!

Solution

First, note that declaration as type checking is not provided by standard ANSI Common Lisp This is an extension introduced by cmucl SbCl is a descendant of cmucl

The Common Lisp type system applies to vectors and arrays in a somewhat unusual way

Element type

Creating array with element type This means that the LISP system will create an array that can store elements of this type However, Common Lisp does not require a special array version for each element type If a particular version of the array is not available, the element type is promoted to the next "larger" type

Element type upgrade example

CL-USER 14 > (upgraded-array-element-type '(unsigned-byte 1))
(UNSIGNED-BYTE 1)

CL-USER 15 > (upgraded-array-element-type '(unsigned-byte 2))
(UNSIGNED-BYTE 2)

Therefore, there are array versions optimized for (unsigned byte 1) and (unsigned byte 2)

CL-USER 16 > (upgraded-array-element-type '(unsigned-byte 3))
(UNSIGNED-BYTE 4)

OOPS！ There is no array optimized for (unsigned byte 3) If you request such an array, you will get a slightly larger array (unsigned byte 4)

CL-USER 17 > (upgraded-array-element-type '(unsigned-byte 4))
(UNSIGNED-BYTE 4)

CL-USER 18 > (upgraded-array-element-type '(unsigned-byte 5))
(UNSIGNED-BYTE 8)

CL-USER 19 > (upgraded-array-element-type 'integer)
T

The figure above shows that integers have no special array You'll get a generic array

Your code

(defun test (vec)
  (declare (type (vector integer) vec))
  (format nil "~a~&" (elt vec 0)))

So your statement really means:

The variable VEC is bound to a vector that can hold integers

This does not mean:

The variable VEC is bound to a vector that holds only integers

CL-USER 21 > (typep '#(a "b" #\c) '(vector integer))
T

The above returns true in my lisp, because the vector is a general vector, which can store integers So it checks the type of vector, but it doesn't care whether the contents of the vector are actually integer types It just says that the vector could contains integers

Predicate based type checking

Common Lisp allows type declarations to use predicates

CL-USER 28 > (defun vector-of-numbers-p (vector)
               (and (typep vector 'vector)
                    (every 'integerp vector)))
VECTOR-OF-NUMBERS-P

CL-USER 29 > (typep '#(a "b" #\c) '(satisfies arrayp))
T

CL-USER 30 > (typep '#(a "b" #\c) '(satisfies vector-of-numbers-p))
NIL

CL-USER 31 > (typep '#(1 2 3) '(satisfies vector-of-numbers-p))
T

But check it at compile time? Maybe not