10
$\begingroup$

Type systems and programming languages are sometimes described as being sound, or unsound, or sometimes just "not sound". What does being sound actually imply about them? Is it always the same thing, or does the context matter sometimes?

$\endgroup$
3
  • $\begingroup$ It might be appropriate to tie in mathematical soundness, which I think is related to the meaning of soundness vis. type systems. $\endgroup$ Dec 15, 2023 at 23:32
  • $\begingroup$ @D.BenKnoble There is enough to talk about there that it would be worth making that into its own question (if not more than one). And before you can answer the question, you need to first answer the questions "how do type systems relate to mathematical logic? And how does 'semantics' (especially operational semantics), in the sense of programming languages, relate to mathematical logic?" $\endgroup$ Dec 16, 2023 at 15:44
  • 3
    $\begingroup$ For some practical examples see stackoverflow.com/questions/23939168/… $\endgroup$ Jan 10 at 4:12

3 Answers 3

5
$\begingroup$

A language has a sound type system if every well-typed program behaves as defined by the language's semantics during execution, avoiding runtime type errors. Robin Milner, who introduced this concept, famously stated that "well-typed programs cannot 'go wrong'," meaning they don’t get "stuck" during execution. "Getting stuck" means reaching a state which is neither a final state nor a state which can take a step according to the language's semantics.

There are two main approaches to type soundness: syntactic and semantic.

Syntactic type soundness

This approach, formulated by Wright and Felleisen, is by far the most popular. It consists of two theorems, often called "progress" and "preservation".

  • Progress: A well-typed expression is either a value or it can take a computational step according to the semantics of the language.

  • Preservation: Whenever an expression takes a step, its type does not change.

Semantic type soundness

This is a more general approach. An expression of type $A$ is semantically type sound if it "behaves like it has type $A$" at runtime. This approach takes into account how unsafe features might be used together with abstraction features to ultimately produce safe programs. Syntactic type soundness, on the other hand, is often too conservative in such cases.

See this blogpost by Dreyer et al. for more details. Additionally, Dreyer gives a talk on this topic here. See also the recent paper A Logical Approach to Type Soundness by Timany et al.

There is more technical detail on what it means for a program to "take a step" according to a semantics in the answer here. These technical details, however, are not necessary to know if you only want an intuitive understanding of type soundness.

Further reading

Blogposts

Papers

Talks

$\endgroup$
3
$\begingroup$

Formally, if a language is sound, for all programs $P$, types T and values v that can possibly exist in this language, if $P$ is well-typed and an expression in $P$ has type T and evaluates to v, v is an instance of T.

Informally, a type system is sound if you can't create runtime type errors, i.e. you can't assign a String to an Int. To clarify, you can type up a program which assigns a value of type String to a variable of type Int, but the type-checker will reject it and the compiler won't compile it. In an unsound type system, if you make this assignment convoluted enough, the type-checker will be "tricked" and let you compile the program; then when you run it and the unsound assignment is executed, at best you'll get an unexpected "runtime type mismatch" exception when you didn't make any casts, at worst the interpreter/machine will proceed unaware and you'll get undefined and/or weird behavior.


Even "strongly-typed" programming languages like Java and Rust may be unsound in niche ways: counterexamples. Strong type system ≠ sound type system and weak type system ≠ unsound type system; strong means the type system has more rules and less implicit casts, sound means that the type system's rules are consistent. Here's a program which, in older versions of Java (up to 2016), throws a ClassCastException despite not having any casts (source, related stack-exchange):

// Counterexample by Nada Amin and Ross Tate
class Unsound {
  static class Constrain<A, B extends A> {}
  static class Bind<A> {
    <B extends A>
    A upcast(Constrain<A,B> constrain, B b) {
      return b;
    }
  }
  static <T,U> U coerce(T t) {
    Constrain<U,? super T> constrain = null;
    Bind<U> bind = new Bind<U>();
    return bind.upcast(constrain, t);
  }
  public static void main(String[] args) {
    String zero = Unsound.<Integer,String>coerce(0);
  }
}

Fortunately, this kind of code isn't going to be written by accident, so while Rust, OCaml, and Haskell may have niche soundness issues, in practice they are considered "sound enough" (see the related stack-exchange post above for more explanation). But common languages have straightforward soundness bugs, including C, TypeScript, and even Java; here's an example you may have accidentally triggered which still works in Java today:

class Vehicle {}
class Car extends Vehicle {}
class Bus extends Vehicle {}
public class App {
  public static void main(String[] args) {
    Car[] c = { new Car() };
    Vehicle[] v = c;
    v[0] = new Bus(); // crashes with ArrayStoreException
  }
}

In formal models soundness is an unambiguous equation, but in the real world there are a few nuances:

  1. If a language lets you explicitly downcast (from Base to Subtype, like in C++ and Java, (Subtype)base), is it still sound?

  2. If a language implicitly downcasts, but throws a "runtime type exception" instead of silently ignoring, is it still sound? (Java examples above)

  3. If a language silently ignores type errors but never produces formally undefined behavior, is it still sound? (TypeScript, because you can have a value of the wrong type but JavaScript is nearly SEGFAULT-proof).

I think that all 3 are considered unsound, but I argue that only 2 and 3 are problems. If you really care about soundness and the only places it breaks are explicit operations, you can just not do those operations. The real issue with unsound languages is when you accidentally, unawarely cause a soundness bug; these are painful to debug for me (and I assume most programmers) who rely on the type system and expect mis-typed values to show up at compile time, or in the explicitly-unsound casts. But to be unambiguous, I'd still call languages which satisfy 2 and 3 "mostly sound" or "sound enough".

$\endgroup$
7
  • $\begingroup$ That Java program does not throw a ClassCastException; it is a static error. $\endgroup$
    – Michael Homer
    Dec 16, 2023 at 0:44
  • $\begingroup$ I don't think an explicit cast would usually be considered unsound, technically speaking (particularly a downcast). An explicit cast can be a lot like applying a function that takes an argument of one type and happens to produce a result of a different type. Though, it does depend a lot on the specific details of the type system and the semantics. $\endgroup$ Dec 16, 2023 at 1:17
  • $\begingroup$ It looks like the Java unsound example was fixed, which means I don't trust the other counterexamples weren't also fixed, so I updated to say these languages may be unsound. $\endgroup$
    – tarzh
    Dec 16, 2023 at 1:53
  • $\begingroup$ @tarzh the second Java example is a well known example of Java array (co)|(contra)variance, not present in Kotlin for example $\endgroup$
    – Seggan
    Dec 17, 2023 at 4:11
  • $\begingroup$ Does this mean that dynamically typed languages are by definition unsound? $\endgroup$
    – Seggan
    Dec 17, 2023 at 4:11
1
$\begingroup$

Soundness is a property of a type system. A type system assigns a type to a program (or expression). The assignment is sound when indeed the evaluation of that program (or expression) always yields a value of that type. As extension of this, a type system is sound when all its type assignments are sound, that it, reflect the evaluation of the program (or expression).

The soundness of a type system is proven against a formalisation of the semantics of a language. Both the type system and the formal semantics may capture only part of the behaviour of an actual language.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .