Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/3471874.3472982acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
research-article

Haskell⁻¹: automatic function inversion in Haskell

Published: 18 August 2021 Publication History

Abstract

We present an approach for automatic function inversion in Haskell. The inverse functions we generate are based on an extension of Haskell's computational model with non-determinism and free variables. We implement this functional logic extension of Haskell via a monadic lifting of functions and type declarations. Using inverse functions, we additionally show how Haskell's pattern matching can be augmented with support for functional patterns, which enable arbitrarily deep pattern matching in data structures. Finally, we provide a plugin for the Glasgow Haskell Compiler to seamlessly integrate inverses and functional patterns into the language, covering almost all of the Haskell2010 language standard.

References

[1]
Andreas Abel, Marcin Benke, Ana Bove, John Hughes, and Ulf Norell. 2005. Verifying Haskell Programs Using Constructive Type Theory. In Proceedings of the 2005 ACM SIGPLAN Workshop on Haskell (Haskell ’05). Association for Computing Machinery, New York, NY, USA. 62–73. isbn:978-1-59593-071-2 https://doi.org/10.1145/1088348.1088355
[2]
Sergei Abramov and Robert Glück. 2000. The Universal Resolving Algorithm: Inverse Computation in a Functional Language. In Mathematics of Program Construction (MPC ’00). Springer-Verlag, Berlin, Heidelberg. 187–212. https://doi.org/10.1007/10722010_13
[3]
Sergei Abramov, Robert Glück, and Yuri Klimov. 2007. An Universal Resolving Algorithm for Inverse Computation of Lazy Languages. In Proceedings of the 6th International Andrei Ershov Memorial Conference on Perspectives of Systems Informatics (PSI ’06). Springer-Verlag, Berlin, Heidelberg. 27–40. https://doi.org/10.1007/978-3-540-70881-0_6
[4]
Jesús M. Almendros-Jiménez and Germán Vidal. 2007. Automatic Partial Inversion of Inductively Sequential Functions. In Proceedings of the 18th International Conference on Implementation and Application of Functional Languages (IFL ’06). Springer-Verlag, Berlin, Heidelberg. 253–270. https://doi.org/10.1007/978-3-540-74130-5_15
[5]
Sergio Antoy and Michael Hanus. 2006. Declarative Programming with Function Patterns. In Proceedings of the 15th International Conference on Logic-Based Program Synthesis and Transformation (LOPSTR ’05). Springer-Verlag, Berlin, Heidelberg. 6–22. https://doi.org/10.1007/11680093_2
[6]
Sergio Antoy and Michael Hanus. 2010. Functional Logic Programming. Commun. ACM, 53, 4 (2010), April, 74–85. issn:0001-0782 https://doi.org/10.1145/1721654.1721675
[7]
Bernd Braß el and Jan Christiansen. 2008. A Relation Algebraic Semantics for a Lazy Functional Logic Language. In Proceedings of the 10th International Conference on Relational and Kleene Algebra Methods in Computer Science (RelMiCS ’08). Springer-Verlag, Berlin, Heidelberg. 37–53. https://doi.org/10.1007/978-3-540-78913-0_5
[8]
Bernd Braß el, Michael Hanus, Björn Peemöller, and Fabian Reck. 2011. KiCS2: A New Compiler from Curry to Haskell. In Proceedings of the 20th International Conference on Functional and Constraint Logic Programming, Herbert Kuchen (Ed.) (WFLP ’11). Springer-Verlag, Berlin, Heidelberg. 1–18. isbn:978-3-642-22531-4
[9]
Bernd Braß el, Michael Hanus, Björn Peemöller, and Fabian Reck. 2013. Implementing Equational Constraints in a Functional Language. In Proceedings of the 15th International Symposium on Practical Aspects of Declarative Languages, Kostis Sagonas (Ed.) (PADL ’13, Vol. 7752). Springer-Verlag, Berlin, Heidelberg. 125–140. isbn:978-3-642-45284-0 https://doi.org/10.1007/978-3-642-45284-0_9
[10]
Koen Claessen and Peter Ljunglöf. 2001. Typed Logical Variables in Haskell. Electronic Notes in Theoretical Computer Science, 41, 1 (2001), 37. issn:1571-0661 https://doi.org/10.1016/S1571-0661(05)80544-4
[11]
Nils Anders Danielsson and Patrik Jansson. 2004. Chasing Bottoms. In International Conference on Mathematics of Program Construction (MPC ’04). Springer-Verlag, Berlin, Heidelberg. 85–109.
[12]
Satoshi Egi, Akira Kawata, Mayuko Kori, and Hiromi Ogawa. 2020. Sweet Egison: A Haskell Library for Non-Deterministic Pattern Matching.
[13]
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.). 11275, Springer International Publishing, Cham. 3–23. isbn:978-3-030-02767-4 https://doi.org/10.1007/978-3-030-02768-1_1
[14]
Martin Erwig and Simon Peyton Jones. 2001. Pattern Guards and Transformational Patterns. Electronic Notes in Theoretical Computer Science, 41, 1 (2001), 3. issn:1571-0661 https://doi.org/10.1016/S1571-0661(05)80540-7
[15]
Sebastian Fischer, Oleg Kiselyov, and Chung-Chieh Shan. 2011. Purely Functional Lazy Nondeterministic Programming. Journal of Functional Programming, 21, 4-5 (2011), Sept., 413–465. https://doi.org/10.1017/S0956796811000189
[16]
Robert Glück and Masahiko Kawabe. 2004. Derivation of Deterministic Inverse Programs Based on LR Parsing. In Proceedings of the 7th International Conference on Functional and Logic Programming (FLOPS ’04). Springer-Verlag, Berlin, Heidelberg. 291–306. https://doi.org/10.1007/978-3-540-24754-8_21
[17]
Sebastian Graf, Simon Peyton Jones, and Ryan G. Scott. 2020. Lower Your Guards: A Compositional Pattern-Match Coverage Checker. Proceedings of the ACM on Programming Languages, 4, ICFP (2020), Article 107, Aug., https://doi.org/10.1145/3408989
[18]
Michael Hanus, Björn Peemöller, and Jan Rasmus Tikovsky. 2014. Integration of Finite Domain Constraints in KiCS2. In Proceedings of the 7th Working Conference on Programming Languages (ATPS ’14, Vol. 1129). CEUR, 151–170.
[19]
Michael Hanus and Finn Teegen. 2020. Adding Data to Curry. In Declarative Programming and Knowledge Management (WFLP ’19). Springer International Publishing, Cham. 230–246. https://doi.org/10.1007/978-3-030-46714-2_15
[20]
Michael Hanus (ed.). 2016. Curry: An Integrated Functional Logic Language (Version 0.9.0).
[21]
M. C.B. Hennessy and E. A. Ashcroft. 1977. Parameter-Passing Mechanisms and Nondeterminism. In Proceedings of the Ninth Annual ACM Symposium on Theory of Computing (STOC ’77). Association for Computing Machinery, New York, NY, USA. 306–311. https://doi.org/10.1145/800105.803420
[22]
Ralf Hinze and Simon Peyton Jones. 2000. Derivable Type Classes. In Proceedings of the 2000 Haskell Workshop (Haskell ’00).
[23]
John Hughes. 1999. Restricted Data Types in Haskell. In Proceedings of the 1999 Haskell Workshop (Haskell ’99).
[24]
J. Jaffar and J.-L. Lassez. 1987. Constraint Logic Programming. In Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL ’87). Association for Computing Machinery, New York, NY, USA. 111–119. isbn:0-89791-215-2 https://doi.org/10.1145/41625.41635
[25]
Johan Jeuring, Patrik Jansson, and Cláudio Amaral. 2012. Testing Type Class Laws. In Proceedings of the 2012 Haskell Symposium (Haskell ’12). Association for Computing Machinery, New York, NY, USA. 49–60. https://doi.org/10.1145/2364506.2364514
[26]
Mark P. Jones. 1993. A System of Constructor Classes: Overloading and Implicit Higher-Order Polymorphism. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture (FPCA ’93). Association for Computing Machinery, New York, NY, USA. 52–61. isbn:0-89791-595-X https://doi.org/10.1145/165180.165190
[27]
Mark P. Jones. 1995. Functional Programming with Overloading and Higher-Order Polymorphism. In Advanced Functional Programming, Gerhard Goos, Juris Hartmanis, Jan Leeuwen, Johan Jeuring, and Erik Meijer (Eds.). 925, Springer-Verlag, Berlin, Heidelberg. 97–136. isbn:978-3-540-59451-2 https://doi.org/10.1007/3-540-59451-5_4
[28]
Andrew J. Kennedy and Dimitrios Vytiniotis. 2012. Every Bit Counts: The Binary Representation of Typed Data and Programs. Journal of Functional Programming, 22, 4– 5 (2012), Aug., 529–573. issn:0956-7968 https://doi.org/10.1017/S0956796812000263
[29]
Konstantin Läufer and Martin Odersky. 1994. Polymorphic Type Inference and Abstract Data Types. ACM Transactions on Programming Languages and Systems, 16, 5 (1994), Sept., 1411–1430. issn:0164-0925 https://doi.org/10.1145/186025.186031
[30]
Sheng Liang, Paul Hudak, and Mark Jones. 1995. Monad Transformers and Modular Interpreters. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’95). Association for Computing Machinery, New York, NY, USA. 333–343. https://doi.org/10.1145/199448.199528
[31]
Geoffrey Mainland. 2007. Why It’s Nice to Be Quoted: Quasiquoting for Haskell. In Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop (Haskell ’07). Association for Computing Machinery, New York, NY, USA. 73–82. https://doi.org/10.1145/1291201.1291211
[32]
Simon Marlow (ed.). 2010. Haskell 2010 Language Report.
[33]
Kazutaka Matsuda and Meng Wang. 2013. FliPpr: A Prettier Invertible Printing System. In Proceedings of the 22nd European Conference on Programming Languages and Systems (ESOP ’13). Springer-Verlag, Berlin, Heidelberg. 101–120. https://doi.org/10.1007/978-3-642-37036-6_6
[34]
Kazutaka Matsuda and Meng Wang. 2020. Sparcl: A Language for Partially-Invertible Computation. Proc. ACM Program. Lang., 4, ICFP (2020), Aug., https://doi.org/10.1145/3409000
[35]
John McCarthy. 1956. The Inversion of Functions Defined by Turing Machines. In Automata Studies, Annals of Mathematical Studies, J. McCarthy C.E. Shannon (Ed.). Princeton University Press, 177–181.
[36]
Markus Mohnen. 1996. Context Patterns in Haskell. In Selected Papers from the 8th International Workshop on Implementation of Functional Languages (IFL ’96). Springer-Verlag, Berlin, Heidelberg. 41–57. isbn:3-540-63237-9
[37]
Kazutaka Morita, Akimasa Morihata, Kiminori Matsuzaki, Zhenjiang Hu, and Masato Takeichi. 2007. Automatic Inversion Generates Divide-and-Conquer Parallel Programs. PLDI ’07. Association for Computing Machinery, New York, NY, USA. 146–155. https://doi.org/10.1145/1250734.1250752
[38]
Matthew Naylor, Emil Axelsson, and Colin Runciman. 2007. A Functional-Logic Library for Wired. In Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop (Haskell ’07). Association for Computing Machinery, New York, NY, USA. 37–48. https://doi.org/10.1145/1291201.1291207
[39]
Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe. 2005. Partial Inversion of Constructor Term Rewriting Systems. In Proceedings of the 16th International Conference on Term Rewriting and Applications (RTA ’05). Springer-Verlag, Berlin, Heidelberg. 264–278. https://doi.org/10.1007/978-3-540-32033-3_20
[40]
Dominic Orchard and Tom Schrijvers. 2010. Haskell Type Constraints Unleashed. In Proceedings of the 10th International Conference on Functional and Logic Programming (FLOPS ’10). Springer-Verlag, Berlin, Heidelberg. 56–71. https://doi.org/10.1007/978-3-642-12251-4_6
[41]
Nigel Perry. 1991. The Implementation of Practical Functional Programming Languages. University of London.
[42]
Simon 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 ’06). Association for Computing Machinery, New York, NY, USA. 50–61. isbn:1-59593-309-3 https://doi.org/10.1145/1159803.1159811
[43]
Simon Peyton Jones, Stephanie Weirich, Richard A. Eisenberg, and Dimitrios Vytiniotis. 2016. A Reflection on Types. In A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, Sam Lindley, Conor McBride, Phil Trinder, and Don Sannella (Eds.). Springer International Publishing, Cham. 292–317. isbn:978-3-319-30936-1 https://doi.org/10.1007/978-3-319-30936-1_16
[44]
Matthew Pickering, Gergő Érdi, Simon Peyton Jones, and Richard A. Eisenberg. 2016. Pattern Synonyms. In Proceedings of the 9th International Symposium on Haskell (Haskell ’16). Association for Computing Machinery, New York, NY, USA. 80–91. https://doi.org/10.1145/2976002.2976013
[45]
Uday S. Reddy. 1985. Narrowing as the Operational Semantics of Functional Languages. In Proceedings of the 1985 Symposium on Logic Programming (SLP ’85). IEEE-CS, Boston, Massachusetts, USA. 138–151.
[46]
Tillmann Rendel and Klaus Ostermann. 2010. Invertible Syntax Descriptions: Unifying Parsing and Pretty Printing. In Proceedings of the Third ACM Haskell Symposium on Haskell (Haskell ’10). Association for Computing Machinery, New York, NY, USA. 1–12. https://doi.org/10.1145/1863523.1863525
[47]
Alexander Romanenko. 1991. Inversion and Metacomputation. In Proceedings of the 1991 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’91). Association for Computing Machinery, New York, NY, USA. 12–22. https://doi.org/10.1145/115865.115868
[48]
Tom Schrijvers, Simon Peyton Jones, Manuel Chakravarty, and Martin Sulzmann. 2008. Type Checking with Open Type Functions. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP ’08). Association for Computing Machinery, New York, NY, USA. 51–62. https://doi.org/10.1145/1411204.1411215
[49]
Neil Sculthorpe, Jan Bracker, George Giorgidze, and Andy Gill. 2013. The Constrained-Monad Problem. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13). Association for Computing Machinery, New York, NY, USA. 287–298. https://doi.org/10.1145/2500365.2500602
[50]
Silvija Seres and Michael Spivey. 1999. Embedding Prolog in Haskell. In Proceedings of the 1999 Haskell Workshop (Haskell ’99).
[51]
Peter Sestoft. 1996. ML Pattern Match Compilation and Partial Evaluation. In Partial Evaluation, Olivier Danvy, Robert Glück, and Peter Thiemann (Eds.). Springer-Verlag, Berlin, Heidelberg. 446–464. isbn:978-3-540-70589-5 https://doi.org/10.1007/3-540-61580-6_22
[52]
Tim Sheard and Simon Peyton Jones. 2002. Template Meta-Programming for Haskell. In Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell (Haskell ’02). Association for Computing Machinery, New York, NY, USA. 1–16. isbn:1-58113-605-6 https://doi.org/10.1145/581690.581691
[53]
Saurabh Srivastava, Sumit Gulwani, Swarat Chaudhuri, and Jeffrey S. Foster. 2011. Path-Based Inductive Synthesis for Program Inversion. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’11). Association for Computing Machinery, New York, NY, USA. 492–503. https://doi.org/10.1145/1993498.1993557
[54]
Jan Stolarek, Simon Peyton Jones, and Richard A. Eisenberg. 2015. Injective Type Families for Haskell. In Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell (Haskell ’15). Association for Computing Machinery, New York, NY, USA. 118–128. https://doi.org/10.1145/2804302.2804314
[55]
Philip Wadler. 1985. How to Replace Failure by a List of Successes: A Method for Exception Handling, Backtracking, and Pattern Matching in Lazy Functional Languages. In Proceedings of a Conference on Functional Programming Languages and Computer Architecture (FPCA ’85). Springer-Verlag, Berlin, Heidelberg. 113–128.
[56]
Philip Wadler. 1987. Efficient Compilation of Pattern-Matching. In The Implementation of Functional Programming Languages, Simon L. Peyton Jones (Ed.). Prentice-Hall, 78–103. https://doi.org/10.1016/0141-9331(87)90510-2
[57]
Philip Wadler. 1987. Views: A Way for Pattern Matching to Cohabit with Data Abstraction. In Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL ’87). Association for Computing Machinery, New York, NY, USA. 307–313. https://doi.org/10.1145/41625.41653
[58]
Philip Wadler. 1990. Comprehending Monads. In Proceedings of the 1990 ACM Conference on LISP and Functional Programming (LFP ’90). Association for Computing Machinery, New York, NY, USA. 61–78. https://doi.org/10.1145/91556.91592
[59]
Philip Wadler and Stephen Blott. 1989. How to Make Ad-Hoc Polymorphism Less Ad Hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’89). Association for Computing Machinery, New York, NY, USA. 60–76. https://doi.org/10.1145/75277.75283
[60]
Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhães. 2012. Giving Haskell a Promotion. In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI ’12). Association for Computing Machinery, New York, NY, USA. 53–66. https://doi.org/10.1145/2103786.2103795

