Error Localization for Sequential Effect Systems

Gordon, Colin S., Yun, Chaewon

30th Annual Static Analysis Symposium (SAS), October 2023, doi: 10.1007/978-3-031-44245-2_16

Abstract

We describe a new concrete approach to giving predictable error locations for sequential (flow-sensitive) effect systems. Prior implementations of sequential effect systems rely on either computing a bottom-up effect and comparing it to a declaration (e.g., method annotation) or leaning on constraint-based type inference. These approaches both give errors at locations or granularities far removed from where a mistake might have been made. Instead of relying on constraint solving, we draw on the notion of a residual from literature on ordered algebraic structures. Applying these to effect quantales (a large class of sequential effect systems) yields an implementation approach which accepts exactly the same program as an original effect quantale, but for effect-incorrect programs is guaranteed to fail type-checking with predictable error locations tied to evaluation order. We have implemented this idea in a generic effect system implementation framework for Java, and report on experiences applying effect systems from the literature and novel effect systems to Java programs. We find that the reported error locations with our technique are significantly closer to the program points that lead to failed effect checks.

Photos taken by Louis Rustenholz at SAS'23 and posted to the @symposiumSAS Twitter account.

Bibtex

@inproceedings{sas23,
  author = {Gordon, Colin S. and Yun, Chaewon},
  title = {Error Localization for Sequential Effect Systems},
  abbr = {SAS},
  booktitle = {30th Annual Static Analysis Symposium (SAS)},
  year = {2023},
  month = {October},
  bibtex_show = {true},
  arxiv = {2307.15777},
  url = {https://arxiv.org/abs/2307.15777},
  springer = {https://link.springer.com/chapter/10.1007/978-3-031-44245-2_16},
  doi = {10.1007/978-3-031-44245-2_16},
  youtube = {https://www.youtube.com/watch?v=QVI6VRHRySs},
  abstract = {
  We describe a new concrete approach to giving predictable error locations for sequential (flow-sensitive) effect systems. Prior implementations of sequential effect systems rely on either computing a bottom-up effect and comparing it to a declaration (e.g., method annotation) or leaning on constraint-based type inference. These approaches both give errors at locations or granularities far removed from where a mistake might have been made.

Instead of relying on constraint solving, we draw on the notion of a residual from literature on ordered algebraic structures. Applying these to effect quantales (a large class of sequential effect systems) yields an implementation approach which accepts exactly the same program as an original effect quantale, but for effect-incorrect programs is guaranteed to fail type-checking with predictable error locations tied to evaluation order. We have implemented this idea in a generic effect system implementation framework for Java, and report on experiences applying effect systems from the literature and novel effect systems to Java programs. We find that the reported error locations with our technique are significantly closer to the program points that lead to failed effect checks.
  },
}