> This is interesting, because I generally feel like getting the types right actually IS most of the work that needs to be done
When I was much younger, I was told by my elders that to a first approximation a function doesn't need a name because it's defined by its range and domain. If it's hard to discern what the function does just by the range and domain then your type system isn't powerful enough. This insight is as powerful as it is superficially wrong.
That insight is wrong. Not just superficially; it goes against the whole point of types.
1) Consider easing functions in animation (see easings.net for examples). They all have domain and range "real numbers between 0 and 1", yet they are all meaningfully different.
2) Consider filters in audio processing. They all have domain and range "streams of real numbers", yet they are all meaningfully different. The fact that they have the same type is important - it allows composition of filters, which I'd hope would sound exciting to a typed programmer!
3) Consider sorting algorithms. Even under a very advanced type system, the domain would be "arrays of numbers" and the range would be "sorted arrays of numbers". Yet there are tons of sorting algorithms that are meaningfully different. The fact that they have the same type is important - it allows a sorting library to evolve without breaking applications.
See the common thread? Types enable mixing and matching functionality. If a type allows only one functionality, it's useless for that purpose.
When I was much younger, I was told by my elders that to a first approximation a function doesn't need a name because it's defined by its range and domain. If it's hard to discern what the function does just by the range and domain then your type system isn't powerful enough. This insight is as powerful as it is superficially wrong.