Generic and Indexed Programming
Generic and Indexed Programming
复制标题
通用和索引编程
DOI：
10.1007/978-3-642-32202-0
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
J. Gibbons
中科院分区：
文献类型：
--
作者：
J. Gibbons
泛型编程是通过特殊的参数化使程序更广泛地适用——不仅仅是值或类型的维度，还包括数据的形状、代数结构、策略、计算范式等。索引编程是依赖类型编程的一种轻量级形式，通过允许声明和检查参数之间的关系来限制灵活性：两个参数的形状是否一致，编码值是否匹配某种类型，沿着通道传输的值是否符合所声明的协议，等等。通用性和索引性这两种力量很好地相互平衡，同时促进和控制通用性。牛津大学的通用和索引编程项目是由英国工程和物理科学研究委员会在2006-2010年期间资助的，目的是探索这两种力量之间的相互作用。项目的收尾活动采取了a的形式
Generic programming is about making programs more widely applicable via exotic kinds of parametrization—not just along the dimensions of values or of types, but also of things such as the shape of data, algebraic structures, strategies, computational paradigms, and so on. Indexed programming is a lightweight form of dependently typed programming, constraining flexibility by allowing one to state and check relationships between parameters: that the shapes of two arguments agree, that an encoded value matches some type, that values transmitted along a channel conform to the stated protocol, and so on. The two forces of genericity and indexing balance each other nicely, simultaneously promoting and controlling generality. The Generic and Indexed Programming project at Oxford was funded by the UK Engineering and Physical Sciences Research Council over the period 2006–2010 to explore the interaction between these two forces. The closing activity of the project took the form of a