Skip to main content
SpringerLink
Log in

Agda Meets Accelerate

  • Conference paper
  • First Online:
Book cover Implementation and Application of Functional Languages (IFL 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8241))

Included in the following conference series:

Abstract

Embedded languages in Haskell benefit from a range of type extensions, such as type families, that are subsumed by dependent types. However, even with those type extensions, embedded languages for data parallel programming lack desirable static guarantees, such as static bounds checks in indexing and collective permutation operations.

This observation raises the question whether an embedded language for data parallel programming would benefit from fully-fledged dependent types, such as those available in Agda. We explored that question by designing and implementing an Agda frontend to Accelerate, a Haskell-embedded language for data parallel programming aimed at GPUs. We discuss the potential of dependent types in this domain, describe some of the limitations that we encountered, and share some insights from our preliminary implementation.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 72.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    An identifier can be an almost arbitrary string of Unicode characters except spaces, parentheses, and curly braces. Agda also supports mixfix syntax with the position of arguments indicated by underscores in the defining occurrence of an identifier.

  2. 2.

    To distinguish Haskell code from Agda code, we display Haskell code in a framed boxes.

  3. 3.

    Accelerate employs caching to avoid the transfer of arrays that are already available in GPU memory.

  4. 4.

    \(\top \) is a one-element type, whereas \(\bot \) is a type without elements. These types customarily represent truth and falsity.

  5. 5.

    In Agda, arguments in double curly braces are instance arguments [5] that are aggressively inferred. We use them like type class constraints in Haskell.

  6. 6.

    Recent work on Haskell’s type system manages to avoid this issue [19].

  7. 7.

    Accelerate currently does not support Maybe types as array elements.

References

  1. Bove, A., Dybjer, P., Norell, U.: A brief overview of agda - a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 73–78. Springer, Heidelberg (2009)

    Google Scholar 

  2. Catanzaro, B., Garland, M., Keutzer, K.: Copperhead: Compiling an embedded data parallel language. Technical Report UCB/EECS-2010-124. University of California, Berkeley (2010)

    Google Scholar 

  3. Chakravarty, M.M.T., Keller, G., Lee, S., McDonell, T.L., Grover, V.: Accelerating Haskell array codes with multicore GPUs. In: Carro, M., Reppy, J.H. (eds.) Workshop on Declarative Aspects of Multicore Programming, DAMP 2011, Austin, TX, USA, January 2011, pp. 3–14. ACM (2011)

    Google Scholar 

  4. Chakravarty, M.M.T., Keller, G., Peyton Jones, S.: Associated type synonyms. In: Pierce, B.C. (ed.) Proceedings International Conference on Functional Programming 2005, Tallinn, Estonia, September 2005, pp. 241–253. ACM Press, New York (2005)

    Google Scholar 

  5. Devriese, D., Piessens, F.: On the bright side of type classes: Instance arguments in Agda. In: Danvy, O. (ed.) Proceedings International Conference on Functional Programming 2011, Tokyo, Japan, September 2011, pp. 143–155. ACM Press, New York (2011)

    Google Scholar 

  6. Goldberg, D.: What every computer scientist should know about floating-point arithmetic. ACM Comput. Surv. 23(1), 5–48 (1991)

    Article  Google Scholar 

  7. Jones, S.L.P., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: Lawall, J. (ed.) ICFP, Portland, Oregon, USA, September 2006, pp. 50–61. ACM Press, New York (2006)

    Google Scholar 

  8. 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. ACM (2010)

    Google Scholar 

  9. Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis, Napoli (1984)

    MATH  Google Scholar 

  10. Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009)

    Google Scholar 

  11. Peebles, D.: A dependently typed model of the Repa library in Agda. https://github.com/copumpkin/derpa (2011)

  12. Rose, J.R., et al.: C\(^*\): An extended c language for data parallel programming. In: Proceedings of the Second International Conference on Supercomputing, pp. 2–16 (1987)

    Google Scholar 

  13. Saraswat, V.: Report on the programming language X10. http://dist.codehaus.org/x10/documentation/languagespec/x10-200.pdf. October 2009. Version 2.0

  14. Schrijvers, T., Peyton Jones, S.L., Chakravarty, M.M.T., Sulzmann, M.: Type checking with open type functions. In: Thiemann, P. (ed.) Proceedings International Conference on Functional Programming 2008, Victoria, BC, Canada, October 2008, pp. 51–62. ACM Press, New York (2008)

    Google Scholar 

  15. Swierstra, W.: More dependent types for distributed arrays. Higher-Order Symbolic Comput., pp. 1–18 (2010)

    Google Scholar 

  16. Swierstra, W., Altenkirch, T.: Dependent types for distributed arrays. In: Trends in Functional Programming, vol. 9 (2008)

    Google Scholar 

  17. Tarditi, D., Puri, S., Oglesby, J.: Accelerator: using data parallelism to program GPUs for general-purpose uses. In: ASPLOS-XII: Proceedings of the 12th International Conference on Architectural Support for Programming Language and Operating Systems, pp. 325–335. ACM (2006)

    Google Scholar 

  18. Xi, H.: Dependent ML: An approach to practical programming with dependent types. J. Funct. Program. 12(2) (2007)

    Google Scholar 

  19. Yorgey, B.A., Weirich, S., Cretin, J., Jones, S.L.P., Vytiniotis, D., Magalhães, J.P.: Giving Haskell a promotion. In: Pierce, B.C. (ed.) Proceedings of TLDI 2012, Philadelphia, PA, USA, January 2012, pp. 53–66. ACM (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Freiburg, Freiburg, Germany

    Peter Thiemann

  2. University of New South Wales, Sydney, Australia

    Manuel M. T. Chakravarty

Authors
  1. Peter Thiemann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Manuel M. T. Chakravarty
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peter Thiemann .

Editor information

Editors and Affiliations

  1. University of Oxford, Oxford, United Kingdom

    Ralf Hinze

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Thiemann, P., Chakravarty, M.M.T. (2013). Agda Meets Accelerate. In: Hinze, R. (eds) Implementation and Application of Functional Languages. IFL 2012. Lecture Notes in Computer Science(), vol 8241. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41582-1_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-41582-1_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-41581-4

  • Online ISBN: 978-3-642-41582-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation