Abstract
Reversible languages are programming languages where all programs can
run both forwards and backwards. Reversible functional languages have
been proposed that use symmetric pattern matching and data
construction. To be reversible, these languages require linearity:
Every variable must be used exactly once, so no references are copied
and all references are followed exactly once. Copying of values must
use deep copying. Similarly, equality testing requires deep
comparison of trees.
A previous paper describes reversible treatment of reference counts,
which allows sharing of structures without deep copying, but there are
limitations. Applying a constructor to arguments creates a new node
with reference count 1, so pattern matching is by symmetry restricted
to nodes with reference count 1. A variant pattern that does not
change the reference count of the root node is introduced to allow
manipulation of shared data. Having two distinct patterns for shared
and unshared data, however, adds a burden on the programmer.
We observe that we can allow pattern matching on nodes with arbitrary
reference count if we also allow constructor application to return
nodes with arbitrary reference counts. We do this by using maximal
sharing: If a newly constructed node is identical to an already
existing node, we return a pointer to the existing node (increasing
its reference count) instead of allocating a new node with reference
count 1.
To avoid searching the entire heap for an identical node, we use
hash-consing to restrict the search to a small segment of the heap.
We estimate how large this segment needs to be to give a very low
probability of allocation failure when the heap is less than half
full. Experimentally, we find that overlapping segments gives
dramatically better results than disjoint segments.
run both forwards and backwards. Reversible functional languages have
been proposed that use symmetric pattern matching and data
construction. To be reversible, these languages require linearity:
Every variable must be used exactly once, so no references are copied
and all references are followed exactly once. Copying of values must
use deep copying. Similarly, equality testing requires deep
comparison of trees.
A previous paper describes reversible treatment of reference counts,
which allows sharing of structures without deep copying, but there are
limitations. Applying a constructor to arguments creates a new node
with reference count 1, so pattern matching is by symmetry restricted
to nodes with reference count 1. A variant pattern that does not
change the reference count of the root node is introduced to allow
manipulation of shared data. Having two distinct patterns for shared
and unshared data, however, adds a burden on the programmer.
We observe that we can allow pattern matching on nodes with arbitrary
reference count if we also allow constructor application to return
nodes with arbitrary reference counts. We do this by using maximal
sharing: If a newly constructed node is identical to an already
existing node, we return a pointer to the existing node (increasing
its reference count) instead of allocating a new node with reference
count 1.
To avoid searching the entire heap for an identical node, we use
hash-consing to restrict the search to a small segment of the heap.
We estimate how large this segment needs to be to give a very low
probability of allocation failure when the heap is less than half
full. Experimentally, we find that overlapping segments gives
dramatically better results than disjoint segments.
| Translated title of the contribution | Spildopsamling fot reversible funktionssprog |
|---|---|
| Original language | English |
| Title of host publication | Reversible computation : 7th International Conference, RC 2015, Grenoble, France, July 16-17, 2015, Proceedings |
| Editors | Jean Krivine, Jean-Bernard Stefani |
| Number of pages | 16 |
| Publisher | Springer |
| Publication date | 2015 |
| Pages | 79-94 |
| Chapter | 5 |
| ISBN (Print) | 978-3-319-20859-6 |
| ISBN (Electronic) | 978-3-319-20860-2 |
| DOIs | |
| Publication status | Published - 2015 |
| Event | International Conference, RC 2015 - Grenoble, France Duration: 16 Jul 2015 → 17 Jul 2015 Conference number: 7 |
Conference
| Conference | International Conference, RC 2015 |
|---|---|
| Number | 7 |
| Country/Territory | France |
| City | Grenoble |
| Period | 16/07/2015 → 17/07/2015 |
| Series | Lecture notes in computer science |
|---|---|
| Volume | 9138 |
| ISSN | 0302-9743 |