A simpler encoding of indexed types
Pages 14 - 22
Abstract
In functional programming languages, generalized algebraic data types (GADTs) are very useful as the unnecessary pattern matching over them can be ruled out by the failure of unification of type arguments. In dependent type systems, this is usually called indexed types and it’s particularly useful as the identity type is a special case of it. However, pattern matching over indexed types is very complicated as it requires term unification in general. We study a simplified version of indexed types (called simpler indexed types) where we explicitly specify the selection process of constructors, and we discuss its expressiveness, limitations, and properties.
References
[1]
Guillaume Allais, James Chapman, Conor McBride, and James McKinna. 2017. Type-and-Scope Safe Programs and Their Proofs. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017). Association for Computing Machinery, New York, NY, USA. 195–207. isbn:9781450347051 https://doi.org/10.1145/3018610.3018613
[2]
Lennart Augustsson and Kent Petersson. 1994. Silly Type Families DRAFT.
[3]
Aya developers. 2021. The Aya Proof Assistant. https://github.com/aya-prover/aya-dev
[4]
Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 23 (2013), 9, 552–593. issn:1469-7653 https://doi.org/10.1017/S095679681300018X
[5]
Edwin Brady, Conor McBride, and James McKinna. 2004. Inductive Families Need Not Store Their Indices. In Types for Proofs and Programs, Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 115–129. isbn:978-3-540-24849-1
[6]
Evan Cavallo and Robert Harper. 2019. Higher Inductive Types in Cubical Computational Type Theory. Proc. ACM Program. Lang., 3, POPL (2019), Article 1, Jan., 27 pages. https://doi.org/10.1145/3290314
[7]
James Chapman, Pierre-Évariste Dagand, Conor McBride, and Peter Morris. 2010. The Gentle Art of Levitation. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP ’10). Association for Computing Machinery, New York, NY, USA. 3–14. isbn:9781605587943 https://doi.org/10.1145/1863543.1863547
[8]
James Cheney and Ralf Hinze. 2003. First-class phantom types. Cornell University.
[9]
Jesper Cockx and Andreas Abel. 2018. Elaborating Dependent (Co)Pattern Matching. Proc. ACM Program. Lang., 2, ICFP (2018), Article 75, July, 30 pages. https://doi.org/10.1145/3236770
[10]
Jesper Cockx, Dominique Devriese, and Frank Piessens. 2014. Pattern Matching without K. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP ’14). Association for Computing Machinery, New York, NY, USA. 257–268. isbn:9781450328739 https://doi.org/10.1145/2628136.2628139
[11]
Jesper Cockx, Dominique Devriese, and Frank Piessens. 2016. Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016). Association for Computing Machinery, New York, NY, USA. 270–283. isbn:9781450342193 https://doi.org/10.1145/2951913.2951917
[12]
Jesper Cockx, Gaëtan Gilbert, and Nicolas Tabareau. 2018. Vectors are records, too. TYPES 2018.
[13]
Jesper Cockx, Frank Piessens, and Dominique Devriese. 2014. Overlapping and Order-Independent Patterns. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 87–106. isbn:978-3-642-54833-8
[14]
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2015. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. FLAP, 4 (2015), 3127–3170.
[15]
Thierry Coquand. 1992. Pattern matching with dependent types. In Proceedings of the Workshop on Types for Proofs and Programs. 71–83.
[16]
Pierre-Évariste Dagand and Conor McBride. 2014. Transporting functions across ornaments. Journal of Functional Programming, 24, 2-3 (2014), 316–383. https://doi.org/10.1017/S0956796814000069
[17]
Peter Dybjer. 2003. A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. Journal of Symbolic Logic, 65 (2003), 06, https://doi.org/10.2307/2586554
[18]
Fredrik Nordvall Forsberg and Anton Setzer. 2010. Inductive-inductive definitions. In International Workshop on Computer Science Logic. 454–468.
[19]
Healfdene Goguen, Conor McBride, and James McKinna. 2006. Eliminating Dependent Pattern Matching. Springer Berlin Heidelberg, Berlin, Heidelberg. 521–540. isbn:978-3-540-35464-2 https://doi.org/10.1007/11780274_27
[20]
Group for Dependent Types and HoTT. 2015. The Arend Proof Assistant. https://arend-lang.github.io
[21]
Kaveh (https://mathoverflow.net/users/7507/kaveh). 2018. History of the notation for substitution. MathOverflow. https://mathoverflow.net/q/243084
[22]
HsiangShang Ko and Jeremy Gibbons. 2016. Programming with ornaments. Journal of Functional Programming, 27 (2016), e2. https://doi.org/10.1017/S0956796816000307
[23]
Per Martin-Löf. 1975. An intuitionistic theory of types: predicative part. In Logic Colloquium ’73, Proceedings of the Logic Colloquium, H.E. Rose and J.C. Shepherdson (Eds.) (Studies in Logic and the Foundations of Mathematics, Vol. 80). North-Holland, 73–118.
[24]
Ulf Norell. 2009. Dependently Typed Programming in Agda. In Proceedings of the 4th International Workshop on Types in Language Design and Implementation (TLDI ’09). ACM, New York, NY, USA. 1–2. isbn:978-1-60558-420-1 https://doi.org/10.1145/1481861.1481862
[25]
Tim Sheard and Emir Pasalic. 2008. Meta-programming With Built-in Type Equality. Electronic Notes in Theoretical Computer Science, 199 (2008), 49–65. issn:1571-0661 https://doi.org/10.1016/j.entcs.2007.11.012 Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages (LFM 2004).
[26]
The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book Institute for Advanced Study.
[27]
Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2019. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. Proc. ACM Program. Lang., 3, ICFP (2019), Article 87, July, 29 pages. https://doi.org/10.1145/3341691
[28]
Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2020. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. Preprint available at https://staff.math.su.se/anders.mortberg/papers/cubicalagda2.pdf
[29]
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. 2006. Simple unification-based type inference for GADTs. In International Conference on Functional Programming (ICFP’06). https://www.microsoft.com/en-us/research/publication/simple-unification-based-type-inference-for-gadts/ 2016 ACM SIGPLAN Most Influential ICFP Paper Award.
[30]
Hongwei Xi, Chiyan Chen, and Gang Chen. 2003. Guarded Recursive Datatype Constructors. In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’03). Association for Computing Machinery, New York, NY, USA. 224–235. isbn:1581136285 https://doi.org/10.1145/604131.604150
[31]
Christoph Zenger. 1997. Indexed Types. Theor. Comput. Sci., 187, 1–2 (1997), Nov., 147–165. issn:0304-3975 https://doi.org/10.1016/S0304-3975(97)00062-5
Index Terms
- A simpler encoding of indexed types
Recommendations
Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types
Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its applicability to a variety of type systems, its error reporting, and its ease of implementation. Following principles from ...
Generalized algebraic data types and object-oriented programming
OOPSLA '05: Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applicationsGeneralized algebraic data types (GADTs) have received much attention recently in the functional programming community. They generalize the (type) parameterized algebraic datatypes (PADTs) of ML and Haskell by permitting value constructors to return ...
Impredicative Encodings of (Higher) Inductive Types
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer SciencePostulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit dependent eliminators. To recover η and ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2021
22 pages
Copyright © 2021 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 ACM 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 2021
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
ICFP '21
Sponsor:
ICFP '21: 26th ACM SIGPLAN International Conference on Functional Programming
August 22, 2021
Virtual, Republic of Korea
Upcoming Conference
ICFP '25
- Sponsor:
- sigplan
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 130Total Downloads
- Downloads (Last 12 months)38
- Downloads (Last 6 weeks)6
Reflects downloads up to 24 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