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 onl...
详细信息
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.
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 da...
详细信息
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.
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 da...
详细信息
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 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...
详细信息
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 genericprogramming libraries or language extensions for Haskell. To compare and characterise the many genericprogramming libraries in a typed functional language, we introduce a set of criteria and develop a genericprogramming benchmark: a set of characteristic examples testing various facets of datatype-generic programming. We have implemented the benchmark for nine existing Haskell genericprogramming libraries and present the evaluation of the libraries. The comparison is useful for reaching a common standard for genericprogramming, but also for a programmer who has to choose a particular approach for datatype-generic programming.
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 c...
详细信息
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.
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)...
详细信息
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 equi...
详细信息
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.
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 ef...
详细信息
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.
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...
详细信息
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.
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 c...
详细信息
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.
暂无评论