检索结果-内蒙古大学图书馆

datatype-generic programming Meets Elaborator Reflection

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2022年第ICFP期6卷 225–253页

作者： Ko, Hsiang-Shang Chen, Liang-Ting Lin, Tzu-Chi Acad Sinica Inst Informat Sci 128 Acad RdSect 2 Taipei 115201 Taiwan

datatype-generic programming is natural and useful in dependently typed languages such as Agda. However, datatype-generic libraries in Agda are not reused as much as they should be, because traditionally they work only on datatypes decoded from a library's own version of datatype descriptions;this means that different generic libraries cannot be used together, and they do not work on native datatypes, which are preferred by the practical Agda programmer for better language support and access to other libraries. Based on elaborator reflection, we present a framework in Agda featuring a set of general metaprograms for instantiating datatype-generic programs as, and for, a useful range of native datatypes and functions - including universe-polymorphic ones - in programmer-friendly and customisable forms. We expect that datatype-generic libraries built with our framework will be more attractive to the practical Agda programmer. As the elaborator reflection features used by our framework become more widespread, our design can be ported to other languages too.

关键词： datatype-generic programming dependently typed programming inductive families universe polymorphism elaborator reflection metaprogramming

来源：评论

学校读者我要写书评

暂无评论

System F-omega with Equirecursive Types for datatype-generic programming 16

System F-omega with Equirecursive Types for Datatype-Generic...

引用

43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of programming Languages (POPL)

作者： Cai, Yufei Giarrusso, Paolo G. Ostermann, Klaus Univ Tubingen Tubingen Germany

ISBN: (纸本)9781450335492

Traversing an algebraic datatype by hand requires boilerplate code which duplicates the structure of the datatype. datatype-generic programming (DGP) aims to eliminate such boilerplate code by decomposing algebraic datatypes into type constructor applications from which generic traversals can be synthesized. However, different traversals require different decompositions, which yield isomorphic but unequal types. This hinders the interoperability of different DGP techniques. In this paper, we propose F-omega(mu), an extension of the higher-order polymorphic lambda calculus F-omega with records, variants, and equirecursive types. We prove the soundness of the type system, and show that type checking for first-order recursive types is decidable with a practical type checking algorithm. In our soundness proof we define type equality by interpreting types as infinitary lambda-terms (in particular, Berarducci-trees). To decide type equality we beta-normalize types, and then use an extension of equivalence checking for usual equirecursive types. Thanks to equirecursive types, new decompositions for a datatype can be added modularly and still inter-operate with each other, allowing multiple DGP techniques to work together. We sketch how generic traversals can be synthesized, and apply these components to some examples. Since the set of datatype decomposition becomes extensible, System F-omega(mu) enables using DGP techniques incrementally, instead of planning for them up-front or doing invasive refactoring.

关键词： datatype-generic programming equirecursive types functors

来源：评论

学校读者我要写书评

暂无评论

System F-omega with Equirecursive Types for datatype-generic programming

引用

ACM SIGPLAN NOTICES 2016年第1期51卷 30-43页

作者： Cai, Yufei Giarrusso, Paolo G. Ostermann, Klaus Univ Tubingen Tubingen Germany

关键词： datatype-generic programming equirecursive types functors

来源：评论

学校读者我要写书评

暂无评论

Comparing Libraries for generic programming in Haskell

Comparing Libraries for Generic Programming in Haskell

引用

1st ACM SIGPLAN Haskell Symposium

作者： Rodriguez, Alexey Jeuring, Johan Jansson, Patrik Gerdes, Alex Kiselyov, Oleg Oliveira, Bruno C. D. S. Univ Utrecht NL-3508 TC Utrecht Netherlands Chalmers Univ Technol Gothenburg Sweden Univ Gothenburg Gothenburg Sweden Univ Oxford Oxford OX1 2JD England

ISBN: (纸本)9781605580647

datatype-generic programming is defining functions that depend on the structure, or "shape", of datatypes. It has been around for more than 10 years, and a lot of progress has been made, in particular in the lazy functional programming language Haskell. There are more than 10 proposals for generic programming libraries or language extensions for Haskell. To compare and characterise the many generic programming libraries in a typed functional language, we introduce a set of criteria and develop a generic programming benchmark: a set of characteristic examples testing various facets of datatype-generic programming. We have implemented the benchmark for nine existing Haskell generic programming libraries and present the evaluation of the libraries. The comparison is useful for reaching a common standard for generic programming, but also for a programmer who has to choose a particular approach for datatype-generic programming.

关键词： Design Measurement datatype-generic programming libraries comparison

来源：评论

学校读者我要写书评

暂无评论

Typed Syntactic Meta-programming 13

Typed Syntactic Meta-programming

引用

18th ACM SIGPLAN International Conference on Functional programming

作者： Devriese, Dominique Piessens, Frank Katholieke Univ Leuven iMinds DistriNet Louvain Belgium

ISBN: (纸本)9781450323260

