3 ms·

Enough unit testing will test everything the type system can. However, that is way more work than a good type system.

• chriswarbo 3y ago
  > Enough unit testing will test everything the type system can Depends on the type system. For example, if we have parametricity then we can constrain possible values quite a lot; e.g. a value with type 'forall t. t -> t' is the identity function (or diverges, if our language is non-total). If we don't have parametricity, such values could do all sorts of shenanigans, e.g. def f[T](x: T): T = x match { case n: BigInt if isOdd(n) && isPerfect(n) => n+1 case _ => x } This acts as the identity function for all values of all types; except if we give it a BigInt which is an odd perfect number. This is probably the identity function, but ensuring there are no edge cases would require our test suite to solve a famously hard problem https://en.wikipedia.org/wiki/Perfect_number#Odd_perfect_numbers https://en.wikipedia.org/wiki/Perfect_number#Odd_perfect_num... (This sort of guarantee is known as a "free theorem", e.g. see https://bartoszmilewski.com/2014/09/22/parametricity-money-for-nothing-and-theorems-for-free https://bartoszmilewski.com/2014/09/22/parametricity-money-f... )