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.