Syntactic Implicit Parameters with Static Overloading (Extended Version)

Implicits provide a powerful mechanism for term-based inference, where “obvious” arguments can be omitted and inferred by the type checker. This can greatly reduce the programmers burden and improve the clarity of expression. As such, many languages support a form of implicits in practice, such as type classes in Haskell or Lean, or implicits in Scala. Unfortunately, many of these systems have become increasingly complex and often require significant implementation effort.

In this paper we take a fresh look at the design space with an arguably simpler approach based on two orthogonal features: _syntactic implicit parameters_ and _static overloading_. Each of these features is limited in scope and has a straightforward implementation. Taken together though, they are surprisingly expresive and we believe they can cover many of the common usage scenarios of implicits in practice.

We formalize our system and provide various examples, and prove our elaboration is coherent. We also give an inference algorithm and show it is sound and complete. Our system is fully implemented in the Koka language, and we describe our experience with these features at scale, and discuss further extensions.