scholarly journals Getting to the point: index sets and parallelism-preserving autodiff for pointful array programming

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-29
Author(s):  
Adam Paszke ◽  
Daniel D. Johnson ◽  
David Duvenaud ◽  
Dimitrios Vytiniotis ◽  
Alexey Radul ◽  
...  

We present a novel programming language design that attempts to combine the clarity and safety of high-level functional languages with the efficiency and parallelism of low-level numerical languages. We treat arrays as eagerly-memoized functions on typed index sets, allowing abstract function manipulations, such as currying, to work on arrays. In contrast to composing primitive bulk-array operations, we argue for an explicit nested indexing style that mirrors application of functions to arguments. We also introduce a fine-grained typed effects system which affords concise and automatically-parallelized in-place updates. Specifically, an associative accumulation effect allows reverse-mode automatic differentiation of in-place updates in a way that preserves parallelism. Empirically, we benchmark against the Futhark array programming language, and demonstrate that aggressive inlining and type-driven compilation allows array programs to be written in an expressive, "pointful" style with little performance penalty.

1994 ◽  
Vol 24 (1) ◽  
pp. 1-25 ◽  
Author(s):  
Brigham Bell ◽  
Wayne Citrin ◽  
Clayton Lewis ◽  
John Rieman ◽  
Robert Weaver ◽  
...  

2013 ◽  
Vol 23 (5) ◽  
pp. 552-593 ◽  
Author(s):  
EDWIN BRADY

AbstractMany components of a dependently typed programming language are by now well understood, for example, the underlying type theory, type checking, unification and evaluation. How to combine these components into a realistic and usable high-level language is, however, folklore, discovered anew by successive language implementors. In this paper, I describe the implementation ofIdris, a new dependently typed functional programming language.Idrisis intended to be ageneral-purposeprogramming language and as such provides high-level concepts such as implicit syntax, type classes anddonotation. I describe the high-level language and the underlying type theory, and present a tactic-based method forelaboratingconcrete high-level syntax with implicit arguments and type classes into a fully explicit type theory. Furthermore, I show how this method facilitates the implementation of new high-level language constructs.


Sign in / Sign up

Export Citation Format

Share Document