Common Lisp difference between declare check-type

Question

Can some one explain the differences between the following two cases (specifically what the comments are saying if for me not understandable) which come from the CLHS on function:

;; This function assumes its callers have checked the types of the
;; arguments, and authorizes the compiler to build in that assumption.
(defun discriminant (a b c)
  (declare (number a b c))
  "Compute the discriminant for a quadratic equation."
  (- (* b b) (* 4 a c))) =>  DISCRIMINANT
(discriminant 1 2/3 -2) =>  76/9

;; This function assumes its callers have not checked the types of the
;; arguments, and performs explicit type checks before making any assumptions. 
(defun careful-discriminant (a b c)
  "Compute the discriminant for a quadratic equation."
  (check-type a number)
  (check-type b number)
  (check-type c number)
  (locally (declare (number a b c))
    (- (* b b) (* 4 a c)))) =>  CAREFUL-DISCRIMINANT
(careful-discriminant 1 2/3 -2) =>  76/9

Answer 1

CHECK-TYPE : runtime type checking and repair

check-type does an actual runtime check. It also usually provides a way to interactively fix the value.

* (let ((a "1"))
    (check-type a number)
    (+ a 2))

debugger invoked on a SIMPLE-TYPE-ERROR in thread
#<THREAD "main thread" RUNNING {10005184C3}>:
  The value of A is "1", which is not of type NUMBER.

Type HELP for debugger help, or (SB-EXT:EXIT) to exit from SBCL.

restarts (invokable by number or by possibly-abbreviated name):
  0: [STORE-VALUE] Supply a new value for A.
  1: [ABORT      ] Exit debugger, returning to top level.

(SB-KERNEL:CHECK-TYPE-ERROR A "1" NUMBER NIL)
0] 0

Enter a form to be evaluated: 1
3

DECLARE : Type declaration

Common Lisp is dynamically typed: each data object has a type.

Common Lisp additionally allows one to use static types for variables and functions. There are

• various types and compound types
• ways to define new types with deftype
• type declarations with declare
• subtype checks with subtypep
• runtime type checks with typep
• runtime type conditional with typecase, ctypecase and etypecase

Now Common Lisp implementations use type declarations for various things and what they do with them is highly implementation specific.

The main usage of static type declarations with (declare (type ...)) in Common Lisp compilers is:

• ignoring them. Typically Lisp interpreters and some compilers are completely ignoring them

• use them for speed and space optimization. This is done by many compilers. They can use these type declarations to create specialized code.

• use them for runtime type checks. Some implementations use type declarations for runtime checks.

• use them for compile-time type checks. Some implementations are using type declarations for compile-time type checks. Examples are sbcl and cmucl.

Note that the Common Lisp standard does not say how these type declarations are used. It just provides a syntax to define and declare types. Common Lisp implementations then either make use of them or ignore them.

Especially sophisticated use of type declarations can be found with SBCL and CMUCL.

Example for type checks

Let's see how SBCL uses type declarations for both runtime and compile-time type checks:

Runtime type check with SBCL:

* (defun add (a b)
    (declare (type number a b))
    (list a b))
ADD
* (add 1 "3")

debugger invoked on a TYPE-ERROR in thread
#<THREAD "main thread" RUNNING {10005184C3}>:
  The value
    "3"
  is not of type
    NUMBER
  when binding B

Type HELP for debugger help, or (SB-EXT:EXIT) to exit from SBCL.

restarts (invokable by number or by possibly-abbreviated name):
  0: [ABORT] Exit debugger, returning to top level.

(ADD 1 "3") [external]
   source: (SB-INT:NAMED-LAMBDA ADD
               (A B)
             (DECLARE (TYPE NUMBER A B))
             (BLOCK ADD (LIST A B)))
0] 

As we can see SBCL uses the type declaration for a runtime check. But different from check-type it does not offer to provide a different value and the corresponding re-check...

Compile-time type check with SBCL:

