System $F^ω$ with Coherent Implicit Resolution

TL;DR

The paper tackles coherence and completeness challenges in implicit resolution for polymorphic, higher-kinded systems by proposing a declarative extension of System $F^\omega$ to implicit parameters, denoted $F^\omega_{CCI}$, featuring contextual abstractions and a unified treatment of type and term abstractions. A core contribution is the declarative resolution judgment $\Gamma \Vdash \tau \leadsto \tau'$ and a least-depth, unambiguous resolution strategy, underpinned by a rich set of rules and supported by a Coq mechanization to establish coherence; an algorithmic, terminating formulation is left for ongoing work. The framework supports first-class, locally scoped, overlapping, and higher-order given instances, including higher-kinded types, while triggering implicit resolution only at explicit ascriptions to preserve syntax-directedness. This work provides a principled foundation for coherent implicit programming with strong theoretical guarantees and a path toward practical implementations.

Abstract

We propose a calculus for modeling implicit programming that supports first-class, overlapping, locally scoped, and higher-order instances with higher-kinded types. We propose a straightforward generalization of the well-established System $F^ω$ to implicit parameters, with a uniform treatment of type and term abstractions. Unlike previous works, we give a declarative specification of unambiguous, and thus coherent, resolution without introducing restrictions motivated by an algorithmic formulation of resolution.