On the bright side of type classes
- 19 September 2011
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 16th ACM SIGPLAN international conference on Functional programming
- Vol. 46 (9), 143-155
- https://doi.org/10.1145/2034773.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 modification. 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 system.status: publisheKeywords
This publication has 17 references indexed in Scilit:
- Haskell Type Constraints UnleashedLecture Notes in Computer Science, 2010
- First-Class Type ClassesLecture Notes in Computer Science, 2008
- Canonical Big OperatorsLecture Notes in Computer Science, 2008
- A history of HaskellPublished by Association for Computing Machinery (ACM) ,2007
- Practical type inference for arbitrary-rank typesJournal of Functional Programming, 2007
- RepLibPublished by Association for Computing Machinery (ACM) ,2006
- Simple unification-based type inference for GADTsPublished by Association for Computing Machinery (ACM) ,2006
- Scrap your boilerplate with classPublished by Association for Computing Machinery (ACM) ,2005
- Faking it Simulating dependent types in HaskellJournal of Functional Programming, 2002
- Type-checking multi-parameter type classesJournal of Functional Programming, 2002