To be fair, I like pluggable type systems a lot. I don't think that privileged type systems are the end-all-be-all.
I disagree a lot that the current effect systems don't prevent errors, however. You're right that linear types are difficult to encode in Haskell at least, but you can get away with a lot of bang for relatively little buck even without them.
The right choice (or choices) in design space here is a big challenge. It'll be exciting to see new research as it develops. I'm especially excited to see what comes of Pfenning's Pi calculus linear types [0].
[0] To be clear, I don't know if they're "his" excepting that he appears to be doing a lot of modern research there and that's where I learned about them.
I disagree a lot that the current effect systems don't prevent errors, however. You're right that linear types are difficult to encode in Haskell at least, but you can get away with a lot of bang for relatively little buck even without them.
The right choice (or choices) in design space here is a big challenge. It'll be exciting to see new research as it develops. I'm especially excited to see what comes of Pfenning's Pi calculus linear types [0].
[0] To be clear, I don't know if they're "his" excepting that he appears to be doing a lot of modern research there and that's where I learned about them.