Generic level polymorphic n-ary functions
Pages 14 - 26
Abstract
Agda's standard library struggles in various places with n-ary functions and relations. It introduces congruence and substitution operators for functions of arities one and two, and provides users with convenient combinators for manipulating indexed families of arity exactly one.
After a careful analysis of the kinds of problems the unifier can easily solve, we design a unifier-friendly representation of n-ary functions. This allows us to write generic programs acting on n-ary functions which automatically reconstruct the representation of their inputs' types by unification. In particular, we can define fully level polymorphic n-ary versions of congruence, substitution and the combinators for indexed families, all requiring minimal user input.
References
[1]
Andreas Abel and Brigitte Pientka. 2011. Higher-Order Dynamic Pattern Unification for Dependent Types and Records. In Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings (Lecture Notes in Computer Science), C.-H. Luke Ong (Ed.), Vol. 6690. Springer, 10–26.
[2]
Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. 2018. Towards Certified Meta-Programming with Typed Template-Coq. 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 (Lecture Notes in Computer Science), Jeremy Avigad and Assia Mahboubi (Eds.), Vol. 10895. Springer, 20–39.
[3]
Kenichi Asai, Oleg Kiselyov, and Chung-chieh Shan. 2011. Functional un |unparsing. Higher-Order and Symbolic Computation 24, 4 (2011), 311–340.
[4]
Lennart Augustsson. 1998. Cayenne - a Language with Dependent Types. In Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP ’98), Baltimore, Maryland, USA, September 27-29, 1998., Matthias Felleisen, Paul Hudak, and Christian Queinnec (Eds.). ACM, 239–250.
[5]
Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. 2012. Proofs for free - Parametricity for dependent types. J. Funct. Program. 22, 2 (2012), 107–152.
[6]
Nils Anders Danielsson and Ulf Norell. 2008. Parsing Mixfix Operators. In Implementation and Application of Functional Languages -20th International Symposium, IFL 2008, Hatfield, UK, September 10-12, 2008. Revised Selected Papers (Lecture Notes in Computer Science), Sven-Bodo Scholz and Olaf Chitil (Eds.), Vol. 5836. Springer, 80–99.
[7]
Olivier Danvy. 1998. Functional Unparsing. J. Funct. Program. 8, 6 (1998), 621–625. http://journals.cambridge.org/action/ displayAbstract?aid=44189
[8]
Peter Dybjer. 1994. Inductive Families. Formal Asp. Comput. 6, 4 (1994), 440–465.
[9]
Daniel Fridlender and Mia Indrika. 2000. Do we need dependent types? J. Funct. Program. 10, 4 (2000), 409–415.
[10]
Ralf Hinze. 2000. A New Approach to Generic Functional Programming. In POPL 2000, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, January 19-21, 2000, Mark N. Wegman and Thomas W. Reps (Eds.). ACM, 119–132.
[11]
Paul Hudak. 1996. Building Domain-Specific Embedded Languages. ACM Comput. Surv. 28, 4es (1996), 196.
[12]
Per Martin-Löf. 1982. Constructive mathematics and computer programming. Studies in Logic and the Foundations of Mathematics 104 (1982), 153–175.
[13]
Conor McBride. 2002. Faking it: Simulating dependent types in Haskell. J. Funct. Program. 12, 4&5 (2002), 375–392.
[14]
Conor McBride and Ross Paterson. 2008. Applicative programming with effects. J. Funct. Program. 18, 1 (2008), 1–13.
[15]
Ulf Norell. 2008. Dependently Typed Programming in Agda. In Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures (Lecture Notes in Computer Science), Pieter W. M. Koopman, Rinus Plasmeijer, and S. Doaitse Swierstra (Eds.), Vol. 5832. Springer, 230–266.
[16]
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. 2018. The MetaCoq Project. (2018). Unpublished draft, extended version of the ITP18 paper.
[17]
D. A. Turner. 2004. Total Functional Programming. J. UCS 10, 7 (2004), 751–768.
[18]
Wendy Verbruggen, Edsko de Vries, and Arthur Hughes. 2008. Polytypic programming in COQ. In Proceedings of the ACM SIGPLAN Workshop on Genetic Programming, WGP 2008, Victoria, BC, Canada, September 20, 2008, Ralf Hinze and Don Syme (Eds.). ACM, 49–60.
[19]
Stephanie Weirich and Chris Casinghino. 2010. Arity-generic datatypegeneric programming. In Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, PLPV 2010, Madrid, Spain, January 19, 2010, Jean-Christophe Filliâtre and Cormac Flanagan (Eds.). ACM, 15–26.
Recommendations
Arity-generic datatype-generic programming
PLPV '10: Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verificationSome 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. ...
Decidability of conversion for type theory in type theory
Type theory should be able to handle its own meta-theory, both to justify its foundational claims and to obtain a verified implementation. At the core of a type checker for intensional type theory lies an algorithm to check equality of types, or in other ...
Intrinsically typed compilation with nameless labels
To avoid compilation errors it is desirable to verify that a compiler is type correct—i.e., given well-typed source code, it always outputs well-typed target code. This can be done intrinsically by implementing it as a function in a dependently typed ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2019 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 18 August 2019
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Conference
ICFP '19
Sponsor:
ICFP '19: ACM SIGPLAN International Conference on Functional Programming
August 18, 2019
Berlin, Germany
Upcoming Conference
ICFP '25
- Sponsor:
- sigplan
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 142Total Downloads
- Downloads (Last 12 months)11
- Downloads (Last 6 weeks)4
Reflects downloads up to 27 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in