Abstract
The array-computational model pioneered by Iverson’s languages APL and J offers a simple and expressive solution to the “von Neumann bottleneck.” It includes a form of rank, or dimensional, polymorphism, which renders much of a program’s control structure implicit by lifting base operators to higher-dimensional array structures. We present the first formal semantics for this model, along with the first static type system that captures the full power of the core language.
The formal dynamic semantics of our core language, Remora, illuminates several of the murkier corners of the model. This allows us to resolve some of the model’s ad hoc elements in more general, regular ways. Among these, we can generalise the model from SIMD to MIMD computations, by extending the semantics to permit functions to be lifted to higher-dimensional arrays in the same way as their arguments.
Our static semantics, a dependent type system of carefully restricted power, is capable of describing array computations whose dimensions cannot be determined statically. The type-checking problem is decidable and the type system is accompanied by the usual soundness theorems. Our type system’s principal contribution is that it serves to extract the implicit control structure that provides so much of the language’s expressive power, making this structure explicitly apparent at compile time.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Backus, J.: Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs. Commun. ACM 21(8), 613–641 (1978)
Blelloch, G.: NESL: A nested data-parallel language (version 3.1). Tech. rep. (1995)
Blelloch, G., Chatterjee, S., Hardwick, J.C., Sipelstein, J., Zagha, M.: Implementation of a portable nested data-parallel language. Journal of Parallel and Distributed Computing 21, 102–111 (1994)
Brooks, F.P.: The Design of Design: Essays from a Computer Scientist. Addison-Wesley (2010)
Chakravarty, M.M.T., Leshchinskiy, R., Peyton Jones, S., Keller, G., Marlow, S.: Data parallel haskell: a status report. In: DAMP 2007: Workshop on Declarative Aspects of Multicore Programming, ACM Press (2007)
Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex, 1st edn. MIT Press (2009)
Iverson, K.E.: A programming language. John Wiley & Sons, Inc., New York (1962)
Jay, C.B.: The fish language definition. Tech. rep. (1998)
Jay, C.B., Cockett, J.: Shapely types and shape polymorphism. In: Sannella, D. (ed.) ESOP 1994. LNCS, vol. 788, pp. 302–316. Springer, Heidelberg (1994)
Jsoftware, Inc.: Jsoftware: High-performance development platform, http://www.jsoftware.com/
Keller, G., Chakravarty, M.M., Leshchinskiy, R., Peyton Jones, S., Lippmeier, B.: Regular, shape-polymorphic, parallel arrays in haskell. In: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, pp. 261–272. ACM, New York (2010)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)
Peyton Jones, S., Leshchinskiy, R., Keller, G., Chakravarty, M.M.: Harnessing the multicores: Nested data parallelism in haskell. In: FSTTCS, vol. 2, pp. 383–414 (2008)
Ragan-Kelley, J., Adams, A., Paris, S., Levoy, M., Amarasinghe, S., Durand, F.: Decoupling algorithms from schedules for easy optimization of image processing pipelines. ACM Trans. Graph. 31(4), 32:1–32:12 (2012)
Scholz, S.B.: Single assignment c: efficient support for high-level array operations in a functional setting. J. Funct. Program. 13(6), 1005–1059 (2003)
Thatte, S.: A type system for implicit scaling. Sci. Comput. Program. 17(1-3), 217–245 (1991), http://dx.doi.org/10.1016/0167-64239190040-5
Trojahner, K., Grelck, C.: Dependently typed array programs don’t go wrong. Journal of Logic and Algebraic Programming 78(7), 643–664 (2009)
Xi, H.: Dependent types in practical programming. Ph.D. thesis, Pittsburgh, PA, USA (1998) aAI9918624
Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation, PLDI 1998, pp. 249–257. ACM, New York (1998)
Zima, H., Chapman, B.: Supercompilers for Parallel and Vector Computers. ACM Press (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Slepak, J., Shivers, O., Manolios, P. (2014). An Array-Oriented Language with Static Rank Polymorphism. In: Shao, Z. (eds) Programming Languages and Systems. ESOP 2014. Lecture Notes in Computer Science, vol 8410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54833-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-54833-8_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54832-1
Online ISBN: 978-3-642-54833-8
eBook Packages: Computer ScienceComputer Science (R0)