Agda Meets Accelerate

Peter Thiemann and Manuel M. T. Chakravarty.

In 24th Symposium on Implementation and Application of Functional Languages (IFL 2012), Revised Papers, Spinger Verlag, LNCS 8241, 2013.

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.

PDF (16 pages)

This page is part of Manuel Chakravarty's WWW-stuff.