Kan Extensions for Program Optimisation—Or: Art and Dan Explain an Old Trick
Many program optimisations involve transforming a program in direct style to an equivalent program in continuation-passing style. This paper investigates the theoretical underpinnings of this transformation in the categorical setting of monads. We argue that so-called absolute Kan Extensions underli...
| Main Author: | |
|---|---|
| Format: | Conference item |
| Published: |
Springer Berlin / Heidelberg
2012
|
| _version_ | 1826305933115916288 |
|---|---|
| author | Hinze, R |
| author_facet | Hinze, R |
| author_sort | Hinze, R |
| collection | OXFORD |
| description | Many program optimisations involve transforming a program in direct style to an equivalent program in continuation-passing style. This paper investigates the theoretical underpinnings of this transformation in the categorical setting of monads. We argue that so-called absolute Kan Extensions underlie this program optimisation. It is known that every Kan extension gives rise to a monad, the codensity monad, and furthermore that every monad is isomorphic to a codensity monad. The end formula for Kan extensions then induces an implementation of the monad, which can be seen as the categorical counterpart of continuation-passing style. We show that several optimisations are instances of this scheme: Church representations and implementation of backtracking using success and failure continuations, among others. Furthermore, we develop the calculational properties of Kan extensions, powers and ends. In particular, we propose a two-dimensional notation based on string diagrams that aims to support effective reasoning with Kan extensions. |
| first_indexed | 2024-03-07T06:40:19Z |
| format | Conference item |
| id | oxford-uuid:f90fee56-d21d-406f-8982-d43cd94b289f |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:40:19Z |
| publishDate | 2012 |
| publisher | Springer Berlin / Heidelberg |
| record_format | dspace |
| spelling | oxford-uuid:f90fee56-d21d-406f-8982-d43cd94b289f2022-03-27T12:55:03ZKan Extensions for Program Optimisation—Or: Art and Dan Explain an Old TrickConference itemhttp://purl.org/coar/resource_type/c_5794uuid:f90fee56-d21d-406f-8982-d43cd94b289fDepartment of Computer ScienceSpringer Berlin / Heidelberg2012Hinze, RMany program optimisations involve transforming a program in direct style to an equivalent program in continuation-passing style. This paper investigates the theoretical underpinnings of this transformation in the categorical setting of monads. We argue that so-called absolute Kan Extensions underlie this program optimisation. It is known that every Kan extension gives rise to a monad, the codensity monad, and furthermore that every monad is isomorphic to a codensity monad. The end formula for Kan extensions then induces an implementation of the monad, which can be seen as the categorical counterpart of continuation-passing style. We show that several optimisations are instances of this scheme: Church representations and implementation of backtracking using success and failure continuations, among others. Furthermore, we develop the calculational properties of Kan extensions, powers and ends. In particular, we propose a two-dimensional notation based on string diagrams that aims to support effective reasoning with Kan extensions. |
| spellingShingle | Hinze, R Kan Extensions for Program Optimisation—Or: Art and Dan Explain an Old Trick |
| title | Kan Extensions for Program Optimisation—Or: Art and Dan Explain an Old Trick |
| title_full | Kan Extensions for Program Optimisation—Or: Art and Dan Explain an Old Trick |
| title_fullStr | Kan Extensions for Program Optimisation—Or: Art and Dan Explain an Old Trick |
| title_full_unstemmed | Kan Extensions for Program Optimisation—Or: Art and Dan Explain an Old Trick |
| title_short | Kan Extensions for Program Optimisation—Or: Art and Dan Explain an Old Trick |
| title_sort | kan extensions for program optimisation or art and dan explain an old trick |
| work_keys_str_mv | AT hinzer kanextensionsforprogramoptimisationorartanddanexplainanoldtrick |