Document Open Access Logo

NumLin: Linear Types for Linear Algebra

Authors Dhruv C. Makwana , Neelakantan R. Krishnaswami

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2019.14.pdf
  • Filesize: 0.73 MB
  • 25 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Program specifications
Keywords
  • numerical
  • linear
  • algebra
  • types
  • permissions
  • OCaml

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We present NumLin, a functional programming language whose type system is designed to enforce the safe usage of the APIs of low-level linear algebra libraries (such as BLAS/LAPACK). We do so through a brief description of its key features and several illustrative examples. We show that NumLin’s type system is sound and that its implementation improves upon naïve implementations of linear algebra programs, almost towards C-levels of performance. By doing so, we demonstrate (a) that linear types are well-suited to expressing the APIs of low-level linear algebra libraries accurately and concisely and (b) that, despite the complexity of prior work on it, fractional permissions can actually be implemented using simple, well-known techniques and be used practically in real programs.

Cite As Get BibTex

Dhruv C. Makwana and Neelakantan R. Krishnaswami. NumLin: Linear Types for Linear Algebra. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 14:1-14:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ECOOP.2019.14

Author Details

Dhruv C. Makwana
  • Unaffiliated
Neelakantan R. Krishnaswami
  • Department of Computer Science and Technology, University of Cambridge, United Kingdom

Acknowledgements

We would like to thank Stephen Dolan for his advice and support with the implementation and evaluation of NumLin. We would also like to thank the (anonymous) reviewers for their feedback and suggestions.

Supplementary Materials

References

  1. Akinori Abe and Eijiro Sumii. A simple and practical linear algebra library interface with static size checking. arXiv preprint, 2015. URL: http://arxiv.org/abs/1512.01898.
  2. Amal Ahmed, Matthew Fluet, and Greg Morrisett. L\^ 3: a linear language with locations. Fundamenta Informaticae, 77(4):397-449, 2007. Google Scholar
  3. Andrew Barber and Gordon Plotkin. Dual intuitionistic linear logic. University of Edinburgh, Department of Computer Science, Laboratory for …, 1996. Google Scholar
  4. Henrik Barthels, Marcin Copik, and Paolo Bientinesi. The generalized matrix chain algorithm. arXiv preprint, 2018. URL: http://arxiv.org/abs/1804.04021.
  5. P Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Computer Science Logic, pages 121-135. Springer, 1995. Google Scholar
  6. Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R Newton, Simon Peyton Jones, and Arnaud Spiwack. Linear Haskell: practical linearity in a higher-order polymorphic language. Procedings of the ACM on Programming Languages, 2(POPL):5, 2017. Google Scholar
  7. Jean-Philippe Bernardy, Vıctor López Juan, and Josef Svenningsson. Composable efficient array computations using linear types. Unpublished Draft, 2016. Google Scholar
  8. Kevin Bierhoff and Jonathan Aldrich. PLURAL: checking protocol compliance under aliasing. In Companion of the 30th international conference on Software engineering, pages 971-972. ACM, 2008. Google Scholar
  9. Kevin Bierhoff, Nels E Beckman, and Jonathan Aldrich. Fraction Polymorphic Permission Inference. Google Scholar
  10. Richard Bornat, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. Permission accounting in separation logic. In ACM SIGPLAN Notices, volume 40 (1), pages 259-270. ACM, 2005. Google Scholar
  11. John Boyland. Checking interference with fractional permissions. In International Static Analysis Symposium, pages 55-72. Springer, 2003. Google Scholar
  12. Alex Bronstein, Yoni Choukroun, Ron Kimmel, and Matan Sela. Consistent discretization and minimization of the l1 norm on manifolds. In 3D Vision (3DV), 2016 Fourth International Conference on, pages 435-440. IEEE, 2016. Google Scholar
  13. Sa Cui, Kevin Donnelly, and Hongwei Xi. Ats: A language that combines programming with theorem proving. In International Workshop on Frontiers of Combining Systems, pages 310-320. Springer, 2005. Google Scholar
  14. Troels Henriksen, Niels GW Serup, Martin Elsman, Fritz Henglein, and Cosmin E Oancea. Futhark: purely functional GPU-programming with nested parallelism and in-place array updates. ACM SIGPLAN Notices, 52(6):556-571, 2017. Google Scholar
  15. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. RustBelt: securing the foundations of the rust programming language. PACMPL, 2(POPL):66:1-66:34, 2018. URL: http://dx.doi.org/10.1145/3158154.
  16. Rudolph Emil Kalman. A new approach to linear filtering and prediction problems. Journal of basic Engineering, 82(1):35-45, 1960. Google Scholar
  17. Conor McBride. Code Mesh London 2016, Keynote: SpaceMonads. https://www.youtube.com/watch?v=QojLQY5H0RI. Accessed: 08/05/2018.
  18. Matthew Rocklin. Mathematically informed linear algebra codes through term rewriting, 2013. Google Scholar
  19. Sven-Bodo Scholz. Single Assignment C: efficient support for high-level array operations in a functional setting. Journal of functional programming, 13(6):1005-1059, 2003. Google Scholar
  20. Philip Wadler. Linear Types Can Change the World. In M. Broy and C. B. Jones, editors, IFIP TC 2 Working Conference on Programming Concepts and Methods, pages 561-581, Sea of Gallilee, Israel, April 1990. North-Holland. Google Scholar
  21. Aaron Weiss, Daniel Patterson, and Amal Ahmed. Rust Distilled: An Expressive Tower of Languages. arXiv preprint, 2018. URL: http://arxiv.org/abs/1806.02693.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact