Syntactic Implicit Parameters with Static Overloading

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 programmer's 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 expressive 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.

val base = 10 in show-int(42) elaborates to val base = 10 in show-int(42,base) which evaluates to "42". We see this elaboration as well in the show-int function itself where the expression show-int(x / base) elaborates to show-int(x / base,base) where it passes the implicit parameter base again to the recursive call.

This view of implicit parameters as a form of dynamic binding (but with a static declaration!) is quite straightforward and seems almost too simple to be of much use. However, it turns out to be quite expressive in combination with static overloading. This brings us to the second idea, where we define static overloading purely as a form of automatic qualification:

Static overloading elaborates plain names to fully qualified names based on the local type context.

The essence of this idea was first described by Leijen and Ye [2025] as an application of type inference under a prefix. First, we allow functions to be declared with qualified names, for example: fun int/show( x : int ) : string show-int(x,10) fun float/show( f : float64 ) : string show-float(f)

(where int/ and float/ can be arbitrary "module" names). Of course, such qualified names already occur naturally as well in most languages when different modules are imported that export the same (unqualified) name. We now allow the programmer to write an unqualified show and have it be resolved to either definition based on the local type context. For example show(1) is elaborated to the fully qualified int/show(1) based on the (static) type of the argument. This is already quite convenient in practice, and is again a simple mechanism that is straightforward to implementfor example the C language implements this form of static overloading for many common math operations. However, static overloading by itself is quite limited as it does not allow for abstraction.

For example, consider a show function for lists: fun list/show( xs : list<a> ) : string match xs Cons(x,xx) -> show(x) ++ "::" ++ list/show(xx) // rejected Nil -> "[]"

This is rejected since we cannot at this point statically resolve which show function is required for the show(x) expression (as the type of the list elements is polymorphic). Here is where we can now use our new syntactic implicit parameters to delay resolving which particular show to use:

fun list/show( xs : list<a>, ?show : a -> string ) : string match xs Cons(x,xx) -> show(x) ++ "::" ++ list/show(xx) Nil -> "[]"