< Back to previous page

Publication

Coherent Implicit Resolution

Book - Dissertation

In programming languages, type-directed resolution is a mechanism that automatically composes expressions using type information. On the one hand, resolution enables a variety of powerful implicit programming features, such as type classes in Haskell, implicits in Scala and traits in Rust. These features allow expressions to be omitted by the programmer and implicitly inferred through resolution, making programs more compact and easier to read. On the other hand, it may introduce semantical ambiguity in the language and break equational reasoning over programs of the language, if not carefully designed. Fortunately, posing appropriate restrictions on the resolution mechanism can save it from unpredictable and counterintuitive behaviour. These restrictions vary with the design of the mechanism, resulting in different, but correct, implicit programming features. The correctness of resolution is formally stated via two properties: coherence, which ensures semantical unambiguity, and stability, which ensures equational reasoning. This research targets techniques for reasoning about calculi that support implicit programming, a task that becomes harder in the presence of such features, and for delivering those calculi together with a verification of their correct behaviour. Furthermore, it identifies points that call for care in the design and in the implementation of type-directed resolution.
Publication year:2021
Accessibility:Open