> Type safety also trivially holds in any dynamically typed language. You just call all values the same type
This isn't what most dynamically typed languages do and I suspect you know it. The reason "1" + 1 works in Perl (that is, produces a defined value rather than an undefined one or a program crash) is because the Perl runtime uses type information to deduce which conversion needs to be performed and then performs it.
The fact the type information is deduced as opposed to declared explicitly doesn't make it anything other than type information.
"The fact the type information is deduced as opposed to declared explicitly doesn't make it anything other than type information."
As I understand it, the fact that it is determined dynamically rather than declared or deduced statically makes it other than type information. Specifically, it makes it tags.
I think that's a valid point. A good example of this is Tcl, where "everything is a string". There are various ways you can treat a given string (as an integer, as a list, etc), but that doesn't make the value those types, it just means it can be used as one.
string is integer 1 ;# true
string is list 1 ;# true (list of length 1)
As the post I linked labors over, "type" and "type safety" have particular, well-defined technical definitions. There are other meanings, in particular the one you suggest "type as Perl means it" is one, but they don't have a consistent formal definition and don't have a consistent notion of "type safety" so it's difficult to use them except in the regime of a single language.
Now, if we take "type" to mean this formal meaning I suggest then dynamic languages have exactly one type. This is a meaningful, if degenerate, analysis. Within this analysis, Perl has one type and trivially satisfies type safety because type safety essentially means "things don't randomly change types" plus "programs continue to evaluate until they reach pre-defined evaluation stopping points". Both of these hold trivially in a language with one type.
The system you refer to, given again that we're sticking with the "formal type" terminology, is called a "tag system". It exists "below" or "after" the static system which ensures type safety and can indeed induce interesting behavior. But, in particular, it is not an analysis which can be considered complete (in any turing compete language) because it depends upon running the program which can lead to non-termination.
So really the distinction is not "deduction" versus "declaration" but instead "static" versus "dynamic". In general, static types are less powerful but more complete and dynamic tags are more powerful but highly incomplete. To confuse the two is to create a tremendous headache all around.
> There are other meanings, in particular the one you suggest "type as Perl means it" is one, but they don't have a consistent formal definition and don't have a consistent notion of "type safety"
Yes, they do: Type safety means "everything happens due to controlled conversion, as opposed to arbitrary behavior when conversions are not performed". For example, feeding an integer bit-pattern into an FPU is going to cause arbitrary behavior: It might work, it might cause a fault, it might crash the system.
> Now, if we take "type" to mean this formal meaning I suggest then dynamic languages have exactly one type.
Then the formal meaning is too weak (that is, not useful enough) to talk about dynamic languages. This has nothing to do with how type-safe dynamic languages actually are.
> "things don't randomly change types"
True in Perl and Python.
> "programs continue to evaluate until they reach pre-defined evaluation stopping points"
This is either true in Perl or meaningless in any language.
> The system you refer to, given again that we're sticking with the "formal type" terminology, is called a "tag system".
Right. The formal type terminology is so weak it has to make up terms to put dynamic languages off to one side, because it can't handle them. That's not really a property of the languages.
> It exists "below" or "after" the static system which ensures type safety and can indeed induce interesting behavior.
That's because it is a type system just the same.
> But, in particular, it is not an analysis which can be considered complete (in any turing compete language) because it depends upon running the program which can lead to non-termination.
Some static type system evaluators aren't guaranteed to terminate:
Of course C's type system evaluator is, but C isn't strongly typed. It's weakly typed, because it has a way to convince the compiler to ignore type information and, for example, verify a program which will feed an integer bit-pattern to the FPU.
Look, we're fighting about terminology not meaning. I have carefully defined my terms and made statements which live entirely within that world. I have also described terms of a larger world, noted that these two formal systems are distinct and also how they fit together.
If you want to talk about that which I called "tags" I'm fine with that. I'm even fine with calling them "types" if you insist---so long as it's also made clear that these "types" have nothing at all to with "static types" as they are different beasts that are essentially non-comparable. That is all fine.
I take argument to trying to smooth out the distinction, though. That is essentially wrong and unworkable.
Static type safety is far from meaningless or weak, but it is absolutely different from your definition of "type safety" as used here. I argue that static types have a precise and meaningful formal definition which extends far beyond what your attempt to define "dynamic type safety" encompasses. What you offer isn't meaningless or invalid---it's just vague and changes depending upon the language you're considering.
This isn't what most dynamically typed languages do and I suspect you know it. The reason "1" + 1 works in Perl (that is, produces a defined value rather than an undefined one or a program crash) is because the Perl runtime uses type information to deduce which conversion needs to be performed and then performs it.
The fact the type information is deduced as opposed to declared explicitly doesn't make it anything other than type information.