Title: On the bright side of type classes: instance arguments in Agda
Authors: Devriese, Dominique ×
Piessens, Frank #
Issue Date: Sep-2011
Publisher: ACM Press
Series Title: ACM SIGPLAN Notices vol:46 issue:9 pages:143-155
Conference: International Conference on Functional Programming edition:16 location:Tokyo, Japan date:19-21 September 2011
Article number: 2034796
Abstract: We present instance arguments: an alternative to type classes and
related features in the dependently typed, purely functional
programming language/proof assistant Agda. They are a new, general
type of function arguments, resolved from call-site scope in a
type-directed way. The mechanism 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 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 standard language mechanisms
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 automatically candidates for instance
resolution. A final novelty of our approach is that existing Agda
libraries using records gain the benefits of type classes without any

We discuss our implementation in Agda (to be part of Agda 2.2.12) 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 corresponding
Haskell code using 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
ISSN: 0362-1340
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
icfp001-Devriese.pdfMain article Published 267KbAdobe PDFView/Open


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

© Web of science