type-safety checking is performed at runtime
That doesn't really make sense to a type theorist. The definition of "type-safety" is only applicable statically.
What checking is done at runtime?
That doesn't really make sense to a type theorist. The definition of "type-safety" is only applicable statically.
What checking is done at runtime?
My favorite analogy for this is the restaurant one. Haskell insists on having two waiters: one to deliver the food and a second to deliver the check. Clojure allows one waiter to deliver both, but throws a fit and leaves the restaurant if the check arrives before the bill. Assembler eats the first thing that arrives and signs the second, even if the bill comes before the food.
Clojure is "type-safe" in that it will exit instead of performing an illogical action (e.g. dividing a string pointer by a network socket). It's just as type-safe as Haskell code littered with fromJust.
What you're talking about now is totality. Both Haskell and Clojure allow non-total functions (functions which may not return a result) - the checking that they do are to stop undefined results. Agda is an example of a language that only allows total functions.
The second was that Clojure arguably has a type system. There is exactly one type, Stuff. Every function takes Stuff and returns Stuff. Of course, functions themselves are a kind of Stuff. Now, it lacks totality, but otherwise every compiled Clojure program has passed the type checker. It's just that type checking is a no-op, since there's no way for anything to have the wrong type.