Title: Instance arguments in Agda - An alternative to type classes
Authors: Devriese, Dominique ×
Piessens, Frank #
Issue Date: 2014
Publisher: Kluwer Academic Publishers
Series Title: Higher-order and Symbolic Computation
Abstract: We present instance arguments: an alternative to type classes and related features. Instance arguments are a new, general type of function arguments, resolved at the call-site scope in a type-directed way. The concept is inspired by both Scala's implicits and Agda's existing implicit arguments, but differs from both in important ways. Our mechanism is designed and implemented for the dependently typed, purely functional programming language/proof assistant Agda, but our design choices can be applied to other programming languages as well.

Like Scala's implicits, we do not provide a separate structure for type classes and their instances, but instead rely on Agda's standard dependently typed records, so that we can reuse standard language mechanisms to provide features that are missing or expensive in other proposals. Like Scala, we support the equivalent of local instances. Unlike Scala, functions taking our new arguments are first-class citizens and can be abstracted over and manipulated in standard ways. Compared to other proposals, we avoid the pitfall of introducing a separate type-level computational model through the instance search mechanism. All values in scope are candidates for instance resolution. A final novelty of our approach is that existing Agda libraries using records gain the benefits of instance arguments without any modification.

We discuss our implementation in Agda (part of Agda v2.3.0 onward) and we use monads as an example to show how it allows existing concepts in the Agda standard library to be used in a similar way as Haskell code uses type classes. We also demonstrate and discuss equivalents and alternatives to some advanced type class-related patterns from the literature and some new patterns specific to our system.
ISSN: 1388-3690
Publication status: accepted
KU Leuven publication type: IT
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
tekst.pdfOA article Accepted 422KbAdobe PDFView/Open Request a copy

These files are only available to some KU Leuven Association staff members


All items in Lirias are protected by copyright, with all rights reserved.