Nah, what's actually useful is to determine how much of your program specification can be enforced with a given type system. That's well defined, and even relatively easy to assess before you pick this or that language for a given project.
I agree that is useful, but it's far from the only useful thing, and I don't think it's entirely distinct from the point at hand. When dealing with subtopics, covariance and contravariance can be seen as a weakening of the type system to make certain things easier.
I think a case could be made that any subversion of requiring the exact type defined or requiring manual conversion is a weakening of the type system, for the definition of weakening that we are using. The important consideration is that neither stronger nor weaker are always necessarily better or worse.
I didn't say it's the only useful thing, but it's perfectly reasonable to measure the expressive power of a type system (or any other language feature, really) by how much it buys you.
> can be seen as a weakening
Covariance and contravariance support by no means "weaken" a type system - they allow you to express more statically, not less.
Well, is expression how we are measuring how "strong" a type system is? It's definitely one way to measure it, but I would rather describe those in terms of safety and versatility. If by "strong" in a type system we mean explicitly following what was spcifically defined, then allowing anything except the specified type can be viewed as a weakening of the type system, regardless of whether it's provably safe or allows more expressiveness. That is, I think strong and weak or orthogonal to to safety and expressiveness (even if usually stronger is safer. as with most things, anything taken to an extreme starts to lose it's useful attributes). I.e. stronger is not necessarily equivalent to better.
That's exactly what expressiveness is. If a type system is versatile enough, you can express what you need to express without bypassing type safety.
> anything except the specified type
Even in this sense, subtyping doesn't weaken a type system. The definition of subtyping is the subsumption rule: given `S <: T` and `x : S`, you can derive `x : T`. (TAPL, p. 182) For similar reasons, adding ML-style let polymorphism to a type system doesn't weaken it.
> strong and weak is orthogonal to safety and expressiveness
I wouldn't say so. Perl is expressive. That expression sometimes comes at a cost of safety, but not always. Safety and expressiveness are not necessarily related.
> Then what exactly is it?
The exactitude of requiring exactly what is expected, and not allowing any substitutions. I'll explain my reasoning below.
> Even in this sense, subtyping doesn't weaken a type system.
Subtyping doesn't even always make sense when talking about strong or weak types. Some languages don't even have subtypes, yet we can still talk about how strong or weak their typing is just by referring to how different types interact, and whether conversion between them is implicit or explicit. Again, I'll call on Perl, which is useful in that it's very, very far from the type systems you have been describing WRT Haskell and Rust (and many languages that use static typing and inheritance).
Perl has two types of typing, variable (data structure) typing, and value typing. Perl is fairly strongly typed when it comes to variable types. It's either a scalar (which can contain many things, including references to other types), an array, which contains scalars, or a hash, which contains scalars (I'll leave out typeglobs and filehandles since they are fairly specialized). Until a few years ago, you could not supply a scalar where a hash or array was expected (e.g., you could not push($foo,"string"), you could only push(@foo,"sting"); ). You could explicitly dereference a scalar containing an array reference to an array and push to that, but it was an explicit dereference which required a @ prefixed the scalar[1].
Perl is fairly weakly typed when it comes to values within scalars. It will attempt to automatically convert the type to the appropriate representation such that the operation makes sense. Thus, adding two strings containing numbers requires no explicit conversion. Concatenating two numbers a string doesn't either. Neither do any string or numeric comparisons, as the conversion is implicit within the operator, as it knows what type it expects. This is why the expressions "1" + "2" and 1 . 2 in Perl are completely unambiguous. The first adds 1 and 2, yielding 3, the second concatenates the strings "1" and "2", yielding "12". The original type presented doesn't matter, it's implicitly converted as needed.
Subtyping, in this case, is irrelevant, because it doesn't exist in this language for these types of typing. It's entirely valid to talk about strong and weak typing in both these aspects or Perl, but they are both different and neither really matches the typing you are referring to with "type systems", because this language functions at a different level. The only way I can see using strong or weak typing as a descriptor across many languages, is to define it as how exact the type of data you are supplying needs to be to match what is expected. That is "strong" has entirely to do with constraints and explicitness. Anything that allows implicit action, even using a subtype which is known to be safe without some indication that you are raising or lowering the type explicitly so it can be used, is a weakening of that constraint (even if it's provably safe. Again, we aren't saying it's strongly safe, just that it's strongly constrained by type).
This reasoning leads to one of your original examples questions:
> Rust is even more weakly typed: boxes (as well as other user-defined pointer types) are implicitly converted to references, iterable objects are implicitly converted to iterators, etc
Yes. In some aspects, Rust has weakened it's typing in very specific circumstances to allow for more expressive programming, by not requiring explicit conversion when it can be inferred by the compiler. In this respect, Rust is more "weakly" typed that it could be, but it's also no less safe, no less fast, and more expressive for doing so, which I'm sure we would both agree is a good trade-off to make in this instance.
I hope that explains my view, and my reasoning, sufficiently. Let me know anything about my reasoning that confuses you, and I'll try to explain better (and of course feel free to poke holes where you see them).
1: Perl experimented with allowing core functions that expected an array or hash to allow a scalar containing a reference to such to work without the dereference, but ended up backing out that change.
Sure, but I was talking about the expressiveness of the type system, not the term language. The expressiveness of a type system lies in how much it tells you about your program, without having to actually run it.
> Rust has weakened its typing
I was trying to use reductio ad absurdum to question the validity of your definitions. I expected "Haskell is weakly typed" and "Rust is weakly typed" to be self-evidently false propositions.
> Sure, but I was talking about the expressiveness of the type system
Expressiveness can be described as expressiveness. I'm not sure why we would need to use strong/weak as an alternative to that term. IMO, it makes the strong/weak terminology less useful by tying it to this concept, which is only really relevant in some languages.
> I was trying to use reductio ad absurdum to question the validity of your definitions. I expected "Haskell is weakly typed" and "Rust is weakly typed" to be self-evidently false propositions.
I'm not sure if this is implying that we disagree on something that you still see to be self evident, or it's meant to explain why you included that and you no longer think it's a position worth holding?
In any case, I think it's worth clarifying that I didn't call Rust weakly typed, I said it hda weakened it's type constraints in a select few cases to increase expressiveness, where it did not cost in safety. (Constraints because everywhere you put strong/weak I think you can append constraints to be more explicit). I don't think it's controversial to say "Rust weakened constraints the type system imposed in some cases where it could be done safely, such as in iterable objects implicitly being seen as iterators in some cases", as that's clearly a bit less constrained than it could be.
Expressiveness is always relative to what a system is meant to express. The purpose of a type system isn't to write your actual programs in it. You use a type system to make sure that programs written in another language (a term language) make sense. So a type system is expressive to the extent it accurately captures the distinction between programs that make sense and programs that don't. (Of course, Goedel tells us that no decidable type system can perfectly capture this distinction.)
As for strong/weak, I don't think the concept is very useful without a clear technical definition in the first place.
> As for strong/weak, I don't think the concept is very useful without a clear technical definition in the first place.
Well, it's definitely not very useful in our case. ;) In all seriousness, as I said previously, I think it's useful for conveying a mixed bag of things to people that aren't very well versed in the specifics. If the person knows something about type systems, you should naturally have more specific language to fall back on to express your intent better.
In any case, I think we are way past of this being worthwhile to continue. I think we've plumbed the depths of this topic, whether we agree or not.
