3 ms·

What is an unsound type system. Why and how is it relevant for programing?

• WalterBright 4y ago
  I can't give you a mathematical definition of it, but my intuitive one is that an unsound type system is a collection of kludges. It's relevant for programming because the language winds up with all kinds of ugly edge cases where things just don't line up right. With a sound type system, you can do things like compose a new type out of other types, and it will work consistently (not produce weird edge behaviors). For example, C's `void` type introduces anomalous behavior. A function returning `void` is not composable, e.g.: void foo(); void v = foo(); would work in a sound type system, but does not work in C. You'll see it in the compiler implementation because it's a special case that appears over and over.
  • Koshkin 4y ago
    Isn’t that why some other languages explicitly draw a distinction between a function and a procedure? I think ‘void’ was introduced in C to do the same thing, implicitly (because omitting the return type does not achieve that).
    • WalterBright 4y ago
      Yes, but Wirth (Pascal's inventor) was an academic, which is why Pascal has a separate notion of functions and procedures. `void` is a hackish special case in the type system, and not just for function returns. It's unsound.