"Type safe" is both a marketing line and a technical definition. As a technical definition, many languages are type safe (including, say, Ruby) but they achieve this by having very low meaning to their (static) types.

Typically, the marketing definition means "type safe and expressively typed" which outlaws trivial type systems and their trivial type safety.

I read your blog post, thanks for the longer description :)

I believe Haskell would be considered have "strong static typing". Unfortunately, "strong" in this context is less precise than one might like: both Haskell and Java are generally considered "strongly typed", but Java allows e.g. type casting in a way that will not be statically type checked.

Haskell also uses type inference rather than requiring type declarations, but that is not _directly_ related.

Java's casting is not totally statically type checked. IIRC, the behavior at runtime is very clear, though - you either get a successful cast, if the object you're casting really is an instance of what you're trying to cast it to, or else you get a ClassCastException (from memory, actual name may vary).

That's not totally static, but within the definitions of the article, it might be good enough to count as "type safety" without falling into the "null type safety" category.

Well, "strict" might be a better name for your "strong".

I don't think it's any less precise a concept. Java type system is less strict than Haskell's, has similar "strictiness" to Python or Ruby (while quite different in static typing), and is more strict than C, or Perl.

Type casting has to be modeled (more or less) as (a) upcasting only (b) a failure of type safety, or (b) an admission that the type system is entirely vacuous.

No, you can have downcasting that is checked for validity at runtime, a la Java (or C++ with RTTI). This is not a failure of type safety, since only valid casts will be performed. It's not vacuous, either - it's not just one big type.

What happens when a cast is invalid?

You have type-safe casts in Haskell, for instance, where the failure is reflected at runtime.

    cast :: (Typeable a, Typeable b) => a -> Maybe b

Those are alright.

In Java, IIRC, the cast fails with a ClassCastException. That seems to me to be "failure is reflected at runtime".

In C++ with RTTI, IIRC it returns null. That's also "failure at runtime" (of a sort), but you have to check it.

RTTI returns nullptr when casting a pointer, but it does throw an exception when casting references. Both of these behaviors are well-defined, although the first is kind of questionable.

Haskell also allows casting in a way that defeats static type checking - `unsafeCoerce`

"Type-safe" as used in the FP community tends to be a much stronger claim than what's described in this post. At the very least, throwing a runtime exception is considered "going wrong" in the Haskell community, and this post keeps throwing out examples of runtime exceptions as avoiding "going wrong".