← Back to context

Comment by ww520

3 days ago

Effect system allows programmers to annotate expressions that can have certain effects, just like the type system annotating type information on them, so compilers can enforce effect rules just like enforcing type rules.

For example for a type system,

  let a: Int      // this says 'a' has the type Int
  a = 5           // compiler allows, as both 'a' and 5 are of Int.
  a = 5.1         // disallowed, as 'a' and 5.1 are of different types.

Similarly for example for an effect system,

  let a: Int
  let b: Int!Div0 // 'b' is of type Int and the Div0 effect.
  let c: Int
  ...
  a = 1 / c       // disallowed, as '/' causes the Div0 effect which 'a' not supported
  b = 1 / c       // allowed, as both '/' and 'b' support the Div0 effect.

The effect annotations can be applied to a function just like the type annotations. Callers of the function need to anticipate (or handle) the effect. E.g. let's say the above code is wrapped in a function 'compute1(..) Int!Div0', a caller calling it can do.

  compute1(..) on effect(Div0) {
     // handle the Div0 effect.
  }