2.2.11
Causal commutative arrows and their optimization
Causal commutative arrows and their optimization, by Hai Liu, Eric Cheng, and Paul Hudak, ICFP 2009.
Extends arrows with two widely used concepts, loop and init. Both concepts arise quite often. Proves a normalisation theorem that reduces any program to a single use of loop, and show that in practice this can yield a speedup of two orders of magnitude. Lovely result!
As the paper notes in passing, 'loop' is closely related to the concept of 'trace' from category theory. Phil Scott is currently visiting Edinburgh, and I'm hoping he, Jeff Eggers, and I might explore the relation betwixt 'trace' and 'loop'.
An compelling example of the value of 'loop' and 'init' is the definition of integral:
This definition is valid for a stream of events, where each event is separated uniformly by time dt. An intriguing question is how to define integral in a similar style when the time between events is not uniform? Or for continuous behaviours rather than discrete events?
Extends arrows with two widely used concepts, loop and init. Both concepts arise quite often. Proves a normalisation theorem that reduces any program to a single use of loop, and show that in practice this can yield a speedup of two orders of magnitude. Lovely result!
As the paper notes in passing, 'loop' is closely related to the concept of 'trace' from category theory. Phil Scott is currently visiting Edinburgh, and I'm hoping he, Jeff Eggers, and I might explore the relation betwixt 'trace' and 'loop'.
An compelling example of the value of 'loop' and 'init' is the definition of integral:
integral = loop (arr (\ (v,i) -> i + dt * v) >>> init 0 >>> arr (\ i -> (i,i)))
This definition is valid for a stream of events, where each event is separated uniformly by time dt. An intriguing question is how to define integral in a similar style when the time between events is not uniform? Or for continuous behaviours rather than discrete events?
