2 ms·
In a statically-typed language, the starting point is "nothing typechecks". Then each additional language feature (e.g. generics, records, ADTs, lifetimes) must
by srssays 10y ago
In a statically-typed language, the starting point is "nothing typechecks". Then each additional language feature (e.g. generics, records, ADTs, lifetimes) must be implemented as an additional capability of the type checker. This "nothing is allowed unless explicitly permitted" is a necessary condition for soundness.
The most important goal for any programming language is that it is useful, i.e. it can express common patterns without hacks or kludges. Languages that are not useful tend to be forgotten.
However, chasing the dual goals of usefulness and soundness inevitably leads to type-system bloat. If "nothing is allowed unless explicitly permitted" and "everything must be somehow allowed" then it the list of things that are explicitly permitted will end up being very, very long.