Arity-generic datatype-generic programming
Arity-generic datatype-generic programming
复制标题
Arity-通用数据类型-通用编程
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Chris Casinghino
中科院分区：
文献类型：
--
作者：
Stephanie Weirich;Chris Casinghino
有些程序是双重通用的。例如，map是数据类型通用的，因为许多不同的数据结构支持映射操作。像Generic Haskell这样的泛型编程语言可以使用单个定义来为每种类型生成map。然而，map也是arity泛型的，因为它属于一系列相关的操作，这些操作的参数数量不同。对于列表，这个家族包括repeat，map，zipWith，zipWith3，zipWith4等。通过依赖类型或巧妙的编程，可以将所有这些函数统一在一个定义中。
然而，没有人探索这两种形式的泛型的组合。这两个轴不是正交的，因为arity的概念出现在Generic Haskell中：repeat、map和zipWith的数据类型泛型版本具有不同的类索引类型arity。在本文中，我们定义arity通用的数据类型通用的程序，通过建立一个框架，通用的Haskell风格的泛型编程的依赖类型的编程语言Agda 2。
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 repeat, map, zipWith, zipWith3, zipWith4, etc. With dependent types or clever programming, one can unify all of these functions together in a single definition.
However, no one has explored the combination of these two forms of genericity. These two axes are not orthogonal because the idea of arity appears in Generic Haskell: datatype-generic versions of repeat, map and zipWith have different arities of kind-indexed types. In this paper, we define arity-generic datatype-generic programs by building a framework for Generic Haskell-style generic programming in the dependently-typed programming language Agda 2.