Re:Understanding contravariance
by willtim on Friday June 22, 2018 @09:23AM
(#17373734)
I thought your comment was specifically about co/contraviance in type parameters with subtyping, because industry has explored the idea of making this unsound (e.g. the Google Dart team). But yes, co/contravariance pops up everywhere and so an unsound type system (or no type system at all) is not the answer. We had best all understand it!
[ Parent
| on HN ]
> so an unsound type system (or no type system at all) is not the answer
And my unpopular opinion is precisely that. "Sound" typesystems enforced at the expense of the kind of cognitive load we see here will hurt rather than help the expression of real world problems in code.
Literally, casting a C function pointer through a void* is a better answer. I'm serious.
But the problem of correct program construction does not go away. There is certainly a middle ground somewhere, beyond which proofs become too expensive for most users. For the sorts of systems I work on, the sweet spot is close to Haskell 98, for others it may well be Python (no types at all).