The syntax should probably be something like
where E means "effect", e is the particular effect(s), and () is the result type of the evaluation. However we implement it, the space of effect annotations e should be a complete lattice. In particular, we want the ability to write something like "E None t" which is identical to t or "E Any t" which can have any effect (useful for wrapping weird C functions).
The syntax should probably be something like
where E means "effect", e is the particular effect(s), and () is the result type of the evaluation. However we implement it, the space of effect annotations e should be a complete lattice. In particular, we want the ability to write something like "E None t" which is identical to t or "E Any t" which can have any effect (useful for wrapping weird C functions).