On 2017-04-19 15:58, Joachim Durchholz wrote:
Am 19.04.2017 um 15:13 schrieb Sergiu Ivanov:
However, there are a couple big "backdoors", like the IO monad.
Well, it's so awkward that people don't *want* to use it.
That's partly because IO isn't very well defined, and therefore used as a catch-all. It's like the "other mail" folder, a stuff-drawer in the kitchen or that one room in the basement: random things tend to accumulate and rot in there because they don't have a better place. One of the worst offenders from my perspective is (non-)determinism. Randomness can be seen as non-deterministic, but it doesn't need IO. At the same time, many things that are in IO are practically not less deterministic than pure functions with _|_ – once you have a good enough model. In other words, these things could be separated. It needs work, to model the real world, to go through all the stuff that's in that black box, to convince people to not use IO if they don't need to, to change the systems to even allow "alternative IOs"… so it's nothing that'll change soon. But my point is: The type system can only help you if there are precise definitions and rules, but IO is the "here be dragons" on our maps of the computational world – for one, because the open work I mentioned is one of the ways to explore that boundary between theoretical and applied computer sciences. IO is the elephant in the room of type-supported hopes of correctness. But then I agree with Joachim: it's also right in the center of the room where everyone can see, acknowledge, and avoid it. Cheers, MarLinn