[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?