5 ms·

> 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

by cbd1984 12y ago

> 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.

kyllo 12y ago
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.
- dllthomas 12y ago
  Arguably, there is an intersection of "cast" and "conversion" where casts are valid.
- cbd1984 12y ago
  > 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.)
  - kyllo 12y ago
    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.
tel 12y ago
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. http://jspha.com/posts/six_points_about_type_safety/ http://jspha.com/posts/six_points_about_type_safety/
- cbd1984 12y ago
  > 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.
  - dllthomas 12y ago
    "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.
    - RHSeeger 12y ago
      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)
  - tel 12y ago
    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.
jeorgun 12y ago
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".
- cbd1984 12y ago
  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.

by cbd1984 12y ago

kyllo 12y ago

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.

dllthomas 12y ago
Arguably, there is an intersection of "cast" and "conversion" where casts are valid.
cbd1984 12y ago
> 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.)
- kyllo 12y ago
  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.

tel 12y ago

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. http://jspha.com/posts/six_points_about_type_safety/ http://jspha.com/posts/six_points_about_type_safety/

cbd1984 12y ago
> 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.
- dllthomas 12y ago
  "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.
  - RHSeeger 12y ago
    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)
- tel 12y ago
  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.

jeorgun 12y ago

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".

cbd1984 12y ago
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.