Thus quoth Joachim Durchholz at 18:39 on Wed, Apr 19 2017:
Am 19.04.2017 um 17:56 schrieb Sergiu Ivanov:
I wanted to say that, when the typechecker sees a function of type IO (), it only knows that it _may_ have side effects, but it cannot verify that these effects compose correctly with the effects coming from other functions in the IO monad.
Ah right. Even Haskell's type system is not able to classify and characterize side effects properly.
The language Eff seems to be built around an algebraic characterisation (according to the author, I haven't yet had the time to check) and handling of effects: http://www.eff-lang.org/ According to the page, the proposed formalism allows doing elegantly what in Haskell is typically done with monad transformers. I actually started thinking about porting the algebraic handling of effects to Haskell, which may be possible since its type system seems to be expressive enough, but my time is quite limited these days.
I don't think that that's a defect in the type system though; I've had my own experiences with trying to do that (based on design by contract, if anybody is interested), and I found it's pretty much uncontrollable unless you go for temporal logic, which is so hard to reason about that I do not think it's going to be useful to most programmers. (Temporal logic exists in several variants, so maybe I was just looking at the wrong one.)
Temporal logics kind of require guys with PhDs in your team :-) From what I know, the usual approach is designing (or adapting) a temporal logic for your specific task, since general properties are often undecidable. Your experience of handling effects seems interesting to me. -- Sergiu