6 ms·

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 relat

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.

kbenson 10y ago
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.
- catnaroek 10y ago
  > far from the only useful thing 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.
  - kbenson 10y ago
    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.
    - catnaroek 10y ago
      > safety and versatility 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 Then what exactly is it?
      - kbenson 10y ago
        > That's exactly what expressiveness is. 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.

kbenson 10y ago

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.

catnaroek 10y ago
> far from the only useful thing 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.
- kbenson 10y ago
  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.
  - catnaroek 10y ago
    > safety and versatility 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 Then what exactly is it?
    - kbenson 10y ago
      > That's exactly what expressiveness is. 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.