Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Memoization in Type-Directed Partial Evaluation
| |
|
Memoization in Type-Directed Partial Evaluation
Vincent Balat7  and Olivier Danvy8
| (7) |
PPS, Université Paris VII, Denis Diderot Case 7014, 2 place Jussieu, F-75251 Paris Cedex 05, France |
| (8) |
BRICS Department of Computer Science, University of Aarhus, Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark |
Abstract
We use a code generator—type-directed partial evaluation— to verify conversions between isomorphic types, or more precisely
to verify that a composite function is the identity function at some complicated type. A typed functional language such as
ML provides a natural support to express the functions and type-directed partial evaluation provides a convenient setting
to obtain the normal form of their composition. However, off-the-shelf type-directed partial evaluation turns out to yield
gigantic normal forms.
We identify that this gigantism is due to redundancies, and that these redundancies originate in the handling of sums, which
uses delimited continuations. We successfully eliminate these redundancies by extending type-directed partial evaluation with
memoization capabilities. The result only works for pure functional programs, but it provides an unexpected use of code generation
and it yields orders-of-magnitude improvements both in time and in space for type isomorphisms.
Basic Research in Computer Science (www. brics. dk), funded by the Danish National Research Foundation.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|