[throwthrow0987]

If you have an effect ReadsFromDB, you can't enforce statically that someone will not come along and change the ReadsFromDB effect to write to the db. That's why I think Haskell got it right in the first instance, functions are either pure or IO.

[jorkadeen]

What do you mean? In Flix, if a function has "Bool" as a return type then it can only return a Boolean value. That's what a type system ensures. Similarly, in Flix if a function has the "ReadsFromDB" effect then it can call operations that cause "ReadsFromDB"-- but it cannot cause any other effect. In particular, if there is also a "WriteToDb" then it cannot perform that effect.

This is not just aspirational. It is an iron-clad guarantee; it is what is formally called "effect safety" and it has been proven for calculi that model the Flix type and effect system.

To sum up: In Flix:

- If a function is pure then it cannot perform side-effects.

- If a function has the Console effect then it can only perform operations defined on Console.

- If a function has the Console and Http effect then it can only perform operations defined on Console and Http.

and so on.

[thdhhghgbhy]

But you have user defined effects don't you? E.g say I define an effect ReadsFromDB, it doesn't necessarily do what it says on the tin, and there is no way a compiler can check that it does. It could read from the db, and send some rockets into space. So a consequence of that is that these "effect systems" just amount to giving names to blocks of code. That's not necessarily a bad thing.

[xigoi]

If you define a variable called number_of_apples, there is no way for the compiler to check that it actually contains the number of apples. How is that different?

[thdhhghgbhy]

It's different. Effect systems claim to be a 'major evolution' that 'enforce modularity'. But they don't really enforce anything other than the modularity provided by standard oop classes or if in a fp language, function modules.