Comment by Joker_vD
1 year ago
Could someone explain to me how effects are radically different from types? Every time I see them introduced, it's always "type and effect system", not just "extending the type system with effect types", yet the rules the effects obey seem to be fundamentally the same that e.g. the constrained generics follow.
I would describe an effect system as the part of a type system which describes actions and side effects rather than values. Under this definition, effects are radically different from types in the sense that apples are radically different from fruit.
This requires a somewhat broad notion of what types are in the first place. I think most people have a mental model of types that describes data types like int or string, but anyone familiar with Java knows what effects are because Java has the “throws” keyword, which is an effect. If your method in Java throws IOException, the method must be marked “throws IOException” or it is a type error.
So I think our definition of “type” should be broad enough to include effect systems.
Types usually describe values. Compilers use types to prove various things about possible values, like their size, alignment, valid bit patterns, etc.
Effects describe code. For example, a "panic" effect states that function may trigger panic/exception during its execution. In other words, existence or absence of an effect is a function property. You can view effects as special types which are used only for functions (to be slightly more precise, signature + effects form function type), but you would need to use a slightly more advanced notion of type system which includes subtyping, e.g. function "panic fn(u32) -> u64" can be used in place of "panic io fn(u32) -> u64".