Cited By

View all
  • (2024)Example-Based Reasoning about the Realizability of Polymorphic ProgramsProceedings of the ACM on Programming Languages10.1145/36746368:ICFP(317-337)Online publication date: 15-Aug-2024
  • (2023)Embedding Functional Logic Programming in Haskell via a Compiler PluginPractical Aspects of Declarative Languages10.1007/978-3-031-24841-2_3(37-55)Online publication date: 16-Jan-2023

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
Haskell 2021: Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell
August 2021
135 pages
ISBN:9781450386159
DOI:10.1145/3471874
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 2021

Permissions

Request permissions for this article.

Check for updates

Badges

Author Tags

  1. GHC plugin
  2. Haskell
  3. inversion
  4. monadic transformation
  5. partial inversion
  6. pattern matching

Qualifiers

  • Research-article

Conference

ICFP '21
Sponsor:

Acceptance Rates

Overall Acceptance Rate 57 of 143 submissions, 40%

Upcoming Conference

ICFP '25
ACM SIGPLAN International Conference on Functional Programming
October 12 - 18, 2025
Singapore , Singapore

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)27
  • Downloads (Last 6 weeks)3
Reflects downloads up to 06 Jan 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Example-Based Reasoning about the Realizability of Polymorphic ProgramsProceedings of the ACM on Programming Languages10.1145/36746368:ICFP(317-337)Online publication date: 15-Aug-2024
  • (2023)Embedding Functional Logic Programming in Haskell via a Compiler PluginPractical Aspects of Declarative Languages10.1007/978-3-031-24841-2_3(37-55)Online publication date: 16-Jan-2023

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media