[bjourne]

This method of adding static typing to a dynamically typed language is called gradual typing. It works and is sound but can come at a considerable cost if the compiler doesn't support it well.

Suppose that you have function that you know only returns fixnum, but isn't declared as such, and you use that result as the input to a function declared to only take fixnum then the compiler has to add runtime type checks. Even very cheap type checks can cause massive overhead if they are executed in tight loops.

Or suppose the fixnum x is given as input to an identity function: (id x). The compiler knows that x is a fixnum, but unless it is sufficiently smart it has no idea that (id x) is one too.

[juki]

This problem is somewhat lessened because SBCL also allows you to tell it to not add any implicit runtime type checks (explicit checks are still there) with an `(optimize (safety 0))` declaration. Of course, then you have to be sure that the code is indeed safe, so you probably don't want it as a global declaration, but only locally for the tight loops. When optimizing for speed SBCL also gives warnings for generic arithmetic, so you can add the necessary declarations.

[bjourne]

Sure, but then you lose soundness. That is, it becomes possible to fool the compiler into thinking, say, a string is a fixnum, leading to crashes. It becomes equivalent to the optional typing of mypy which also is easy too fool because it doesn't insert any type checks.

    def oh():
        return 'hi'
    x: int = oh()
    x + 3

It type checks fine but contains a type error.

[juki]

You don't lose soundness; you just tell the compiler to not check types at run time, because you've already done it yourself (e.g. by not exposing the unsafe code directly outside the package, but instead having a safe wrapper around it). This isn't really any different from using unsafe/foreign code in a statically typed language.

[bjourne]

Yes, you do lose soundness. You can lose soundness in statically typed languages too (even in Haskell). But the difference is the frequency in which it is lost. In SBCL Lisp, if you want fast code, the answer is "almost all the time".

[juki]

We must be using a different definition of soundness then. As I see it, implicit run time type checks do not affect the semantics of a program, and as such, do not have any bearing on its soundness. They're merely a debugging tool to help one detect unsoundness as early as possible in development, or to fail gracefully with good error logging in a production environment. Optimizing for `(safety 0)` only tells the compiler that you know the piece of code is sound, so there is no need to check at run time. It's still just as sound or unsound as it would be with the type checks.

I suppose you could argue that someone might write a program that relies on being able to call a function with the wrong type of arguments and catch the resulting error. In this case removing the type checks obviously changes the behavior of the program. This however would not be portable across different CL implementations anyway, so you should really be using explicit type checks.

> But the difference is the frequency in which it is lost. In SBCL Lisp, if you want fast code, the answer is "almost all the time".

SBCL code is fast enough for the vast majority of a program even with full run time type checking, so you would only be using `(safety 0)` for very performance critical code, whose safety you have ensured yourself. The `(safety 0)` declaration also does not disable any compile time checking that SBCL does.

[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.

[armitron]

> In SBCL Lisp, if you want fast code, the answer is "almost all the time".

Absolutely false, (declare (optimize (speed 3) (safety 1)) is perfectly valid.

[TeMPOraL]

> Suppose that you have function that you know only returns fixnum, but isn't declared as such, and you use that result as the input to a function declared to only take fixnum then the compiler has to add runtime type checks.

If you know, you can declare it. You can drop a (declaim (ftype ...)) anywhere you want, it doesn't have to be next to the function. You can also declare it locally, near the call site. Finally, you can always use `the', as in (the fixnum (yourfunction ...)), which declares what the return value at a given point is going to be.

As 'juki said, when you add (declare (optimize (safety 0))), SBCL will happily drop runtime type checks within the scope of the declaration. You can do that in as small a scope as possible, even doing something like this:

  (defun bar (y)
    (let ((x (locally
              (declare (optimize (speed 3) (safety 0)))
              (the fixnum (foo y)))))
      x))

The reason SBCL will insert some runtime type checks without (safety 0), even when a function is globally declared to accept and return some values, is because in Lisp, you can't assume a declaration will forever stay in force. Your function that always return fixnum can be redefined at runtime to occasionally return strings.