"Statically-typed" and "type-safe" don't mean the same thing.
"Type-safe" means that the type of a value is always correct. For example, if I have a function of type Int -> String, a type-safe language will not let me pass it a Float argument, no matter what I do. A type-unsafe language might let me, if I can "cast" the value to a new type without changing its representation (ie. it's still a Float, but the type-checker now thinks it's an Int).
Type-safe languages are preferred over type-unsafe languages, since they avoid all kinds of problems like undefined behaviour.
"Statically-typed" means that every variable, function argument, return value, etc. is associated with (usually one, "principle") type. These may be written explicitly, inferred, etc.
"Dynamically-typed" means that all values use the same static type. This type is usually a recursive sum of lots of useful types, for example (in pseudo-Haskell):
type UniType = I Int | L [UniType] | F (UniType -> UniType) | O (Object UniType) | E Error | ....
Dynamically-typed languages are type-safe, but in a trivial way: there's no way for a value to have the wrong type, since there's only 1 type!
Many users of dynamically typed languages don't realise that static types are being used "behind the scenes", because:
* All of their code has the same type, so there's no need for any annotations, inference, type-checking or compilation. Many believe it's because there are no types, rather than the fact these have been made trivial.
* Sum types and recursive types aren't widely known, especially to those using dynamic languages who don't need to care about types at all. Hence, many make the assumption that "I don't know how to type this code" implies "this code is untypeable" and refer to such things as 'dynamic behaviour'.
* Many dynamic languages are implemented in languages with unsafe, anemic type systems, like C. Since 'dynamic behaviour' can't be represented safely in these languages, it's implemented unsafely, reinforcing the assumption that dynamic languages aren't type-safe.
* Other dynamic languages are implemented in themselves, which hides the UniType underlying it all.
* A few dynamic languages are implemented in languages with strong, safe type-systems, where the UniType is explicit and obvious, but most users stick to the dynamic language and never look at the implementation.
* Many languages confuse terminology by using the word "type" to refer to tags (the "I", "L", "F", "O", "E", ... in my UniType above); for example "if (get_type(x) === "int") {...}" instead of "if (get_tag(x) === I) {...}", but this doesn't make sense: types don't exist at runtime and even if they did the "get_type" function would always return the same thing (the UniType). The fact that many languages represent tags as strings doesn't help either!
* Dynamic languages allow any variable to contain any value, but most of the time only a small part of this domain is expected. This causes most functions to be partial, but whenever this partiality is encountered, one of two things happens: a) the program fails with a "runtime type error", which is incorrect and doesn't make sense, b) the language supplies an error value in response, and is regarded as doing something "unsafe" or "untyped", when in fact error values are perfectly valid (I've tagged them with "E" above) and it's the programmer's fault for not handling all of the possible cases they (implicitly, via UniType) asked for.
The work you've linked to is about selectively weakening the types in a program, so rather than having the whole thing be unityped or the whole thing use distinct types, instead we can write code both ways, then automatically strengthen/weaken the types and lower/lift the functions, so that they interoperate. The types are always safe, but the unityped part will have many more partial functions than total functions.
In contrast, we can't (yet) make a type system "gradually safe", since a single unsafe cast can break anything else ("ex falso quodlibet"). It would require some kind of para-consistent logic, which I've never seen in type theory. The difference is that 'gradual types' let us say "Any" instead of "Int", whereas unsafe types let us say "X" instead of "Int", for any "X".
Well, to people like Bob Harper, there is no such thing as a dynamic "type" (they are tags instead). The argument over terminology appears on comp.types every once in awhile. Then there are people into dynamic languages who swear they have more than one type and actually check these types at run type. Then the static type theorists say...you are just checking tags, and the DL people are like...what's the difference?
The dynamic typing folks don't care to provide a definition of types and overload the term to mean many things, the static typing folks have a rigorous one.
It's a technical term so the colloquial definition has little relevance to it's use in computing. You can read the definition in TAPL or PFPL.
> tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
> It's a technical term so the colloquial definition has little relevance to it's use in computing. You can read the definition in TAPL or PFPL.
Technical books often define terms in a way convenient for the material and approach they are presenting, not in a way that is general to the field; particularly, if terms are used in different ways within the field at the time they are written, they typically have to choose for consistency within the book -- that doesn't make that definition the right one for the field, it simply means that's what the term means in the context of the work.
And, ultimately, the semantic argument is meaningless. It doesn't really matter whether you have static and dynamic types in different languages or you call the former "types" and the latter "tags" (except that the former terminology actually explains the difference in a way that tells you what the difference is every time you use the terms.) The substance is the same, and getting worked up over line-drawing regarding the boundary of "type" is a distraction from any discussion of substance.
Type is pretty much used by most programmers to mean "type" as it is stated in the dictionary; so dynamic type checking is not a misnomer to them. Only type theorists are diligent about the colloquial definition, but they can only really use it like that when talking to other type theorists.
Yes, the usage of the word "type" depends on the community; I would say it's not controversial to use the type-theoretic context here, since TFA is written by a type theorist.
However, my main point was that "type-safe" and "type-unsafe" are not synonimous with "static" and "dynamic". The original question was probably about static vs dynamic, but I think it's important to point out the distinction; especially when reading material like Bob's that assumes some familiarity with the terms.
From a Curry-Howard point of view:
* Static types are logical formulas, values are their proofs.
* "Dynamic types" are the clauses of one big disjunctive formula: Int OR Bool OR Error OR Array OR String OR ....
* Safe type systems are sound logics; they don't let us prove "FALSE".
* Unsafe type systems are unsound logics; they let us prove "FALSE", and hence anything (ex falso quodlibet).
Importantly, the big disjunctive formula used by dynamic languages is trivial to prove. For example, I can prove it with a constant like "10", without having to perform any computation. Trivial formulas are equivalent to "TRUE" (the logical proposition, not the boolean value!), hence dynamic languages only allow us to prove "TRUE". This makes them type-safe, since they can't prove "FALSE", but it makes them uninformative: proving "TRUE" doesn't tell us anything we didn't already know!
The only languages which can be type-unsafe are static languages, since they're the only ones which can express types other than "TRUE" (eg. "FALSE"). If a static language is unsafe, then there's essentially no benefit to it having static types, since we can't trust any of the information it gives us.
That's why academics prefer type-safe languages, whether they're static or dynamic, whether or not you agree with Harper that one's a sub-set of the other. Unsafe languages specifically hinder our reasoning. Sure, we might be confident that our particular C program is safe, despite C being an unsafe language, but we can't generalise that to "for all C programs 'P'...", which makes it difficult to study languages-in-the-abstract. Of course, we lose nothing if we make the language safe, so we might as well do that (eg. define a safe sub-set of C like http://compcert.inria.fr/doc/ ).
Essentially, asking "Why do programming languages researchers seem so enamored with type-safe languages?" is like asking "Why do Mathematicians seem so enamored with sound logics?". Of course, there is research in non-monotonic logics, para-consistent logics, etc. and that's great, but if we're going to have an academia-vs-industry debate, then I think the unsound logics, and hence the type-unsafe languages, have the taller ivory towers.
Of course, there are many other ways that static and dynamic languages may be safe or unsafe (eg. memory safety, thread safety, non-total, etc.). (Safe) type systems can eliminate some of these problems (eg. memory safety with linear types), but just because it's possible with some type-system feature doesn't make a language lacking that feature type-unsafe; the worst we could say is that it's type-uninformative.
For example, Haskell's type system doesn't distinguish total functions (eg. via a data/codata separation). This makes Haskell unsafe with regards to termination/cotermination, but it doesn't make Haskell type-unsafe. Since dynamic types are completely uninformative, they can't solve any problems that type systems are suited to, but that still doesn't make them type-unsafe.
For example, it's not that dynamic languages allow type-unsafe operations like passing strings to "+ : Int -> Int -> Int", it's that dynamic languages don't allow us to restrict the type of "+" at all; we can't even specify that it's a function, let alone what that function's input and return types are! If it generates a run-time error that's fine, since "run-time error" is a perfectly valid value, as far as the type system's concerned.
Now, we may think this is an unsafe thing to do, but it doesn't make the language type-unsafe. It just makes it "semantically unsafe" or "unsafe without lots of tests" or somesuch.
"Type-safe" means that the type of a value is always correct. For example, if I have a function of type Int -> String, a type-safe language will not let me pass it a Float argument, no matter what I do. A type-unsafe language might let me, if I can "cast" the value to a new type without changing its representation (ie. it's still a Float, but the type-checker now thinks it's an Int).
Type-safe languages are preferred over type-unsafe languages, since they avoid all kinds of problems like undefined behaviour.
"Statically-typed" means that every variable, function argument, return value, etc. is associated with (usually one, "principle") type. These may be written explicitly, inferred, etc.
"Dynamically-typed" means that all values use the same static type. This type is usually a recursive sum of lots of useful types, for example (in pseudo-Haskell):
Dynamically-typed languages are type-safe, but in a trivial way: there's no way for a value to have the wrong type, since there's only 1 type!Many users of dynamically typed languages don't realise that static types are being used "behind the scenes", because:
* All of their code has the same type, so there's no need for any annotations, inference, type-checking or compilation. Many believe it's because there are no types, rather than the fact these have been made trivial.
* Sum types and recursive types aren't widely known, especially to those using dynamic languages who don't need to care about types at all. Hence, many make the assumption that "I don't know how to type this code" implies "this code is untypeable" and refer to such things as 'dynamic behaviour'.
* Many dynamic languages are implemented in languages with unsafe, anemic type systems, like C. Since 'dynamic behaviour' can't be represented safely in these languages, it's implemented unsafely, reinforcing the assumption that dynamic languages aren't type-safe.
* Other dynamic languages are implemented in themselves, which hides the UniType underlying it all.
* A few dynamic languages are implemented in languages with strong, safe type-systems, where the UniType is explicit and obvious, but most users stick to the dynamic language and never look at the implementation.
* Many languages confuse terminology by using the word "type" to refer to tags (the "I", "L", "F", "O", "E", ... in my UniType above); for example "if (get_type(x) === "int") {...}" instead of "if (get_tag(x) === I) {...}", but this doesn't make sense: types don't exist at runtime and even if they did the "get_type" function would always return the same thing (the UniType). The fact that many languages represent tags as strings doesn't help either!
* Dynamic languages allow any variable to contain any value, but most of the time only a small part of this domain is expected. This causes most functions to be partial, but whenever this partiality is encountered, one of two things happens: a) the program fails with a "runtime type error", which is incorrect and doesn't make sense, b) the language supplies an error value in response, and is regarded as doing something "unsafe" or "untyped", when in fact error values are perfectly valid (I've tagged them with "E" above) and it's the programmer's fault for not handling all of the possible cases they (implicitly, via UniType) asked for.
The work you've linked to is about selectively weakening the types in a program, so rather than having the whole thing be unityped or the whole thing use distinct types, instead we can write code both ways, then automatically strengthen/weaken the types and lower/lift the functions, so that they interoperate. The types are always safe, but the unityped part will have many more partial functions than total functions.
In contrast, we can't (yet) make a type system "gradually safe", since a single unsafe cast can break anything else ("ex falso quodlibet"). It would require some kind of para-consistent logic, which I've never seen in type theory. The difference is that 'gradual types' let us say "Any" instead of "Int", whereas unsafe types let us say "X" instead of "Int", for any "X".