Generic Programming with Dependent Types
| Autor: | Chris Casinghino, Stephanie Weirich |
|---|---|
| Rok vydání: | 2012 |
| Předmět: |
Parametric polymorphism
Functional programming Generic programming Theoretical computer science Functional logic programming Computer science Programming language Agda computer.software_genre TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Haskell Generalized algebraic data type computer Declarative programming computer.programming_language |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783642322013 SSGIP |
| DOI: | 10.1007/978-3-642-32202-0_5 |
| Popis: | Some programs are doubly generic. For example, map is datatype-generic in that many different data structures support a mapping operation. A generic programming language like Generic Haskell can use a single definition to generate map for each type. However, map is also arity-generic because it belongs to a family of related operations that differ in the number of arguments. For lists, this family includes familiar functions from the Haskell standard library (such as repeat, map, and zipWith). This tutorial explores these forms of genericity individually and together. These two axes are not orthogonal: datatype-generic versions of repeat, map and zipWith have different arities of kind-indexed types. We explore these forms of genericity in the context of the Agda programming language, using the expressiveness of dependent types to capture both forms of genericity in a common framework. Therefore, this tutorial serves as an introduction to dependently typed languages as well as generic programming. The target audience of this work is someone who is familiar with functional programming languages, such as Haskell or ML, but would like to learn about dependently typed languages. We do not assume prior experience with Agda, type- or arity-generic programming. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|