We present a novel set of meta-programming primitives for use in a dependently-typed functional language. The types of our meta-programs provide strong and precise guarantees about their termination, correctness and completeness. Our system supports typesafe construction and analysis of terms, types and typing contexts. Unlike alternative approaches, they are written in the same style as normal programs and use the language's standard functional computational model. We formalise the new meta-programming primitives, implement them as an extension of Agda, and provide evidence of usefulness by means of two compelling applications in the fields of datatype-generic programming and proof tactics.

关键词： meta-programming dependent types datatype-generic programming tactics

来源：评论

学校读者我要写书评

暂无评论

The right kind of generic programming

The right kind of generic programming

引用

8th ACM SIGPLAN Workshop on generic programming, WGP 2012

作者： Magalhães, José Pedro Department of Computer Science University of Oxford United Kingdom

ISBN: (纸本)9781450315760

Haskell is known for its strong, static type system. A good type system classifies values, constraining the valid terms of the language and preventing many common programming errors. The Glasgow Haskell Compiler (GHC) has further extended the type language of Haskell, adding support for type-level computation and explicit type equality constraints. Type-level programming is used to classify values, but types themselves have remained notoriously unclassified. Recently, however, the kind-level language was extended with support for user-defined kinds and kind polymorphism. In this paper we revisit generic programming approaches that rely heavily on type-level computation, and analyse how to improve them with the extended kind language. For instructive purposes, we list a series of advantages given by the new features, and also a number of shortcomings that prevent desirable use patterns. © 2012 ACM.

关键词： agda datakinds datatype-generic programming haskell kind polymorphism

来源：评论

学校读者我要写书评

暂无评论

Optimizing SYB traversals is easy!

引用

SCIENCE OF COMPUTER programming 2015年第Part2期112卷 170-193页

作者： Adams, Michael D. Farmer, Andrew Magalhaes, Jose Pedro Univ Utah Sch Comp Salt Lake City UT 84112 USA Univ Illinois Dept Comp Sci Urbana IL 61801 USA Univ Kansas Informat & Telecommun Technol Ctr Lawrence KS 66045 USA Univ Oxford Dept Comp Sci Oxford OX1 2JD England

The most widely used generic-programming system in the Haskell community, Scrap Your Boilerplate (SYB), also happens to be one of the slowest. generic traversals in SYB are often an order of magnitude slower than equivalent handwritten, non-generic traversals. Thus while SYB allows the concise expression of many traversals, its use incurs a significant runtime cost. Existing techniques for optimizing other generic-programming systems are not able to eliminate this overhead. This paper presents an optimization that eliminates this cost. Essentially, it is a partial evaluation that takes advantage of domain-specific knowledge about the structure of SYB. It optimizes SYB traversals to be as fast as handwritten, non-generic code, and benchmarks show that this optimization improves the speed of SYB traversals by an order of magnitude or more. (C) 2015 Published by Elsevier B.V.

关键词： Optimization Partial evaluation datatype-generic programming Haskell Scrap Your Boilerplate (SYB)

来源：评论

学校读者我要写书评

暂无评论

Incremental computing with data structures

引用

SCIENCE OF COMPUTER programming 2018年 164卷 18-36页

作者： Morihata, Akimasa Univ Tokyo Grad Sch Arts & Sci Tokyo Japan

Incremental computing is a method of maintaining consistency between an input and output. If only a small portion of the input is modified, it is natural to expect that the corresponding output can be obtained more efficiently than full re-computation. However, for nontrivial data structures, such as self-balancing binary search trees, even the most primitive modifications may lead to drastic change of the underlying structure. In this paper, we develop an method of incremental computing on data structures that may consist of complex modifications. The key idea is to use shortcut fusion in order to decompose a complex modification to a series of simple ones. Based on this idea, we extend Jeuring's incremental computing method on algebraic data structures to one on more complex data structures. The method is purely functional and does not rely on any run-time support. Its correctness is straightforward from parametricity. Moreover, its cost is often proportional to that of the corresponding modification. (C) 2017 Elsevier B.V. All rights reserved.

关键词： Data structures datatype-generic programming Incremental computing Shortcut fusion

来源：评论

学校读者我要写书评

暂无评论

Combinators and type-driven transformers in Objective Caml

引用

SCIENCE OF COMPUTER programming 2015年 114卷 57-73页

作者： Boulytchev, Dmitry St Petersburg State Univ St Petersburg 198504 Russia

We describe an implementation of LDTA 2011 Tool Challenge tasks in Objective Caml language. Instead of using some dedicated domain-specific tools we utilize typical functional programming machinery such as polymorphic functions, monads and combinators;in addition we extensively use an idiom of type-driven transformers, which can be considered as a form of datatype-generic programming. Our implementation provides a good example of utilization of Objective Caml specific features such as open and implicitly defined types. As a result we provide a highly modular implementation built up of separately compiled components combined in a type-safe manner. (C) 2015 Elsevier B.V. All rights reserved.

关键词： Compilers Functional programming datatype-generic programming Combinators Modularization and code reuse

来源：评论

学校读者我要写书评

暂无评论

Typed Syntactic Meta-programming

引用

ACM SIGPLAN NOTICES 2013年第9期48卷 73-85页

作者： Devriese, Dominique Piessens, Frank Katholieke Univ Leuven iMinds DistriNet Louvain Belgium

关键词： meta-programming dependent types datatype-generic programming tactics

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：