Cited By
View all- Melquiond GMoreau J(2024)A Safe Low-Level Language for Computer Algebra and Its Formally Verified CompilerProceedings of the ACM on Programming Languages10.1145/36746298:ICFP(121-146)Online publication date: 15-Aug-2024
Polymorphic Types with Polynomial Sizes
Pages 36 - 49
Abstract
This article presents a compile-time analysis for tracking the size of data-structures in a statically typed and strict functional language. This information is valuable for static checking and code generation. Rather than relying on dependent types, we propose a type-system close to that of ML: polymorphism is used to define functions that are generic in types and sizes; both can be inferred. This approach is convenient, in particular for a language used to program critical embedded systems, where sizes are indeed known at compile-time. By using sizes that are multivariate polynomials, we obtain a good compromise between the expressiveness of the size language and its properties (verification, inference).
The article defines a minimal functional language that is sufficient to capture size constraints in types. It presents its dynamic semantics, the type system and inference algorithm. Last, we sketch some practical extensions that matter for a more realistic language.
Supplementary Material
This document contains the proofs and detailed formalization of the results presented in the article.
- Download
- 546.63 KB
References
[1]
Alexander Aiken and Edward L. Wimmers. 1993. Type Inclusion Constraints and Type Inference. In Proceedings of the conference on Functional programming languages and computer architecture, FPCA 1993, Copenhagen, Denmark, June 9-11, 1993, John Williams (Ed.). ACM, 31–41. https://doi.org/10.1145/165180.165188
[2]
Emil Axelsson, Koen Claessen, and Mary Sheeran. 2005. Wired: Wire-Aware Circuit Design. In Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, Proceedings, Dominique Borrione and Wolfgang J. Paul (Eds.) (Lecture Notes in Computer Science, Vol. 3725). Springer, 5–19. https://doi.org/10.1007/11560548_4
[3]
John G. P. Barnes. 2003. High Integrity Software - The SPARK Approach to Safety and Security. Addison-Wesley. isbn:978-0-321-13616-9 http://www.addison-wesley.de/main/main.asp?page=englisch/bookdetails&ProductID=88293
[4]
Richard S. Bird and Philip Wadler. 1988. Introduction to functional programming. Prentice Hall. isbn:978-0-13-484197-7
[5]
Per Bjesse, Koen Claessen, Mary Sheeran, and Satnam Singh. 1998. Lava: Hardware Design in Haskell. 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, 174–184. https://doi.org/10.1145/289423.289440
[6]
Koen Claessen, Mary Sheeran, and Joel Svensson. 2012. Expressive array constructs in an embedded GPU kernel programming language. In Proceedings of the POPL 2012 Workshop on Declarative Aspects of Multicore Programming, DAMP 2012, Philadelphia, PA, USA, Saturday, January 28, 2012, Umut A. Acar and Vítor Santos Costa (Eds.). ACM, 21–30. https://doi.org/10.1145/2103736.2103740
[7]
Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. 2017. SCADE 6: A formal language for embedded critical software development (invited paper). In 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017, Sophia Antipolis, France, September 13-15, 2017, Frédéric Mallet, Min Zhang, and Eric Madelaine (Eds.). IEEE Computer Society, 1–11. https://doi.org/10.1109/TASE.2017.8285623
[8]
Francesco Dagnino, Viviana Bono, Elena Zucca, and Mariangiola Dezani-Ciancaglini. 2020. Soundness Conditions for Big-Step Semantics. In Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Peter Müller (Ed.) (Lecture Notes in Computer Science, Vol. 12075). Springer, 169–196. https://doi.org/10.1007/978-3-030-44914-8_7
[9]
Martin Elsman, Troels Henriksen, and Niels Gustav Westphal Serup. 2019. Data-parallel flattening by expansion. In Proceedings of the 6th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming, ARRAY@PLDI 2019, Phoenix, AZ, USA, June 22, 2019, Jeremy Gibbons (Ed.). ACM, 14–24. https://doi.org/10.1145/3315454.3329955
[10]
John Feo, David C. Cann, and R. R. Oldehoeft. 1990. A Report on the Sisal Language Project. J. Parallel Distributed Comput., 10, 4 (1990), 349–366. https://doi.org/10.1016/0743-7315(90)90035-N
[11]
Cormac Flanagan. 2006. Hybrid type checking. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, J. Gregory Morrisett and Simon L. Peyton Jones (Eds.). ACM, 245–256. https://doi.org/10.1145/1111037.1111059
[12]
J-L Gaudiot, Wim Bohm, Walid Najjar, Tom DeBoni, John Feo, and Patrick Miller. 1997. The Sisal model of functional programming and its implementation. In Parallel Algorithms/Architecture Synthesis (Proceedings. Second Aizu International Symposium). IEEE, 112–123.
[13]
Léonard Gérard, Adrien Guatto, Cédric Pasteur, and Marc Pouzet. 2012. A modular memory optimization for synchronous data-flow languages: application to arrays in a lustre compiler. In SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2012, LCTES ’12, Beijing, China - June 12 - 13, 2012, Reinhard Wilhelm, Heiko Falk, and Wang Yi (Eds.). ACM, 51–60. https://doi.org/10.1145/2248418.2248426
[14]
Nicolas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. 1991. The synchronous data flow programming language LUSTRE. Proc. IEEE, 79, 9 (1991), 1305–1320. https://doi.org/10.1109/5.97300
[15]
Fritz Henglein. 1993. Type Inference with Polymorphic Recursion. ACM Transactions on Programming Languages and Systems (TOPLAS), 15, 2 (1993), 253–289. https://doi.org/10.1145/169701.169692
[16]
Troels Henriksen and Martin Elsman. 2021. Towards size-dependent types for array programming. In ARRAY 2021: Proceedings of the 7th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming, Virtual Event, Canada, 21 June, 2021, Tze Meng Low and Jeremy Gibbons (Eds.). ACM, 1–14. https://doi.org/10.1145/3460944.3464310
[17]
Troels Henriksen, Niels G. W. Serup, Martin Elsman, Fritz Henglein, and Cosmin E. Oancea. 2017. Futhark: purely functional GPU-programming with nested parallelism and in-place array updates. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017, Albert Cohen and Martin T. Vechev (Eds.). ACM, 556–571. https://doi.org/10.1145/3062341.3062354
[18]
Roger Hindley. 1969. The principal type-scheme of an object in combinatory logic. Transactions of the american mathematical society, 146 (1969), 29–60.
[19]
John Hughes, Lars Pareto, and Amr Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In Conference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996, Hans-Juergen Boehm and Guy L. Steele Jr. (Eds.). ACM Press, 410–423. https://doi.org/10.1145/237721.240882
[20]
C Barry Jay and Milan Sekanina. 1997. Shape checking of array programs. In Computing: the Australasian Theory Seminar, Proceedings (Australian Computer Science Communications, Vol. 19). University of Technology, Sydney, Australia, 113–121.
[21]
Mark P. Jones. 1997. First-class Polymorphism with Type Inference. In Conference Record of POPL’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France, 15-17 January 1997, Peter Lee, Fritz Henglein, and Neil D. Jones (Eds.). ACM Press, 483–496. https://doi.org/10.1145/263699.263765
[22]
Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical type inference for arbitrary-rank types. Journal of functional programming, 17, 1 (2007), 1–82. https://doi.org/10.1017/S0956796806006034
[23]
Andrew Kennedy. 1994. Dimension Types. In Programming Languages and Systems - ESOP’94, 5th European Symposium on Programming, Edinburgh, UK, April 11-13, 1994, Proceedings, Donald Sannella (Ed.) (Lecture Notes in Computer Science, Vol. 788). Springer, 348–362. https://doi.org/10.1007/3-540-57880-3_23
[24]
Kenneth L. Knowles and Cormac Flanagan. 2007. Type Reconstruction for General Refinement Types. In Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings, Rocco De Nicola (Ed.) (Lecture Notes in Computer Science, Vol. 4421). Springer, 505–519. https://doi.org/10.1007/978-3-540-71316-6_34
[25]
Florence Maraninchi and Lionel Morel. 2004. Arrays and Contracts for the Specification and Analysis of Regular Systems. In 4th International Conference on Application of Concurrency to System Design (ACSD 2004), 16-18 June 2004, Hamilton, Canada. IEEE Computer Society, 57–66. https://doi.org/10.1109/CSD.2004.1309116
[26]
Lambert G. L. T. Meertens. 1983. Incremental Polymorphic Type Checking in B. In Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 1983, John R. Wright, Larry Landweber, Alan J. Demers, and Tim Teitelbaum (Eds.). ACM Press, 265–275. https://doi.org/10.1145/567067.567092
[27]
Robin Milner. 1978. A Theory of Type Polymorphism in Programming. Journal of computer and system sciences, 17, 3 (1978), 348–375. https://doi.org/10.1016/0022-0000(78)90014-4
[28]
John C. Mitchell and Gordon D. Plotkin. 1988. Abstract Types Have Existential Type. ACM Transactions on Programming Languages and Systems (TOPLAS), 10, 3 (1988), 470–502. https://doi.org/10.1145/44501.45065
[29]
Alan Mycroft. 1984. Polymorphic Type Schemes and Recursive Definitions. In International Symposium on Programming, 6th Colloquium, Toulouse, France, April 17-19, 1984, Proceedings, Manfred Paul and Bernard J. Robinet (Eds.) (Lecture Notes in Computer Science, Vol. 167). Springer, 217–228. https://doi.org/10.1007/3-540-12925-1_41
[30]
Hanne Riis Nielson and Flemming Nielson. 1988. Automatic Binding Time Analysis for a Typed lambda-Calculus. Science of computer programming, 10, 1 (1988), 139–176. https://doi.org/10.1016/0167-6423(88)90025-1
[31]
Adam Paszke, Daniel D. Johnson, David Duvenaud, Dimitrios Vytiniotis, Alexey Radul, Matthew J. Johnson, Jonathan Ragan-Kelley, and Dougal Maclaurin. 2021. Getting to the point: index sets and parallelism-preserving autodiff for pointful array programming. Proceedings of the ACM on Programming Languages, 5, ICFP (2021), 1–29. https://doi.org/10.1145/3473593
[32]
François Pottier. 2001. Simplifying Subtyping Constraints: A Theory. Information and computation, 170, 2 (2001), 153–183. https://doi.org/10.1006/inco.2001.2963
[33]
Jonathan Ragan-Kelley, Connelly Barnes, Andrew Adams, Sylvain Paris, Frédo Durand, and Saman P. Amarasinghe. 2013. Halide: a language and compiler for optimizing parallelism, locality, and recomputation in image processing pipelines. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 519–530. https://doi.org/10.1145/2491956.2462176
[34]
Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008. Liquid types. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, Rajiv Gupta and Saman P. Amarasinghe (Eds.). ACM, 159–169. https://doi.org/10.1145/1375581.1375602
[35]
Michel Steuwer, Christian Fensch, Sam Lindley, and Christophe Dubach. 2015. Generating performance portable code using rewrite rules: from high-level functional expressions to high-performance OpenCL code. 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, 205–217. https://doi.org/10.1145/2784731.2784754
[36]
Kai Trojahner and Clemens Grelck. 2009. Dependently typed array programs don’t go wrong. J. Log. Algebraic Methods Program., 78, 7 (2009), 643–664. https://doi.org/10.1016/j.jlap.2009.03.002
[37]
Hongwei Xi and Frank Pfenning. 1998. Eliminating Array Bound Checking Through Dependent Types. In Proceedings of the ACM SIGPLAN ’98 Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, June 17-19, 1998, Jack W. Davidson, Keith D. Cooper, and A. Michael Berman (Eds.). ACM, 249–257. https://doi.org/10.1145/277650.277732
[38]
Hongwei Xi and Frank Pfenning. 1999. Dependent Types in Practical Programming. In POPL ’99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999, Andrew W. Appel and Alex Aiken (Eds.). ACM, 214–227. https://doi.org/10.1145/292540.292560
[39]
Christoph Zenger. 1997. Indexed Types. Theoretical computer science, 187, 1-2 (1997), 147–165. https://doi.org/10.1016/S0304-3975(97)00062-5
Index Terms
- Polymorphic Types with Polynomial Sizes
Recommendations
A polymorphic modal type system for lisp-like multi-staged languages
POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesThis article presents a polymorphic modal type system and its principal type inference algorithm that conservatively extend ML by all of Lisp's staging constructs (the quasi-quotation system). The combination is meaningful because ML is a practical ...
Polymorphic type inference and abstract data types
Many statically typed programming languages provide an abstract data type construct, such as the module in Modula-2. However, in most of these languages, implementations of abstract data types are not first-class values. Thus, they cannot be assigned to ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
June 2023
74 pages
Copyright © 2023 ACM.
Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 06 June 2023
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
ARRAY '23
Sponsor:
ARRAY '23: 9th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming
June 18, 2023
FL, Orlando, USA
Acceptance Rates
Overall Acceptance Rate 17 of 25 submissions, 68%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 106Total Downloads
- Downloads (Last 12 months)23
- Downloads (Last 6 weeks)1
Reflects downloads up to 19 Nov 2024
Other Metrics
Citations
Cited By
View all- Melquiond GMoreau J(2024)A Safe Low-Level Language for Computer Algebra and Its Formally Verified CompilerProceedings of the ACM on Programming Languages10.1145/36746298:ICFP(121-146)Online publication date: 15-Aug-2024
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