[bjourne]

Run time type checks affects the semantics of programs. Consider an identity function declared to only accept fixnums and returns fixnums. If you call this function with a string a type error will be signaled if run time type checks are enabled. This is sound. If you call this function with a string without run time type checks the function will return the string it got in. This is not sound because the run time thinks that it has a fixnum while in reality it is a string. The likely consequence is a segfault.

Think of soundness as a guarantee that if the program type checks, then all type declarations are correct. Note also that soundness is a property of the type system itself. A piece of code is not sound or unsound -- it is the type system itself that is.

[lispm]

SBCL is a strange Lisp implementation, since it does some compile-time type checks, too.

  * (defun id (f) f)
  ID
  * (declaim (ftype (function (fixnum) fixnum) id))
  (ID)

Our new identity function is declared to be of type fixnum -> fixnum.

  * (declaim (optimize (safety 0)))
  NIL

Now we've set safety to 0.

Let's define a function which calls ID with a string

  * (defun use-id (s) (declare (type string s)) (id s))
  ; in: DEFUN USE-ID
  ;     (ID S)
  ; 
  ; caught WARNING:
  ;   Derived type of S is
  ;     (VALUES STRING &OPTIONAL),
  ;   conflicting with its asserted type
  ;     FIXNUM.
  ;   See also:
  ;     The SBCL Manual, Node "Handling of Types"
  ; 
  ; compilation unit finished
  ;   caught 1 WARNING condition
  USE-ID

Even though safety is 0, the compiler warned us about a compile-time type problem.

[juki]

> Consider an identity function declared to only accept fixnums and returns fixnums. If you call this function with a string a type error will be signaled if run time type checks are enabled.

This would be the case that I referred to in the second paragraph of my last comment. I would agree if we were talking about explicit type checks, but a portable Common Lisp program cannot consider implicit added by the compiler to be part of the programs semantics, because a compliant implementation is not required to add any type checks. SBCL just adds them as a debugging aid, but if you rely on type errors being signaled, you have to check them explicitly with `CHECK-TYPE` or something equivalent.

> Think of soundness as a guarantee that if the program type checks

This would be where our view is different. You consider soundness to be a guarantee given by the compiler, while I consider it a property of the program itself (which can sometimes be checked by the compiler, and sometimes by the programmer). Common Lisp does not give any guarantee of type safety. SBCL simply tries to be helpful and catch most real world type errors, but ultimately it is the programmer who must ensure the soundness of the program.

[bjourne]

> This would be the case that I referred to in the second paragraph of my last comment. I would agree if we were talking about explicit type checks, but a portable Common Lisp program cannot consider implicit added by the compiler to be part of the programs semantics, because a compliant implementation is not required to add any type checks.

Hence if you want to talk about portable Common Lisp, you cannot achieve any type of soundness!

> This would be where our view is different. You consider soundness to be a guarantee given by the compiler, while I consider it a property of the program itself (which can sometimes be checked by the compiler, and sometimes by the programmer).

Your view is wrong. Read about type system soundness here https://papl.cs.brown.edu/2014/safety-soundness.html