J. Garrett Morris wrote:
By this logic, head is "unsound", since head [] throws an error. Haskell types are pointed; Haskell computations can diverge.
Well, there are those who would actually agree with that and banish 'head' and friends from the language. But I'll agree with you here. [As an aside - I'm finding that liberal use of Edward's non-empty list type, found in the semigroups package, solves many of those problems for me.] But there are two crucial differences. First, head is just a partial function, not basic language syntax. Second, the divergence of head is constant and well-known, and not dependent on the implementation of a type class at particular types by various library authors.
What happens after the computation diverges is irrelevant to type soundness.
Agreed. I'm not talking about type soundness, in the technical sense. I'm talking about engineering soundness. Thanks, Yitz