Cited By
View all- van der Rest CPoulsen C(2023)Types and Semantics for Extensible Data TypesProgramming Languages and Systems10.1007/978-981-99-8311-7_3(46-66)Online publication date: 26-Nov-2023
Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc
Article No.: 201, Pages 356 - 384
Abstract
We present a novel approach to generic programming over extensible data types. Row types capture the structure of records and variants, and can be used to express record and variant subtyping, record extension, and modular composition of case branches. We extend row typing to capture generic programming over rows themselves, capturing patterns including lifting operations to records and variations from their component types, and the duality between cases blocks over variants and records of labeled functions, without placing specific requirements on the fields or constructors present in the records and variants. We formalize our approach in System Rđ, an extension of Fđ with row types, and give a denotational semantics for (stratified) Rđ in Agda.
References
[1]
Patrick Bahr. 2014. Composing and decomposing data types: a closed type families implementation of data types Ă la carte. In Proceedings of the 10th ACM SIGPLAN workshop on Generic programming, WGP 2014, Gothenburg, Sweden, August 31, 2014, JosĂ© Pedro MagalhĂŁes and Tiark Rompf (Eds.). ACM, 71â82.
[2]
Bernard Berthomieu and Camille le MoniĂšs de Sagazan. 1995. A Calculus of Tagged Types, with applications to process languages. In Workshop on types for program analysis. Aarhus.
[3]
Matthias Blume, Umut A. Acar, and Wonseok Chae. 2006. Extensible programming with first-class cases. In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-21, 2006, John H. Reppy and Julia L. Lawall (Eds.). ACM, 239â250.
[4]
Adam Chlipala. 2010. Ur: statically-typed metaprogramming with type-level record computation. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10, 2010, Benjamin G. Zorn and Alexander Aiken (Eds.). ACM, 122â133.
[5]
Adam Chlipala. 2015. An optimizing compiler for a purely functional web-application language. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015, Kathleen Fisher and John H. Reppy (Eds.). ACM, 10â21. https://doi.org/10.1145/2784731.2784741
[6]
Adam Chlipala. 2015. Ur/Web: A Simple Model for Programming the Web. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 153â165. https://doi.org/10.1145/2676726.2677004
[7]
Jana Dunfield. 2012. Elaborating intersection and union types. In ACM SIGPLAN International Conference on Functional Programming, ICFPâ12, Copenhagen, Denmark, September 9-15, 2012, Peter Thiemann and Robby Bruce Findler (Eds.). ACM, 17â28.
[8]
Jana Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and easy bidirectional typechecking for higher-rank polymorphism. In ACM SIGPLAN International Conference on Functional Programming, ICFPâ13, Boston, MA, USA - September 25 - 27, 2013, Greg Morrisett and Tarmo Uustalu (Eds.). ACM, 429â442. https://doi.org/10.1145/2500365.2500582
[9]
Edward Gan, Jesse A. Tov, and Greg Morrisett. 2014. Type Classes for Lightweight Substructural Types. In Proceedings Third International Workshop on Linearity, LINEARITY 2014, Vienna, Austria, 13th July, 2014, Sandra Alves and Iliano Cervesato (Eds.) (EPTCS, Vol. 176). 34â48. https://doi.org/10.4204/EPTCS.176.4
[10]
Jacques Garrigue. 1998. Programming with Polymorphic Variants. In ML Workshop. ACM.
[11]
Benedict R. Gaster and Mark P. Jones. 1996. A Polymorphic Type System for Extensible Records and Variants. University of Nottingham.
[12]
Robert Harper and Benjamin Pierce. 1991. A Record Calculus Based on Symmetric Concatenation. In Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL â91). ACM, 131â142.
[13]
Daniel Hillerström and Sam Lindley. 2016. Liberating effects with rows and handlers. In TyDe@ICFP. ACM, 15â27.
[14]
Alex Hubers and J. Garrett Morris. 2023. Generic Programming with Extensible Data Types; Or, Making Ad Hoc Extensible Data Types Less Ad HocâArtifact. https://doi.org/10.5281/zenodo.8116889
[15]
Apoorv Ingle, Alex Hubers, and J. Garrett Morris. 2022. Partial type constructors in practice. In Haskell â22: 15th ACM SIGPLAN International Haskell Symposium, Ljubljana, Slovenia, September 15 - 16, 2022, Nadia Polikarpova (Ed.). ACM, 95â107. https://doi.org/10.1145/3546189.3549923
[16]
Mark P. Jones. 1994. Qualified Types: Theory and Practice. Cambridge University Press.
[17]
Mark P. Jones and Iavor S. Diatchki. 2008. Language and program design for functional dependencies. In Proceedings of the first ACM SIGPLAN symposium on Haskell (Haskell â08). ACM, Victoria, BC, Canada. 87â98.
[18]
Mark P. Jones, J. Garrett Morris, and Richard A. Eisenberg. 2020. Partial type constructors: or, making ad hoc datatypes less ad hoc. Proc. ACM Program. Lang., 4, POPL (2020), 40:1â40:28.
[19]
Ambrus Kaposi, AndrĂĄs KovĂĄcs, and Nicolai Kraus. 2019. Shallow Embedding of Type Theory is Morally Correct. In Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings, Graham Hutton (Ed.) (Lecture Notes in Computer Science, Vol. 11825). Springer, 329â365. https://doi.org/10.1007/978-3-030-33636-3_12
[20]
Andrew W. Keep and R. Kent Dybvig. 2013. A nanopass framework for commercial compiler development. In ACM SIGPLAN International Conference on Functional Programming, ICFPâ13, Boston, MA, USA - September 25 - 27, 2013, Greg Morrisett and Tarmo Uustalu (Eds.). ACM, 343â350. https://doi.org/10.1145/2500365.2500618
[21]
Oleg Kiselyov, Ralf LĂ€mmel, and Keean Schupke. 2004. Strongly typed heterogeneous collections. In Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2004, Snowbird, UT, USA, September 22-22, 2004, Henrik Nilsson (Ed.). ACM, 96â107.
[22]
Daan Leijen. 2004. First-class labels for extensible rows (technical report uu-cs-2004-51 ed.). Dept. of Computer Science, Universiteit Utrecht. https://www.microsoft.com/en-us/research/publication/first-class-labels-for-extensible-rows/
[23]
Daan Leijen. 2005. Extensible records with scoped labels. In Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24 September 2005. 179â194.
[24]
Daan Leijen. 2014. Koka: Programming with Row Polymorphic Effect Types. In Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2014, Grenoble, France, 12 April 2014., Paul Levy and Neel Krishnaswami (Eds.) (EPTCS, Vol. 153). 100â126.
[25]
Daan Leijen. 2017. Type directed compilation of row-typed algebraic effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 486â499.
[26]
Daniel Leivant. 1991. Finitely Stratified Polymorphism. Inf. Comput., 93, 1 (1991), 93â113. https://doi.org/10.1016/0890-5401(91)90053-5
[27]
Sam Lindley and James Cheney. 2012. Row-based effect types for database integration. In Proceedings of TLDI 2012: The Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation, Philadelphia, PA, USA, Saturday, January 28, 2012, Benjamin C. Pierce (Ed.). ACM, 91â102.
[28]
Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do be do be do. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 500â514.
[29]
Sam Lindley and J. Garrett Morris. 2017. Lightweight functional session types. In Behavioural Types: from Theory to Tools, Simon Gay and AntĂłnio Ravara (Eds.). River Publishers.
[30]
Henning Makholm and J. B. Wells. 2005. Type inference, principal typings, and let-polymorphism for first-class mixin modules. In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005, Olivier Danvy and Benjamin C. Pierce (Eds.). ACM, 156â167.
[31]
Conor McBride. 2010. Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. In Proceedings of the ACM SIGPLAN Workshop on Generic Programming, WGP 2010, Baltimore, MD, USA, September 27-29, 2010, Bruno C. d. S. Oliveira and Marcin Zalewski (Eds.). ACM, 1â12. https://doi.org/10.1145/1863495.1863497
[32]
Robin Milner. 1978. A theory of type polymorphism in programming. J. Comput. System Sci., 348â375.
[33]
J. Garrett Morris. 2015. Variations on variants. In Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Ben Lippmeier (Ed.) (Haskell â15). ACM, Vancouver, BC. 71â81.
[34]
J. Garrett Morris. 2016. The best of both worlds: linear functional programming without compromise. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 448â461. https://doi.org/10.1145/2951913.2951925
[35]
J. Garrett Morris and James McKinna. 2019. Abstracting extensible data types: or, rows by any other name. Proc. ACM Program. Lang., 3, POPL (2019), 12:1â12:28. https://doi.org/10.1145/3290325
[36]
Bruno Oliveira, Shin-Cheng Mu, and Shu-Hung You. 2015. Modular reifiable matching: a list-of-functors approach to two-level types. In Haskell. ACM, 82â93.
[37]
Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. 2006. Simple unification-based type inference for GADTs. In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-21, 2006, John H. Reppy and Julia Lawall (Eds.). ACM, 50â61. https://doi.org/10.1145/1159803.1159811
[38]
Gordon D. Plotkin and John Power. 2003. Algebraic Operations and Generic Effects. Applied Categorical Structures, 11, 1 (2003), 69â94. https://doi.org/10.1023/A:1023064908962
[39]
Gordon D. Plotkin and Matija Pretnar. 2009. Handlers of Algebraic Effects. In Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, Giuseppe Castagna (Ed.) (Lecture Notes in Computer Science, Vol. 5502). Springer, 80â94. https://doi.org/10.1007/978-3-642-00590-9_7
[40]
François Pottier and Didier Rémy. 2005. The essence of ML type inference. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). The MIT Press.
[41]
Didier RĂ©my. 1989. Typechecking Records and Variants in a Natural Extension of ML. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989. ACM Press, 77â88.
[42]
Didier RĂ©my. 1992. Typing Record Concatenation for Free. In POPL â92. ACM, Albuquerque, New Mexico. 166â176.
[43]
Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliveira, and Steve Zdancewic. 2023. A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in Fâ. Proc. ACM Program. Lang., 7, POPL (2023), 515â543. https://doi.org/10.1145/3571211
[44]
Dipanwita Sarkar, Oscar Waddell, and R. Kent Dybvig. 2004. A nanopass infrastructure for compiler education. In Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, ICFP 2004, Snow Bird, UT, USA, September 19-21, 2004, Chris Okasaki and Kathleen Fisher (Eds.). ACM, 201â212. https://doi.org/10.1145/1016850.1016878
[45]
Martin Sulzmann. 1997. Designing Record Systems. Yale University.
[46]
Wouter Swierstra. 2008. Data types Ă la carte. J. Funct. Program., 18, 04 (2008), 423â436.
[47]
Philip Wadler. 1998. The Expression Problem. http://homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt
[48]
Philip Wadler and Stephen Blott. 1989. How to Make ad-hoc Polymorphism Less ad-hoc. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989. ACM Press, 60â76. https://doi.org/10.1145/75277.75283
[49]
Mitchell Wand. 1987. Complete Type Inference for Simple Objects. In Proceedings of the Symposium on Logic in Computer Science (LICS â87), Ithaca, New York, USA, June 22-25, 1987. IEEE Computer Society, 37â44.
[50]
Mitchell Wand. 1989. Type Inference for Record Concatenation and Multiple Inheritance. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS â89), Pacific Grove, California, USA, June 5-8, 1989. IEEE Computer Society, 92â97.
[51]
Mitchell Wand. 1991. Type Inference for Record Concatenation and Multiple Inheritance. Inf. Comput., 93, 1 (1991), 1â15.
Index Terms
- Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc
Recommendations
Abstracting extensible data types: or, rows by any other name
We present a novel typed language for extensible data types, generalizing and abstracting existing systems of row types and row polymorphism. Extensible data types are a powerful addition to traditional functional programming languages, capturing ideas ...
Qualified types for MLF
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingMLF is a type system that extends a functional language with impredicative rank-n polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that ...
Qualified types for MLF
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingMLF is a type system that extends a functional language with impredicative rank-n polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2023
981 pages
Copyright © 2023 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 31 August 2023
Published in PACMPL Volume 7, Issue ICFP
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- NSF
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 536Total Downloads
- Downloads (Last 12 months)432
- Downloads (Last 6 weeks)64
Reflects downloads up to 12 Dec 2024
Other Metrics
Citations
Cited By
View all- van der Rest CPoulsen C(2023)Types and Semantics for Extensible Data TypesProgramming Languages and Systems10.1007/978-981-99-8311-7_3(46-66)Online publication date: 26-Nov-2023
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