3
I always see that term when I’m reading about type systems, I’d like to know:
2
Since I am not very academic I will answer what is most necessary to understand, someone more connected to the theory may find that not exactly so, I will speak just to understand why most people do not need to know this.
What is its meaning within the context of programming languages?
This is about robustness that I always talk about. The more "audible" is the type system of a programming language, the more robust the code tends to be because this sonority indicates that the type system does not allow to produce invalid states.
It is clear that dynamic typing languages have low sound. Weak typing languages can be even worse at this point. Even the static typed ones may not be as loud as the ones mentioned above.
Dynamic typing languages that do not have a Generics They can’t get that loud. Those that accept that the invalid state of a type also lowers the sound slightly, for example by accepting a value null. Variance is another sophistication required to indicate all possible states.
Higher-sounding languages often have other mechanisms such as Higher Kind type providing guarantees in addition to possible values.
These guarantees complicate the language for both the use and creation of the compiler. So many languages prefer not to be so soundness thus.
Haskell is a high-sounding language, it is often said that after compiling a code in Haskell it is certain that there is no error, except if the problem has been poorly defined.
Some people consider that you should check everything at compile time to be sound. It makes sense, but I don’t know if that definition is strictly correct, because we use the mathematical concept, which has no compilation. It may be hard to prove that something is wrong at runtime without breaking robustness, but I can’t guarantee that it’s not possible.
As far as I know, if a system of types does not let possible invalid states pass by, but also does not let possible valid states pass by, that is, the false positive occurs, it ceases to be audible, because it went by the easy way, not by the way that proved the validity. If you accept the premise that false positives don’t matter then any language that rejects all codes will be sound... and useless.
What a language means to have a sound type system?
It is precisely to have a type system that can express objects in the most detailed way and that the state is always valid.
It’s not that language has a sound type system, it has a sound level. I just can’t tell which point someone uses to say that something is audible or not, and people make these claims. At least in my understanding language can be partly sound. I don’t know why in all my research I never found anything to say about it, so I wonder if the person says "the X language is sound" she knows what she’s talking about. If I knew, I would explain why it is. If she says that a specific mechanism of language is sound, then it’s okay for me.
Sound is the academic way of saying that the type system is safe (not in the sense of invasion, but of not letting invalid states happen and break the program or go wrong).
What are the benefits?
Robustness is the main one, it doesn’t pass a code that can’t be proven wrong. Keeping a certain expressiveness and documentation in the code is another, but I think it’s related.
There are problems in a language having such a type system, if yes, which?
Complexity is a problem. It requires writing a lot of code to suit everything the compiler wants, it’s usually boring to program in those languages. Some languages try to make certain inferences, but this has limits.
Browser other questions tagged terminology characteristic-language language-independent
You are not signed in. Login or sign up in order to post.
In the undergraduate classes the teachers translated as correctness. With this term you can research and try to derive the meaning. It was a term widely used in computer theory and mathematical logic. It is related to completeness and soundness (I think they were the original terms).
– Danizavtz