[junke]

Ok for parametric polymorphism: the identity function in OCaml has type 'a -> 'a, whereas in SBCL it is "(function (T) T)". On the other hand, "(lambda (x) (if x 0 1))" is a function from T (anything) to the type BIT, not to some arbitrary integer type. Moreover:

    (lambda (x)
      (unless (minusp (if x 0 1)) 
        (error "Oops")))

... has type "(function (T) NIL)", meaning that the function does not return a value. That means that types are propagated so that the test can demonstrably always fail. A type in SBCL defines what is returned when execution terminates normally. So for example the type of `(lambda (x) (loop))` is "(function T NIL)", because it never returns (yes, I know you cannot always tell if it halts or not). The bottom type NIL should not be confused with NULL, the singleton type for the NIL value.

In OCaml, exceptions are not visible by the type system and you can write:

    let f x = raise (Failure "NO")

... and still have the type 'a -> 'b

So the kind of analysis that make sense in a language, as well as their soundness, is relative to the properties you want to check. Would you say that OCaml type system is unsound because it allows you to run code that can raise exceptions at runtime? I would love to see more precise type checking in OCaml, for example, and it probably already exists (I'am interested, if anybody has an example). But it probably makes little sense over there.

The same goes for parametric polymorphism in Lisp. The most in-depth approach to bring parametric polymorphism in CL is LIL (https://common-lisp.net/~frideau/lil-ilc2012/lil-ilc2012.htm...), but since it is dynamic, people who view dynamic typing as a deficiency might see that as a restriction.

You also claim that the type system is "unsafe". On the contrary, types being checked at runtime is a safe approach (buffer overflow, etc.) and plays well with the fact that everything can be redefined at runtime (maybe you don't like this aspect). In SBCL, type declarations are assertions. With the default optimization levels, that means that if they cannot be proved, they are checked at runtime (with the few caveats listed in SBCL man page). So if your input variable X is type as NUMBER and the function terminates normally, then you know that X effectively was of type NUMBER (that's a guarantee instead of an assumption). That result can be used in the following calls so that checking the type of X is not necessary anymore (if it is not modified in the meantime). The only case where types are trusted blindly instead of being checked, when necessary, is when you set the safety level to zero. This can be changed locally, not necessarily as a global switch.

[jb1991]

Run time type checks in my experience mean a few things:

1) You can compile or run the program fine even if there are type errors.

2) An existing type error may never be caught if that particular block of execution never runs. Then you can have unexpected surprised later when you finally do something to trigger that block.

3) They are slower than static type checking due to the runtime costs of checking types. Statically-typed compilers can do enormous optimizations once they know exactly what the types are.

[junke]

I am fine with statically checking types, or any kind of proof. Are your floating points calculations always precise enough? Can you detect if no user inputs ever reaches critically secure code without being sanitized? Does this multi-threaded code ever deadlock? There are plenty of things that can be made to guarantee properties you care about, and the reason you do not always use them is because of budget (time, money). Do you always write contracts around your stuff? is it a good contract, not one that just repeat what your code does? If you don't, please understand that I don't always use static types for everything and in all cases. Also, my code is not purely functional either.

If I need to do smart things in Lisp ahead-of-time, I may want to use a DSL and prove whatever I want to prove on it, and generate correct-by-construction code that does not check things at runtime. I could use ACL2, too. Please note also that I can work in a different language when it makes sense.

3) Statically typed compilers include Lisp ones. My code is sometimes underlined in orange like yours, because I made some dumb typo or because types do not match. Likewise, optimizations are done too, in particular inside functions, where things are more static than in the global environment.

What about efficiency? Look at the postal system: you have to wrap letters and objects in enveloppe or packages (except postcards, which are like fixnum), put a label on it with many informations... what a waste of time and space! Yet, each object has a type now and can be dispatched reliably and efficiently. If you put your letter in the wrong box, you will have enough information to recover and perform your job. Once letters are all filtered out from packages, you can avoid checking that they are letters and gain some efficiency. You can build a new kind of service (drone-delivery?) with a special label and dedicated rules and integrate it within a running system without restarting the world. If anything goes wrong, you can have a generic error handling mechanism that does not crash everything. Static types are more like pipes: clean water here, used water there, and they never mix in a wrong way thanks to pipe calculus. So while I agree that static analysis can be great for doing crazy optimizations, there are use-cases where dynamic typing shines, and generally people replicate that using tagged objects anyway: think about game entities which are "typed" dynamically, or frameworks when you can load custom scripts (and those are generally not typed-checked, unlike Lisp).

2) You plan for failure. Even in a statically-type language, you'll have runtime bugs. Only in a mission-critical system are errors fatal. If you place restarts or error handlers accordingly, you'll have the opportunity to fix your stuff. Ask Erlang people about reliable systems.

1) Worse, you compile your code, the compiler complains but you can still run the produced code! Then you can test your error-handling code.

Seriously, this is not a problem in practice. Coding and testing are interleaved because the environment is right here awaiting orders. If you look at the end-result, I am doing the job of the static type checker by fuzzying input in a way that makes sense for that particular function. I also have a global view of the system and more context to decide what will happen at runtime, or not. When I fail (I am not proud of it, like most static analyzers), the runtime is here to catch it.