3 ms·
I thought your comment was specifically about co/contraviance in type parameters with subtyping, because industry has explored the idea of making this unsound (
by willtim 8y ago
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!
- ajross 8y ago> 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.
- willtim 8y agoBut 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).