3 ms·
> Static types do not help at all with software quality, beyond catching some typos I strongly disagree. A type like 'NonEmptyList(A) -> B' gives us more infor
by chriswarbo 6y ago
> Static types do not help at all with software quality, beyond catching some typos
I strongly disagree. A type like 'NonEmptyList(A) -> B' gives us more information than 'List(A) -> B': in programming terms it eliminates the empty case; in logical terms it provides a proof of 'A'. Note that we can represent 'NonEmptyList(A)' using 'Pair(A, List(A))', but give it a nicer list-like API.
Even simple nominal typing can provide useful guarantees, e.g. 'query : String' allows SQL injection, which we can eliminate by defining a separate 'SQL' type. We can represent 'SQL' using a string (we can even make it zero-cost using 'newtype', 'AnyVal', etc.), but crucially we can restrict its API to only allow safe operations, e.g. we can guarantee that strings are escaped by making the escaping function the only way to convert 'String' to 'SQL'; this also prevents double-escaping, since we we can't pass 'SQL' into the escaping function). The exact same technique prevents any injection attack (shell injection, 'eval', etc.).
Maybe such things could be called 'typos', but that's just a rhetorical sleight-of-hand; if injection attacks are typos then typos are incredibly dangerous (e.g. https://nakedsecurity.sophos.com/2018/02/19/hackers-sentenced-for-sql-injections-that-cost-300-million https://nakedsecurity.sophos.com/2018/02/19/hackers-sentence... ). We could say static types are great for software quality, since they can even catch typos (which, as we've established, are incredibly dangerous)!