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.

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.

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?

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.