> It's also nothing to do with static checking—“type safety” holds in all “dynamically typed” languages.
This. Exactly true, and often forgotten.
It's useful here to distinguish between conversions and casts. Conversions use type information to ensure computations remain sensical; the canonical example is a conversion between integers and floating-point values which makes sure you never end up feeding invalid bit patterns into the relevant arithmetic hardware. An example of a cast is taking a bit pattern you had been treating as an integral value and then telling the language it's a floating-point value, and there not being an error at that point.
Conversions don't break the type system; they use the type system. Casts throw types away.
Casts don't only throw types away, they can also add type information to otherwise untyped input, such as reading data from a file or an HTTP request payload.
> Casts don't only throw types away, they can also add type information to otherwise untyped input, such as reading data from a file or an HTTP request payload.
This is true. A more interesting example might be a program which creates database queries from user input casting input strings to the type "unescaped string", and then converting them to type "escaped string" by performing a string-escaping process on them. (A cast from "unescaped string" to "escaped string", which is done implicitly very often in languages where those types are not machine-checkable, is often disastrous.)
Right, but I don't think this sort of type "conversion" (e.g. some function with type signature like this in Haskell)
escapeQueryString :: ByteString -> Query
is really adding or throwing away type information, it's just a function that accepts one type and returns another type. So it's not related to casting, except that it's the opposite of casting. But what that gives you is the ability to compose it with any other function that you define as accepting a `Query` type, and the program will refuse to compile if you ever accidentally try to pass it a ByteString. So it's about enforcing an invariant, in other words.
While I mostly agree, by this definition most things called "casts" aren't anything of the sort. In C++, static_cast (when called on value types) and dynamic_cast are both conversions, not casts--- static_cast<int>(5.5) returns exactly what you'd expect. Java and C# use C-style syntax, but their semantics are the same as those C++ casts. And of course the same is true of non-C-derived languages like Swift.
By your definition, most "casts" are actually conversions--- and while that's probably true, it feels pretty unhelpful, in the same way that it feels unhelpful to say "Python only has one type".
I agree that the terminology I used in my post isn't mainstream, and I won't claim it is. However, I couldn't think of a different word which would have the same familiarity with this audience which could plausibly carry that meaning. If anyone else can come up with better words, I'll use them.
To be clear, here's what I mean:
Conversion: The machine looks at the current type to figure out how to transform the value into a valid instance of the new type.
Casting: The machine ignores the current type and simply applies the new type.
Type safety also trivially holds in any dynamically typed language. You just call all values the same type---suddenly "preservation" and "progress" hold without actually meaning anything.
That's why its "type safety of a system which captures interesting invariants" which is actually interesting.
> 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. Exactly true, and often forgotten.
It's useful here to distinguish between conversions and casts. Conversions use type information to ensure computations remain sensical; the canonical example is a conversion between integers and floating-point values which makes sure you never end up feeding invalid bit patterns into the relevant arithmetic hardware. An example of a cast is taking a bit pattern you had been treating as an integral value and then telling the language it's a floating-point value, and there not being an error at that point.
Conversions don't break the type system; they use the type system. Casts throw types away.