Warm tip: This article is reproduced from stackoverflow.com, please click
common-lisp declare

Common Lisp difference between declare check-type

发布于 2020-04-22 11:22:13

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
Questioner
Student
Viewed
44
Rainer Joswig 2020-02-13 22:39

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.