Abstract
Most statically typed functional programming languages allow programmers to write partial functions: functions that are not defined on all the elements of their domain as specified by their type. Applying a partial function to a value on which it is not defined will raise a run-time exception, thus in practice well-typed programs can and do still go wrong.
To warn programmers about such errors, contemporary compilers for functional languages employ a local and purely syntactic analysis to detect partial case-expressions--those that do not cover all possible patterns of constructors. As programs often maintain invariants on their data, restricting the potential values of the scrutinee to a subtype of its given or inferred type, many of these incomplete case-expressions are harmless. Such an analysis does not account for these invariants and will thus report many false positives, overwhelming the programmer.
We develop a constraint-based type system that detects harmful sources of partiality and prove it correct with respect to an imprecise exception semantics. The analysis accurately tracks the flow of both exceptions--the manifestation of partiality gone wrong--and ordinary data through the program, as well as the dependencies between them. The latter is crucial for usable precision, but has been omitted from previously published exception analyses.
To warn programmers about such errors, contemporary compilers for functional languages employ a local and purely syntactic analysis to detect partial case-expressions--those that do not cover all possible patterns of constructors. As programs often maintain invariants on their data, restricting the potential values of the scrutinee to a subtype of its given or inferred type, many of these incomplete case-expressions are harmless. Such an analysis does not account for these invariants and will thus report many false positives, overwhelming the programmer.
We develop a constraint-based type system that detects harmful sources of partiality and prove it correct with respect to an imprecise exception semantics. The analysis accurately tracks the flow of both exceptions--the manifestation of partiality gone wrong--and ordinary data through the program, as well as the dependencies between them. The latter is crucial for usable precision, but has been omitted from previously published exception analyses.
| Original language | English |
|---|---|
| Title of host publication | PEPM '15: Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation (PEPM 2015) |
| Publisher | Association for Computing Machinery |
| Pages | 127-138 |
| Number of pages | 12 |
| ISBN (Print) | 978-1-4503-3297-2 |
| DOIs | |
| Publication status | Published - 13 Jan 2015 |
Keywords
- type-based program analysis
- exception analysis
- imprecise exceptions
- pattern-matching