Parametric polymorphism and operational improvement
Parametricity, in both operational and denotational forms, has long been a useful tool for reasoning about program correctness. However, there is as yet no comparable technique for reasoning about program improvement, that is, when one program uses fewer resources than another. Existing theories of...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Published: |
Association for Computing Machinery
2018
|
| Online Access: | https://eprints.nottingham.ac.uk/52868/ |
| _version_ | 1848798828166119424 |
|---|---|
| author | Hackett, Jennifer Hutton, Graham |
| author_facet | Hackett, Jennifer Hutton, Graham |
| author_sort | Hackett, Jennifer |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Parametricity, in both operational and denotational forms, has long been a useful tool for reasoning about program correctness. However, there is as yet no comparable technique for reasoning about program improvement, that is, when one program uses fewer resources than another. Existing theories of parametricity cannot be used to address this problem as they are agnostic with regard to resource usage. This article addresses this problem by presenting a new operational theory of parametricity that is sensitive to time costs, which can be used to reason about time improvement properties. We demonstrate the applicability of our theory by showing how it can be used to prove that a number of well-known program fusion techniques are time improvements, including fixed point fusion, map fusion and short cut fusion. |
| first_indexed | 2025-11-14T20:25:58Z |
| format | Article |
| id | nottingham-52868 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T20:25:58Z |
| publishDate | 2018 |
| publisher | Association for Computing Machinery |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-528682020-05-04T19:45:26Z https://eprints.nottingham.ac.uk/52868/ Parametric polymorphism and operational improvement Hackett, Jennifer Hutton, Graham Parametricity, in both operational and denotational forms, has long been a useful tool for reasoning about program correctness. However, there is as yet no comparable technique for reasoning about program improvement, that is, when one program uses fewer resources than another. Existing theories of parametricity cannot be used to address this problem as they are agnostic with regard to resource usage. This article addresses this problem by presenting a new operational theory of parametricity that is sensitive to time costs, which can be used to reason about time improvement properties. We demonstrate the applicability of our theory by showing how it can be used to prove that a number of well-known program fusion techniques are time improvements, including fixed point fusion, map fusion and short cut fusion. Association for Computing Machinery 2018-07-30 Article PeerReviewed Hackett, Jennifer and Hutton, Graham (2018) Parametric polymorphism and operational improvement. Proceedings of the ACM on Programming Languages, 2 . ISSN 2475-1421 https://dl.acm.org/citation.cfm?id=3236763 doi:10.1145/3236763 doi:10.1145/3236763 |
| spellingShingle | Hackett, Jennifer Hutton, Graham Parametric polymorphism and operational improvement |
| title | Parametric polymorphism and operational improvement |
| title_full | Parametric polymorphism and operational improvement |
| title_fullStr | Parametric polymorphism and operational improvement |
| title_full_unstemmed | Parametric polymorphism and operational improvement |
| title_short | Parametric polymorphism and operational improvement |
| title_sort | parametric polymorphism and operational improvement |
| url | https://eprints.nottingham.ac.uk/52868/ https://eprints.nottingham.ac.uk/52868/ https://eprints.nottingham.ac.uk/52868/ |