Type Patterns: Pattern Matching on Shape-Carrying Array Types
IFL '23: Proceedings of the 35th Symposium on Implementation and Application of Functional Languages
Article No.: 11, Pages 1 - 14
Abstract
In this paper we present type patterns: a notation for shape-carrying array types that enables the specification of dependent type signatures while maintaining flexibility and a high level of code readability. Similar notations pre-exist, but we extend them to support rank-polymorphism and specifications of arbitrarily complex constraints between values and types. Furthermore, we enable type patterns to double as a pattern matching mechanism against shapes and shape-components of array arguments, making those values directly available in the corresponding function bodies.
While this notation could be used as a basis for a dependently typed language, in our prototypical implementation in the context of SaC we do not require all dependencies to be resolved statically. Instead, we follow a hybrid approach: we map the proposed type patterns into the pre-existing type system of SaC, and we generate additional constraints which we try to statically resolve as far as possible by means of partial evaluation. Any remaining constraints are checked at run-time. We outline our implementation in the context of the SaC ecosystem, and present several examples demonstrating the effectiveness of this hybrid approach based on partial evaluation.
References
[1]
Zachary Ryan Anderson. 2007. Static analysis of C for hybrid type checking. Technical Report. Tech. Rep. EECS-2007-1, UC Berkeley.
[2]
Lennart Augustsson. 1998. Cayenne—a Language with Dependent Types. In Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming(ICFP ’98). Association for Computing Machinery, New York, NY, USA, 239–250. https://doi.org/10.1145/289423.289451
[3]
Lubin Bailly, Troels Henriksen, and Martin Elsman. 2023. Shape-Constrained Array Programming with Size-Dependent Types. In Proceedings of the 11th ACM SIGPLAN International Workshop on Functional High-Performance and Numerical Computing(FHPNC 2023). Association for Computing Machinery, New York, NY, USA, 29–41. https://doi.org/10.1145/3609024.3609412
[4]
Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. 2005. The Spec# Programming System: An Overview. In Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, and Traian Muntean (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 49–69.
[5]
Robert Bernecky, Stephan Herhut, and Sven-Bodo Scholz. 2010. Symbiotic Expressions. In Implementation and Application of Functional Languages, Marco T. Morazán and Sven-Bodo Scholz (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 107–124.
[6]
Ana Bove, Peter Dybjer, and Ulf Norell. 2009. A Brief Overview of Agda - A Functional Language with Dependent Types. In Theorem Proving in Higher Order Logics, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 73–78.
[7]
Edwin C. Brady. 2011. IDRIS –: Systems Programming Meets Full Dependent Types. In Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification(PLPV ’11). Association for Computing Machinery, New York, NY, USA, 43–54. https://doi.org/10.1145/1929529.1929536
[8]
Adam Chlipala. 2010. An Introduction to Programming and Proving with Dependent Types in Coq. Journal of Formalized Reasoning 3, 2 (Jan. 2010), 1–93. https://doi.org/10.6092/issn.1972-5787/1978
[9]
Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George C. Necula. 2007. Dependent Types for Low-Level Programming. In Programming Languages and Systems, Rocco De Nicola (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 520–535.
[10]
Bruno Dutertre and Leonardo De Moura. 2006. The yices smt solver. Tool paper at http://yices. csl. sri. com/tool-paper. pdf 2, 2 (2006), 1–2.
[11]
Satoshi Egi. 2014. Non-Linear Pattern-Matching against Unfree Data Types with Lexical Scoping. CoRR abs/1407.0729 (2014). arXiv:1407.0729http://arxiv.org/abs/1407.0729
[12]
Satoshi Egi and Yuichi Nishiwaki. 2018. Non-linear Pattern Matching with Backtracking for Non-free Data Types. In Programming Languages and Systems, Sukyoung Ryu (Ed.). Springer International Publishing, Cham, 3–23.
[13]
Martin Erwig. 1997. Active patterns. In Implementation of Functional Languages, Werner Kluge (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 21–40.
[14]
Cormac Flanagan. 2006. Hybrid Type Checking. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL ’06). Association for Computing Machinery, New York, NY, USA, 245–256. https://doi.org/10.1145/1111037.1111059
[15]
Tim Freeman and Frank Pfenning. 1991. Refinement types for ML. In Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation. Association for Computing Machinery, 268–277. https://doi.org/10.1145/113445.113468
[16]
Clemens Grelck. 2012. Single Assignment C (SAC) High Productivity Meets High Performance. Springer Berlin Heidelberg, Berlin, Heidelberg, 207–278. https://doi.org/10.1007/978-3-642-32096-5_5
[17]
Clemens Grelck and Sven-Bodo Scholz. 2006. SAC–A Functional Array Language for Efficient Multi-threaded Execution. International Journal of Parallel Programming 34, 4 (01 Aug 2006), 383–427. https://doi.org/10.1007/s10766-006-0018-x
[18]
Clemens Grelck, Fangyong Tang, 2014. Towards Hybrid Array Types in SaC. In Software Engineering (Workshops)(CEUR Workshop Proceedings), Vol. 1129. CEUR-WS.org, 129–145. https://ceur-ws.org/Vol-1129/paper44.pdf
[19]
Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N Freund, and Cormac Flanagan. 2006. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop, Vol. 6. 93–104.
[20]
Dan Grossman, Michael Hicks, Trevor Jim, and Greg Morrisett. 2005. Cyclone: A type-safe dialect of C. C/C++ Users Journal 23, 1 (2005), 112–139.
[21]
Troels Henriksen and Martin Elsman. 2021. Towards Size-Dependent Types for Array Programming. In Proceedings of the 7th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming(ARRAY 2021). Association for Computing Machinery, New York, NY, USA, 1–14. https://doi.org/10.1145/3460944.3464310
[22]
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). Association for Computing Machinery, New York, NY, USA, 556–571. https://doi.org/10.1145/3062341.3062354
[23]
Stephan Herhut, Sven-Bodo Scholz, Robert Bernecky, Clemens Grelck, and Kai Trojahner. 2008. From Contracts Towards Dependent Types: Proofs by Partial Evaluation. In Implementation and Application of Functional Languages, Olaf Chitil, Zoltán Horváth, and Viktória Zsók (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 254–273.
[24]
C Barry Jay and Milan Sekanina. 1996. Shape checking of array programs. Technical Report. Citeseer.
[25]
Tobias Kohn, Guido van Rossum, Gary Brandt Bucher II, Talin, and Ivan Levkivskyi. 2020. Dynamic Pattern Matching with Python. In Proceedings of the 16th ACM SIGPLAN International Symposium on Dynamic Languages(DLS 2020). Association for Computing Machinery, New York, NY, USA, 85–98. https://doi.org/10.1145/3426422.3426983
[26]
George C. Necula, Scott McPeak, and Westley Weimer. 2002. CCured: Type-Safe Retrofitting of Legacy Code. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL ’02). Association for Computing Machinery, New York, NY, USA, 128–139. https://doi.org/10.1145/503272.503286
[27]
Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. 2004. Dynamic Typing with Dependent Types. In Exploring New Frontiers of Theoretical Informatics, Jean-Jacques Levy, Ernst W. Mayr, and John C. Mitchell (Eds.). Springer US, Boston, MA, 437–450.
[28]
Corneliu Popeea, Dana N. Xu, and Wei-Ngan Chin. 2008. A Practical and Precise Inference and Specializer for Array Bound Checks Elimination. In Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation(PEPM ’08). Association for Computing Machinery, New York, NY, USA, 177–187. https://doi.org/10.1145/1328408.1328434
[29]
Sven-Bodo Scholz. 2003. Single Assignment C: efficient support for high-level array operations in a functional setting. Journal of functional programming 13, 6 (2003), 1005–1059. https://doi.org/10.1017/S0956796802004458
[30]
Sven-Bodo Scholz and Artjoms Šinkarovs. 2021. Tensor Comprehensions in SaC. In Proceedings of the 31st Symposium on Implementation and Application of Functional Languages(IFL ’19). Association for Computing Machinery, New York, NY, USA, Article 15, 13 pages. https://doi.org/10.1145/3412932.3412947
[31]
Justin Slepak, Panagiotis Manolios, and Olin Shivers. 2018. Rank Polymorphism Viewed as a Constraint Problem. In Proceedings of the 5th ACM SIGPLAN International Workshop on Libraries, Languages, and Compilers for Array Programming(ARRAY 2018). Association for Computing Machinery, New York, NY, USA, 34–41. https://doi.org/10.1145/3219753.3219758
[32]
Justin Slepak, Olin Shivers, and Panagiotis Manolios. 2014. An Array-Oriented Language with Static Rank Polymorphism. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 27–46.
[33]
Fangyong Tang, Clemens Grelck, 2012. User-defined shape constraints in SaC. In DRAFT PROCEEDINGS OF THE 24TH SYMPOSIUM ON IMPLEMENTATION AND APPLICATION OF FUNCTIONAL LANGUAGES (IFL 2012). 416–434.
[34]
Kai Trojahner. 2011. QUBE-Array Programming with Dependent Types. Institute of Software Engineering and Programming Languages of the University of Lübeck (2011).
[35]
Kai Trojahner and Clemens Grelck. 2009. Dependently typed array programs don’t go wrong. The Journal of Logic and Algebraic Programming 78, 7 (2009), 643–664. https://doi.org/10.1016/j.jlap.2009.03.002 The 19th Nordic Workshop on Programming Theory (NWPT 2007).
[36]
Bernard van Gastel, Rody Kersten, and Marko C. J. D. van Eekelen. 2015. Using Dependent Types to Define Energy Augmented Semantics of Programs. In Foundational and Practical Aspects of Resource Analysis - 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015, Revised Selected Papers(Lecture Notes in Computer Science), Marko C. J. D. van Eekelen and Ugo Dal Lago (Eds.). Vol. 9964. 20–39. https://doi.org/10.1007/978-3-319-46559-3_2
[37]
Bernard van Gastel and Marko C. J. D. van Eekelen. 2017. Towards Practical, Precise and Parametric Energy Analysis of IT Controlled Systems. In Proceedings 8th Workshop on Developments in Implicit Computational Complexity and 5th Workshop on Foundational and Practical Aspects of Resource Analysis, DICE-FOPARA@ETAPS 2017, Uppsala, Sweden, April 22-23, 2017(EPTCS), Guillaume Bonfante and Georg Moser (Eds.). Vol. 248. 24–37. https://doi.org/10.4204/EPTCS.248.7
[38]
Hongwei Xi and Frank Pfenning. 1998. Eliminating Array Bound Checking through Dependent Types. In Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation(PLDI ’98). Association for Computing Machinery, New York, NY, USA, 249–257. https://doi.org/10.1145/277650.277732
[39]
Hongwei Xi and Frank Pfenning. 1999. Dependent Types in Practical Programming. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL ’99). Association for Computing Machinery, New York, NY, USA, 214–227. https://doi.org/10.1145/292540.292560
[40]
Christoph Zenger. 1997. Indexed types. Theoretical Computer Science 187, 1 (1997), 147–165. https://doi.org/10.1016/S0304-3975(97)00062-5
[41]
He Zhu, Aditya V. Nori, and Suresh Jagannathan. 2015. Dependent Array Type Inference from Tests. In Verification, Model Checking, and Abstract Interpretation, Deepak D’Souza, Akash Lal, and Kim Guldstrand Larsen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 412–430.
Recommendations
Set-theoretic types for polymorphic variants
ICFP '16Polymorphic variants are a useful feature of the OCaml language whose current definition and implementation rely on kinding constraints to simulate a subtyping relation via unification. This yields an awkward formalization and results in a type system ...
Set-theoretic types for polymorphic variants
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional ProgrammingPolymorphic variants are a useful feature of the OCaml language whose current definition and implementation rely on kinding constraints to simulate a subtyping relation via unification. This yields an awkward formalization and results in a type system ...
MLF for everyone (users, implementers, and designers)
ML '07: Proceedings of the 2007 workshop on Workshop on MLMLF is an alternative to ML that permits second-order polymorphism as in System F but retains (partial) type inference a la ML. Type annotations are requested only on parameters of functions that are used polymorphically. Type abstractions and type ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2023
186 pages
ISBN:9798400716317
DOI:10.1145/3652561
Copyright © 2023 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 19 June 2024
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Conference
IFL 2023
IFL 2023: The 35th Symposium on Implementation and Application of Functional Languages
August 29 - 31, 2023
Braga, Portugal
Acceptance Rates
Overall Acceptance Rate 19 of 36 submissions, 53%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 96Total Downloads
- Downloads (Last 12 months)96
- Downloads (Last 6 weeks)32
Reflects downloads up to 14 Nov 2024
Other Metrics
Citations
View Options
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML FormatGet Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in