On the bright side of type classes

We present instance arguments: an alternative to type classes andrelated features in the dependently typed, purely functionalprogramming language/proof assistant Agda. They are a new, generaltype of function arguments, resolved from call-site scope in atype-directed way. The mechanism is inspired by both Scala's implicitsand Agda's existing implicit arguments, but differs from both inimportant ways. Our mechanism is designed and implemented for Agda,but our design choices can be applied to other programming languagesas well.Like Scala's implicits, we do not provide a separate structure fortype classes and their instances, but instead rely on Agda's standarddependently typed records, so that standard language mechanismsprovide features that are missing or expensive in other proposals.Like Scala, we support the equivalent of local instances. UnlikeScala, functions taking our new arguments are first-class citizens andcan be abstracted over and manipulated in standard ways. Compared toother proposals, we avoid the pitfall of introducing a separatetype-level computational model through the instance search mechanism.All values in scope are automatically candidates for instanceresolution. A final novelty of our approach is that existing Agdalibraries using records gain the benefits of type classes without anymodification.We discuss our implementation in Agda (to be part of Agda 2.2.12) andwe use monads as an example to show how it allows existing concepts inthe Agda standard library to be used in a similar way as correspondingHaskell code using type classes. We also demonstrate and discussequivalents and alternatives to some advanced type class-relatedpatterns from the literature and some new patterns specific to oursystem.status: publishe