Dependently typed array programs don’t go wrong. (English) Zbl 1187.68320
Summary: The array programming paradigm adopts multidimensional arrays as the fundamental data structures of computation. Array operations process entire arrays instead of just single elements. This makes array programs highly expressive and introduces data parallelism in a natural way. Array programming imposes non-trivial structural constraints on ranks, shapes, and element values of arrays. A prominent example where such constraints are violated are out-of-bound array accesses. Usually, such constraints are enforced by means of run time checks. Both the run time overhead inflicted by dynamic constraint checking and the uncertainty of proper program evaluation are undesirable.
We propose a novel type system for array programs based on dependent types. Our type system makes dynamic constraint checks obsolete and guarantees orderly evaluation of well-typed programs. We employ integer vectors of statically unknown length to index array types. We also show how constraints on these vectors are resolved using a suitable reduction to integer scalars. Our presentation is based on a functional array calculus that captures the essence of the paradigm without the legacy and obfuscation of a fully-fledged array programming language.
We propose a novel type system for array programs based on dependent types. Our type system makes dynamic constraint checks obsolete and guarantees orderly evaluation of well-typed programs. We employ integer vectors of statically unknown length to index array types. We also show how constraints on these vectors are resolved using a suitable reduction to integer scalars. Our presentation is based on a functional array calculus that captures the essence of the paradigm without the legacy and obfuscation of a fully-fledged array programming language.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68N99 | Theory of software |
References:
| [1] | Sutter, H., A fundamental turn toward concurrency in software, Dr. Dobb’s J., 30, 3 (2005) |
| [2] | Grelck, C., Shared memory multiprocessor support for functional array processing in SAC, J. Funct. Programming, 15, 3, 353-401 (2005) · Zbl 1085.68548 |
| [3] | Iverson, K., A Programming Language (1962), John Wiley: John Wiley New York City, NY, USA · Zbl 0101.34503 |
| [4] | Iverson, K., J Introduction and Dictionary (1995), Iverson Software Inc.: Iverson Software Inc. Toronto, Canada |
| [5] | C. Moler, J. Little, S. Bangert, Pro-Matlab User’s Guide, The MathWorks, Cochituate Place, 24 Prime Park Way, Natick, MA, USA, 1987.; C. Moler, J. Little, S. Bangert, Pro-Matlab User’s Guide, The MathWorks, Cochituate Place, 24 Prime Park Way, Natick, MA, USA, 1987. |
| [6] | Grelck, C.; Scholz, S.-B., SAC: a functional array language for efficient multithreaded execution, Internat. J. Parallel Programming, 34, 4, 383-427 (2006) · Zbl 1102.68438 |
| [7] | C. Grelck, S.-B. Scholz, A. Shafarenko, A binding scope analysis for generic programs on arrays, in: A. Butterfield (Ed.), Implementation and Application of Functional Languages, 17th International Workshop (IFL’05), Dublin, Ireland, September 19-21, 2005, Revised Selected Papers, Lecture Notes in Computer Science, vol. 4015, Springer-Verlag, Berlin, Heidelberg, New York, 2006, pp. 212-230.; C. Grelck, S.-B. Scholz, A. Shafarenko, A binding scope analysis for generic programs on arrays, in: A. Butterfield (Ed.), Implementation and Application of Functional Languages, 17th International Workshop (IFL’05), Dublin, Ireland, September 19-21, 2005, Revised Selected Papers, Lecture Notes in Computer Science, vol. 4015, Springer-Verlag, Berlin, Heidelberg, New York, 2006, pp. 212-230. · Zbl 1236.68029 |
| [8] | S. Herhut, S.-B. Scholz, R. Bernecky, C. Grelck, K. Trojahner, From contracts towards dependent types: proofs by partial evaluation, in: O. Chitil, Z. Horváth, V. Zsók (Eds.), Proceedings of the 19th International Symposium on Implementation and Application of Functional Languages (IFL’07), Freiburg, Germany, Revised Selected Papers, Lecture Notes in Computer Science, vol. 5083, Springer-Verlag, Berlin, Heidelberg, New York, 2008, pp. 254-273.; S. Herhut, S.-B. Scholz, R. Bernecky, C. Grelck, K. Trojahner, From contracts towards dependent types: proofs by partial evaluation, in: O. Chitil, Z. Horváth, V. Zsók (Eds.), Proceedings of the 19th International Symposium on Implementation and Application of Functional Languages (IFL’07), Freiburg, Germany, Revised Selected Papers, Lecture Notes in Computer Science, vol. 5083, Springer-Verlag, Berlin, Heidelberg, New York, 2008, pp. 254-273. |
| [9] | H. Xi, F. Pfenning, Eliminating array bound checking through dependent types, in: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, Montreal, 1998, pp. 249-257.; H. Xi, F. Pfenning, Eliminating array bound checking through dependent types, in: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, Montreal, 1998, pp. 249-257. |
| [10] | Zenger, C., Indexed types, Theoret. Comput. Sci., 187, 1-2, 147-165 (1997) · Zbl 0893.68086 |
| [11] | Xi, H.; Pfenning, F., Dependent types in practical programming, (Aiken, A., Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’99), San Antonio, Texas, USA (1999), ACM Press), 214-227 |
| [12] | Pierce, B., Types and Programming Languages (2002), MIT Press: MIT Press Cambridge, MA, USA · Zbl 0995.68018 |
| [13] | K. Trojahner, C. Grelck, Dependently typed array programs don’t go wrong, Tech. Rep. A-08-06, Schriftenreihe der Institute für Informatik/Mathematik, University of Lübeck, Lübeck, Germany, 2008. <http://www.isp.uni-luebeck.de/papers/2008/dtapdgw-tr08.pdf>.; K. Trojahner, C. Grelck, Dependently typed array programs don’t go wrong, Tech. Rep. A-08-06, Schriftenreihe der Institute für Informatik/Mathematik, University of Lübeck, Lübeck, Germany, 2008. <http://www.isp.uni-luebeck.de/papers/2008/dtapdgw-tr08.pdf>. · Zbl 1187.68320 |
| [14] | Dutertre, B.; de Moura, L., A fast linear-arithmetic solver for DPLL(T), (Ball, T.; Jones, R. B., Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings. Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4144 (2006), Springer Verlag: Springer Verlag Berlin, Heidelberg), 81-94 |
| [15] | Bradley, A. R.; Manna, Z.; Sipma, H. B., What’s decidable about arrays?, (Emerson, E. A.; Namjoshi, K. S., Verification, Model Checking, and Abstract Interpretation, Seventh International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings. Verification, Model Checking, and Abstract Interpretation, Seventh International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, Lecture Notes in Computer Science, vol. 3855 (2006), Springer Verlag: Springer Verlag Berlin, Heidelberg), 427-442 · Zbl 1176.68116 |
| [16] | Falkoff, A.; Iverson, K., The design of APL, IBM J. Res. Develop., 17, 4, 324-334 (1973) · Zbl 0263.68005 |
| [17] | Jenkins, M., Q’Nial: a portable interpreter for the nested interactive array language, Nial, Software Pract. Exp., 19, 2, 111-126 (1989) |
| [18] | Jay, C.; Steckler, P., The functional imperative: shape!, (Hankin, C., Proceedings of the Seventh European Symposium on Programming (ESOP’98), Part of the Joint European Conference on Theory and Practice of Software (ETAPS��98), Lisbon, Portugal. Proceedings of the Seventh European Symposium on Programming (ESOP’98), Part of the Joint European Conference on Theory and Practice of Software (ETAPS’98), Lisbon, Portugal, Lecture Notes in Computer Science, vol. 1381 (1998), Springer Verlag: Springer Verlag Berlin, Germany), 139-153 |
| [19] | de Rose, L.; Padua, D., Techniques for the translation of MATLAB programs into Fortran 90, ACM Trans. Programming Lang. Syst., 21, 2, 286-323 (1999) |
| [20] | C. McCosh, Type-based specialization in a telescoping compiler for MATLAB, Master Thesis TR03-412, Rice University, Houston, Texas, USA, 2003.; C. McCosh, Type-based specialization in a telescoping compiler for MATLAB, Master Thesis TR03-412, Rice University, Houston, Texas, USA, 2003. |
| [21] | Joisha, P.; Banerjee, P., An algebraic array shape inference system for MATLAB, ACM Trans. Programming Lang. Syst., 28, 5, 848-907 (2006) |
| [22] | Cann, D., Retire Fortran? A debate rekindled, Comm. ACM, 35, 8, 1-89 (1992) |
| [23] | Blelloch, G., Programming parallel algorithms, Comm. ACM, 39, 3, 85-97 (1996) |
| [24] | Chakravarty, M. M.; Keller, G., An approach to fast arrays in Haskell, (Jeuring, J.; Jones, S. P., Summer School and Workshop on Advanced Functional Programming, Oxford, England, UK, 2002. Summer School and Workshop on Advanced Functional Programming, Oxford, England, UK, 2002, Lecture Notes in Computer Science, vol. 2638 (2003), Springer Verlag: Springer Verlag Berlin, Germany), 27-58 · Zbl 1278.68057 |
| [25] | Chakravarty, M. M.T.; Leshchinskiy, R.; Peyton Jones, S.; Keller, G.; Marlow, S., Data parallel Haskell: a status report, (DAMP ’07: Proceedings of the 2007 Workshop on Declarative Aspects of Multicore Programming (2007), ACM Press: ACM Press New York, NY, USA), 10-18 |
| [26] | Smith, J.; Nordström, B.; Petersson, K., Programming in Martin-Löf’s Type Theory (1990), Oxford University Press · Zbl 0744.03029 |
| [27] | Augustsson, L., Cayenne – a language with dependent types, (International Conference on Functional Programming (1998), ACM: ACM New York, NY, USA), 239-250 · Zbl 1369.68085 |
| [28] | McBride, C.; McKinna, J., The view from the left, J. Funct. Programming, 14, 1, 69-111 (2004) · Zbl 1069.68539 |
| [29] | T. Altenkirch, C. McBride, J. McKinna, Why dependent types matter (April 2005). <http://www.cs.nott.ac.uk/\( \sim\) txa/publ/ydtm.pdf>.; T. Altenkirch, C. McBride, J. McKinna, Why dependent types matter (April 2005). <http://www.cs.nott.ac.uk/\( \sim\) txa/publ/ydtm.pdf>. |
| [30] | Nanevski, A.; Morrisett, G.; Birkedal, L., Polymorphism and separation in Hoare type theory, (International Conference on Functional Programming (2006), ACM Press: ACM Press New York, NY, USA), 62-73 · Zbl 1321.68351 |
| [31] | H. Xi, Applied type system (extended abstract), in: S. Baradi, M. Coppo, F. Damiani (Eds.), Types for Proofs and Programs, Third International Workshop, TYPES 2003, Torino, Italy, April 30-May 4, 2003, Revised Selected Papers, Lecture Notes in Computer Science, vol. 3085, Springer Verlag, Berlin, Germany, 2004, pp. 394-408.; H. Xi, Applied type system (extended abstract), in: S. Baradi, M. Coppo, F. Damiani (Eds.), Types for Proofs and Programs, Third International Workshop, TYPES 2003, Torino, Italy, April 30-May 4, 2003, Revised Selected Papers, Lecture Notes in Computer Science, vol. 3085, Springer Verlag, Berlin, Germany, 2004, pp. 394-408. · Zbl 1100.03518 |
| [32] | Büther, F., A Compiler for Qube, A Functional Array Programming Language with Dependent Types, Studienarbeit, Institute for Software Technology and Programming Languages (2008), University of Lübeck: University of Lübeck Lübeck, Germany |
| [33] | M. Weigel, Facilitating array programming with dependent types – precise error messages and implicit index arguments for Qube, Master’s thesis, Institute for Software Technology and Programming Languages, University of Lübeck, Lübeck, Germany, 2008.; M. Weigel, Facilitating array programming with dependent types – precise error messages and implicit index arguments for Qube, Master’s thesis, Institute for Software Technology and Programming Languages, University of Lübeck, Lübeck, Germany, 2008. |
| [34] | Scholz, S.-B., WITH-loop-folding: condensing consecutive array operations, (Clack, C.; Davie, T.; Hammond, K., Proceedings of the Ninth International Workshop on Implementation of Functional Languages (IFL’97), St. Andrews, Scotland, UK (1997), University of St. Andrews), 225-242 |
| [35] | C.Grelck, K. Trojahner, Implicit memory management for SAC, in: C.Grelck, F. Huch (Eds.), Proceedings of the 16th International Workshop on Implementation and Application of Functional Languages, IFL 2004, Lübeck, Germany, September 8-10, 2004, Technical Report, vol. 0408, University of Kiel, 2004, pp. 335-348.; C.Grelck, K. Trojahner, Implicit memory management for SAC, in: C.Grelck, F. Huch (Eds.), Proceedings of the 16th International Workshop on Implementation and Application of Functional Languages, IFL 2004, Lübeck, Germany, September 8-10, 2004, Technical Report, vol. 0408, University of Kiel, 2004, pp. 335-348. · Zbl 1119.68008 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
