East of Eden: Parallel Functional Programming in Idris

Implicit parallel programming models typically give less parallelism control to the programmer, but require less specialised expertise. Explicit parallel models, on the other hand, give much greater parallelism control, but can require significant expertise from the programmer. In this paper, we introduce a novel semi-implicit parallel model, called Elysium, for Idris. Elysium therefore demonstrates semi-explicit parallelism for an emerging class of languages known as dependently-typed languages. These dependently-typed languages encourage safer software via their ability to express strong logical guarantees, in the form of proofs, directly in code.Our semi-implicit approach is based on a process model that uses dependent types to guarantee parallelism properties. We demonstrate how we can use this semi-implicit process model to build common algorithmic skeletons, including farms, pipelines and divide and conquer skeletons. We evaluate our process skeleton approach on a number of examples, achieving speedups of up to 22 on a 28-core machine.