journal article
Open Access
Jul 30, 2018
Generic zero-cost reuse for dependent types
Proceedings of the ACM on Programming Languages
Vol. 2
No. ICFP
pp. 1-30
·
Association for Computing Machinery (ACM)
Abstract
Dependently typed languages are well known for having a problem with code reuse. Traditional non-indexed algebraic datatypes (e.g. lists) appear alongside a plethora of indexed variations (e.g. vectors). Functions are often rewritten for both non-indexed and indexed versions of essentially the same datatype, which is a source of code duplication.
We work in a Curry-style dependent type theory, where the same untyped term may be classified as both the non-indexed and indexed versions of a datatype. Many solutions have been proposed for the problem of dependently typed reuse, but we exploit Curry-style type theory in our solution to not only reuse data and programs, but do so at zero-cost (without a runtime penalty). Our work is an exercise in dependently typed generic programming, and internalizes the process of zero-cost reuse as the identity function in a Curry-style theory.
We work in a Curry-style dependent type theory, where the same untyped term may be classified as both the non-indexed and indexed versions of a datatype. Many solutions have been proposed for the problem of dependently typed reuse, but we exploit Curry-style type theory in our solution to not only reuse data and programs, but do so at zero-cost (without a runtime penalty). Our work is an exercise in dependently typed generic programming, and internalizes the process of zero-cost reuse as the identity function in a Curry-style theory.
Topics
No keywords indexed for this article. Browse by subject →
References
24
[1]
Bruno Barras and Bruno Bernardo . 2008. The implicit calculus of constructions as a programming language with dependent types. Foundations of Software Science and Computational Structures ( 2008 ), 365–379. Bruno Barras and Bruno Bernardo. 2008. The implicit calculus of constructions as a programming language with dependent types. Foundations of Software Science and Computational Structures (2008), 365–379.
[7]
Pierre-Evariste Dagand , Nicolas Tabareau , and Éric Tanter . 2018. Foundations of dependent interoperability. Journal of Functional Programming 28 ( 2018 ). Pierre-Evariste Dagand, Nicolas Tabareau, and Éric Tanter. 2018. Foundations of dependent interoperability. Journal of Functional Programming 28 (2018).
[9]
Larry Diehl and Aaron Stump . 2018. Zero-Cost Coercions for Program and Proof Reuse. (2018). arXiv : 1802 .00787 Larry Diehl and Aaron Stump. 2018. Zero-Cost Coercions for Program and Proof Reuse. (2018). arXiv: 1802.00787
[10]
Denis Firsov , Richard Blair , and Aaron Stump . 2018 . Efficient Mendler-Style Lambda-Encodings in Cedille. In Interactive Theorem Proving - 9th International Conference , ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. 235–252 . Denis Firsov, Richard Blair, and Aaron Stump. 2018. Efficient Mendler-Style Lambda-Encodings in Cedille. In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. 235–252.
[11]
[12]
Matthew Flatt and PLT. 2010 . Reference: Racket. Technical Report PLT-TR-2010-1 . PLT Design Inc . https://racket-lang.org/tr1/ . Matthew Flatt and PLT. 2010. Reference: Racket. Technical Report PLT-TR-2010-1. PLT Design Inc. https://racket-lang.org/tr1/ .
[13]
Herman Geuvers. 2001. Induction Is Not Derivable in Second Order Dependent Type Theory. In Typed Lambda Calculi and Applications (TLCA). 166–181. Herman Geuvers. 2001. Induction Is Not Derivable in Second Order Dependent Type Theory. In Typed Lambda Calculi and Applications (TLCA). 166–181.
10.1007/3-540-45413-6_16
[15]
Alexei Kopylov . 2003 . Dependent Intersection: A New Way of Defining Records in Type Theory. In 18th IEEE Symposium on Logic in Computer Science (LICS). 86–95 . Alexei Kopylov. 2003. Dependent Intersection: A New Way of Defining Records in Type Theory. In 18th IEEE Symposium on Logic in Computer Science (LICS). 86–95.
[16]
Conor McBride. 2011. Ornamental algebras algebraic ornaments. (2011). Conor McBride. 2011. Ornamental algebras algebraic ornaments. (2011).
[18]
Alexandre Miquel. 2001. The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping. In Typed Lambda Calculi and Applications (TLCA) Samson Abramsky (Ed.). 344–359. Alexandre Miquel. 2001. The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping. In Typed Lambda Calculi and Applications (TLCA) Samson Abramsky (Ed.). 344–359.
10.1007/3-540-45413-6_27
[19]
Ulf Norell . 2008. Dependently typed programming in Agda . In International School on Advanced Functional Programming . Springer , 230–266. Ulf Norell. 2008. Dependently typed programming in Agda. In International School on Advanced Functional Programming. Springer, 230–266.
[21]
Aaron Stump . 2018a. From Realizability to Induction via Dependent Intersection. Ann. Pure Appl. Logic ( 2018 ). to appear. Aaron Stump. 2018a. From Realizability to Induction via Dependent Intersection. Ann. Pure Appl. Logic (2018). to appear.
[22]
Aaron Stump . 2018b. Syntax and Semantics of Cedille. (2018). arXiv : 1806 .04709 Aaron Stump. 2018b. Syntax and Semantics of Cedille. (2018). arXiv: 1806.04709
[23]
The Coq Development Team. 2008. The Coq Proof Assistant Reference Manual. http://coq.inria.fr The Coq Development Team. 2008. The Coq Proof Assistant Reference Manual. http://coq.inria.fr
Metrics
8
Citations
24
References
Details
- Published
- Jul 30, 2018
- Vol/Issue
- 2(ICFP)
- Pages
- 1-30
- License
- View
Authors
Funding
National Science Foundation
Award: 1524519
U.S. Department of Defense
Award: FA9550-16-1-0082
Cite This Article
Larry Diehl, Denis Firsov, Aaron Stump (2018). Generic zero-cost reuse for dependent types. Proceedings of the ACM on Programming Languages, 2(ICFP), 1-30. https://doi.org/10.1145/3236799
Related
You May Also Like
code2vec: learning distributed representations of code
Uri Alon, Meital Zilberstein · 2019
880 citations
Grounded Copilot: How Programmers Interact with Code-Generating Models
Shraddha Barke, Michael B. James · 2023
275 citations