* (defun subtract (a b)
    (declare (type number a b))
    (concatenate 'string a "-" b " is " (- a b)))

; in: DEFUN SUBTRACT
;     (CONCATENATE 'STRING A "-" B " is " (- A B))
; 
; caught WARNING:
;   Derived type of (SB-KERNEL:SYMEVAL 'A) is
;     (VALUES NUMBER &OPTIONAL),
;   conflicting with its asserted type
;     SEQUENCE.
;   See also:
;     The SBCL Manual, Node "Handling of Types"
; 
; compilation unit finished
;   caught 1 WARNING condition
SUBTRACT

As you can see we are trying to use a number as a sequence. SBCL detects that at compile time and warns.

Answer 2

A declaration affects what happens at compile time. A check-type form is a run time guard.

So, the declaration form says “hey compiler, the values held by the parameters a, b, c can only be numbers”. The check-type form says “hey function, at this point in execution, check that the given values are of the stated type”.

Answer 3

I'm trying to learn some CL myself, so I'll provide the best answer I can. Common Lisp is a dynamic language as compared to a static language. For a static language, check out Haskell - it does a bunch of compile time checks to ensure types match up for all functions and lets you know if it fails. However, in Common Lisp, things are a little different.

However, in Common Lisp, variables aren't typed the way they are in languages such as Java or C++. That is, you don't need to declare the type of object that each variable can hold. Instead, a variable can hold values of any type and the values carry type information that can be used to check types at runtime. Thus, Common Lisp is dynamically typed--type errors are detected dynamically. For instance, if you pass something other than a number to the + function, Common Lisp will signal a type error. On the other hand, Common Lisp is a strongly typed language in the sense that all type errors will be detected--there's no way to treat an object as an instance of a class that it's not.

So the variables we declare as function arguments don't have a type by default. This may be a good read for you: https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node15.html. In the first paragraph, it reads as follow:

It is important to note that in Lisp it is data objects that are typed, not variables. Any variable can have any Lisp object as its value. (It is possible to make an explicit declaration that a variable will in fact take on one of only a limited set of values. However, such a declaration may always be omitted, and the program will still run correctly. Such a declaration merely constitutes advice from the user that may be useful in gaining efficiency. See declare.)

So whenever you make your functions, those variables are using can have any Lisp object as it's value.

And if we take a venture at declare we see the following:

There are two distinct uses of declare , one is to declare Lisp variables as "special" (this affects the semantics of the appropriate bindings of the variables), and the other is to provide advice to help the Common Lisp system (in reality the compiler) run your Lisp code faster, or with more sophisticated debugging options.

Lastly, if we look at check-type we see:

check-type signals a correctable error of type type-error if the contents of place are not of the type typespec.

In both cases for declare and check-type, we are giving the Common Lisp system advice on types and type checking. Let's look at the two example functions you provided.

First, the "discriminant" function uses the declare function to to assert that the arguments are indeed numbers and that the compiler doesn't need to check them. The careful-discriminant function uses check-type to ensure that each variable is indeed a number, and then performs the operation.

You may be asking "Why should I bother with that?", in which the answer is to provide either a more optimized function (discriminant) or a function that provides better debugging and more information on error (careful-discriminant). To show the difference, I fired up SBCL and defined both functions. Then, I used disassemble to show the machine code of each. Notice how careful-discriminant performs more checks than discriminant, leading to more machine code!

(disassemble #'discriminant)

; disassembly for DISCRIMINANT
; Size: 83 bytes. Origin: #x10023700D7                        ; DISCRIMINANT
; 0D7:       498B5D10         MOV RBX, [R13+16]               ; thread.binding-stack-pointer
; 0DB:       48895DF8         MOV [RBP-8], RBX
; 0DF:       840425F8FF1020   TEST AL, [#x2010FFF8]           ; safepoint
; 0E6:       488B55E8         MOV RDX, [RBP-24]
; 0EA:       488B7DE8         MOV RDI, [RBP-24]
; 0EE:       FF1425C0000020   CALL QWORD PTR [#x200000C0]     ; GENERIC-*
; 0F5:       488955D8         MOV [RBP-40], RDX
; 0F9:       488B55F0         MOV RDX, [RBP-16]
; 0FD:       BF08000000       MOV EDI, 8
; 102:       FF1425C0000020   CALL QWORD PTR [#x200000C0]     ; GENERIC-*
; 109:       488B7DE0         MOV RDI, [RBP-32]
; 10D:       FF1425C0000020   CALL QWORD PTR [#x200000C0]     ; GENERIC-*
; 114:       488BFA           MOV RDI, RDX
; 117:       488B55D8         MOV RDX, [RBP-40]
; 11B:       FF1425B8000020   CALL QWORD PTR [#x200000B8]     ; GENERIC--
; 122:       488BE5           MOV RSP, RBP
; 125:       F8               CLC
; 126:       5D               POP RBP
; 127:       C3               RET
; 128:       CC10             INT3 16                         ; Invalid argument count trap
NIL

(disassemble #'careful-discriminant)

; disassembly for CAREFUL-DISCRIMINANT
; Size: 422 bytes. Origin: #x10023701E3                       ; CAREFUL-DISCRIMINANT
; 1E3:       4D8B4510         MOV R8, [R13+16]                ; thread.binding-stack-pointer
; 1E7:       4C8945F8         MOV [RBP-8], R8
; 1EB:       840425F8FF1020   TEST AL, [#x2010FFF8]           ; safepoint
; 1F2:       EB44             JMP L1
; 1F4:       660F1F840000000000 NOP
; 1FD:       0F1F00           NOP
; 200: L0:   488B7DF0         MOV RDI, [RBP-16]
; 204:       4883EC10         SUB RSP, 16
; 208:       488B1571FFFFFF   MOV RDX, [RIP-143]              ; 'A
; 20F:       488B3572FFFFFF   MOV RSI, [RIP-142]              ; 'NUMBER
; 216:       4C894DD8         MOV [RBP-40], R9
; 21A:       488B056FFFFFFF   MOV RAX, [RIP-145]              ; #<SB-KERNEL:FDEFN SB-KERNEL:CHECK-TYPE-ERROR>
; 221:       B906000000       MOV ECX, 6
; 226:       48892C24         MOV [RSP], RBP
; 22A:       488BEC           MOV RBP, RSP
; 22D:       FF5009           CALL QWORD PTR [RAX+9]
; 230:       4C8B4DD8         MOV R9, [RBP-40]
; 234:       488955F0         MOV [RBP-16], RDX
; 238: L1:   840425F8FF1020   TEST AL, [#x2010FFF8]           ; safepoint
; 23F:       488B45F0         MOV RAX, [RBP-16]
; 243:       448D40F1         LEA R8D, [RAX-15]
; 247:       41F6C001         TEST R8B, 1
; 24B:       7512             JNE L2
; 24D:       4180F80A         CMP R8B, 10
; 251:       740C             JEQ L2
; 253:       41F6C00F         TEST R8B, 15
; 257:       75A7             JNE L0
; 259:       8078F129         CMP BYTE PTR [RAX-15], 41
; 25D:       77A1             JNBE L0
; 25F: L2:   EB47             JMP L4
; 261:       660F1F840000000000 NOP
; 26A:       660F1F440000     NOP
; 270: L3:   488B7DE8         MOV RDI, [RBP-24]
; 274:       4883EC10         SUB RSP, 16
; 278:       488B1519FFFFFF   MOV RDX, [RIP-231]              ; 'B
; 27F:       488B3502FFFFFF   MOV RSI, [RIP-254]              ; 'NUMBER
; 286:       4C894DD8         MOV [RBP-40], R9
; 28A:       488B05FFFEFFFF   MOV RAX, [RIP-257]              ; #<SB-KERNEL:FDEFN SB-KERNEL:CHECK-TYPE-ERROR>
; 291:       B906000000       MOV ECX, 6
; 296:       48892C24         MOV [RSP], RBP
; 29A:       488BEC           MOV RBP, RSP
; 29D:       FF5009           CALL QWORD PTR [RAX+9]
; 2A0:       4C8B4DD8         MOV R9, [RBP-40]
; 2A4:       488955E8         MOV [RBP-24], RDX
; 2A8: L4:   840425F8FF1020   TEST AL, [#x2010FFF8]           ; safepoint
; 2AF:       488B45E8         MOV RAX, [RBP-24]
; 2B3:       448D40F1         LEA R8D, [RAX-15]
; 2B7:       41F6C001         TEST R8B, 1
; 2BB:       7512             JNE L5
; 2BD:       4180F80A         CMP R8B, 10
; 2C1:       740C             JEQ L5
; 2C3:       41F6C00F         TEST R8B, 15
; 2C7:       75A7             JNE L3
; 2C9:       8078F129         CMP BYTE PTR [RAX-15], 41
; 2CD:       77A1             JNBE L3
; 2CF: L5:   EB3D             JMP L7
; 2D1:       660F1F840000000000 NOP
; 2DA:       660F1F440000     NOP
; 2E0: L6:   498BF9           MOV RDI, R9
; 2E3:       4883EC10         SUB RSP, 16
; 2E7:       488B15B2FEFFFF   MOV RDX, [RIP-334]              ; 'C
; 2EE:       488B3593FEFFFF   MOV RSI, [RIP-365]              ; 'NUMBER
; 2F5:       488B0594FEFFFF   MOV RAX, [RIP-364]              ; #<SB-KERNEL:FDEFN SB-KERNEL:CHECK-TYPE-ERROR>
; 2FC:       B906000000       MOV ECX, 6
; 301:       48892C24         MOV [RSP], RBP
; 305:       488BEC           MOV RBP, RSP
; 308:       FF5009           CALL QWORD PTR [RAX+9]
; 30B:       4C8BCA           MOV R9, RDX
; 30E: L7:   840425F8FF1020   TEST AL, [#x2010FFF8]           ; safepoint
; 315:       458D41F1         LEA R8D, [R9-15]
; 319:       41F6C001         TEST R8B, 1
; 31D:       7513             JNE L8
; 31F:       4180F80A         CMP R8B, 10
; 323:       740D             JEQ L8
; 325:       41F6C00F         TEST R8B, 15
; 329:       75B5             JNE L6
; 32B:       418079F129       CMP BYTE PTR [R9-15], 41
; 330:       77AE             JNBE L6
; 332: L8:   4C894DD8         MOV [RBP-40], R9
; 336:       488B55E8         MOV RDX, [RBP-24]
; 33A:       488B7DE8         MOV RDI, [RBP-24]
; 33E:       FF1425C0000020   CALL QWORD PTR [#x200000C0]     ; GENERIC-*
; 345:       488955E0         MOV [RBP-32], RDX
; 349:       4C8B4DD8         MOV R9, [RBP-40]
; 34D:       488B55F0         MOV RDX, [RBP-16]
; 351:       BF08000000       MOV EDI, 8
; 356:       FF1425C0000020   CALL QWORD PTR [#x200000C0]     ; GENERIC-*
; 35D:       4C8B4DD8         MOV R9, [RBP-40]
; 361:       498BF9           MOV RDI, R9
; 364:       FF1425C0000020   CALL QWORD PTR [#x200000C0]     ; GENERIC-*
; 36B:       488BFA           MOV RDI, RDX
; 36E:       4C8B4DD8         MOV R9, [RBP-40]
; 372:       488B55E0         MOV RDX, [RBP-32]
; 376:       FF1425B8000020   CALL QWORD PTR [#x200000B8]     ; GENERIC--
; 37D:       4C8B4DD8         MOV R9, [RBP-40]
; 381:       488BE5           MOV RSP, RBP
; 384:       F8               CLC
; 385:       5D               POP RBP
; 386:       C3               RET
; 387:       CC10             INT3 16                         ; Invalid argument count trap
NIL

---

As seen here, Common Lisp can also be compiled, which confuses some people. It is better answered here: How is Lisp dynamic and compiled?.

Answer 4

The difference between the macro check-type and type declarations is that the former cannot be ignored by the compiler (and, when the check fails, one can interactively correct the inputs), while the latter are merely hints to the compiler (and, much more importantly, to the readers of the code) which may be ignored by the compiler.