Jeremy-g: /* Breadth-First Traversal Via Staging */

2023-04-08T16:22:00Z

Breadth-First Traversal Via Staging

← Older revision		Revision as of 18:22, 8 April 2023
Line 6:		Line 6:
	An effectful traversal of a data structure iterates over every element, in some predetermined order, collecting computational effects in the process. Depth-first effectful traversal of a tree is straightforward to define compositionally, since it precisely follows the shape of the data. What about breadth-first effectful traversal? An indirect route is to factorize the data structure into shape and contents, traverse the contents, then rebuild the data structure with new contents. We show that this can instead be done directly using staging, expressed using a construction related to free applicative functors. The staged traversals lend themselves well to fusion; we prove a novel fusion rule for effectful traversals, and use it in another solution to Bird's "repmin" problem.		An effectful traversal of a data structure iterates over every element, in some predetermined order, collecting computational effects in the process. Depth-first effectful traversal of a tree is straightforward to define compositionally, since it precisely follows the shape of the data. What about breadth-first effectful traversal? An indirect route is to factorize the data structure into shape and contents, traverse the contents, then rebuild the data structure with new contents. We show that this can instead be done directly using staging, expressed using a construction related to free applicative functors. The staged traversals lend themselves well to fusion; we prove a novel fusion rule for effectful traversals, and use it in another solution to Bird's "repmin" problem.

	~~Slides~~ and [https://www.cs.ox.ac.uk/publications/publication14875-abstract.html paper].		[[File:M22-Gibbons.pdf]] and [https://www.cs.ox.ac.uk/publications/publication14875-abstract.html paper].

Jeremy-g: Created page with " == Breadth-First Traversal Via Staging == Jeremy Gibbons (joint work with Oisin Kidney, Tom Schrijvers, Nick Wu) An effectful traversal of a data structure iterates over ev..."

2023-04-08T16:19:46Z

Created page with " == Breadth-First Traversal Via Staging == Jeremy Gibbons (joint work with Oisin Kidney, Tom Schrijvers, Nick Wu) An effectful traversal of a data structure iterates over ev..."

New page

== Breadth-First Traversal Via Staging ==

Jeremy Gibbons (joint work with Oisin Kidney, Tom Schrijvers, Nick Wu)

An effectful traversal of a data structure iterates over every element, in some predetermined order, collecting computational effects in the process. Depth-first effectful traversal of a tree is straightforward to define compositionally, since it precisely follows the shape of the data. What about breadth-first effectful traversal? An indirect route is to factorize the data structure into shape and contents, traverse the contents, then rebuild the data structure with new contents. We show that this can instead be done directly using staging, expressed using a construction related to free applicative functors. The staged traversals lend themselves well to fusion; we prove a novel fusion rule for effectful traversals, and use it in another solution to Bird's "repmin" problem.

Slides and [https://www.cs.ox.ac.uk/publications/publication14875-abstract.html paper].

WG211/M22Gibbons - Revision history

Jeremy-g: /* Breadth-First Traversal Via Staging */

Jeremy-g: Created page with " == Breadth-First Traversal Via Staging == Jeremy Gibbons (joint work with Oisin Kidney, Tom Schrijvers, Nick Wu) An effectful traversal of a data structure iterates over ev..."