Pragmatic Aspects of Type-Directed Partial Evaluation
DOI:
https://doi.org/10.7146/brics.v3i15.19977Resumé
Type-directed partial evaluation stems from the residualization of static values in dynamic contexts, given their type and the type of their free variables. Its algorithm coincides with the algorithm for coercinga subtype value into a supertype value, which itself coincides with
Berger and Schwichtenberg's normalization algorithm for the simply typed lambda-calculus. Type-directed partial evaluation thus can be used to specialize a compiled, closed program, given its type.
Since Similix, let-insertion is a cornerstone of partial evaluators for call-by-value procedural languages with computational effects (such as divergence). It prevents the duplication of residual computations, and more generally maintains the order of dynamic side effects in the residual program. This article describes the extension of type-directed partial evaluation
to insert residual let expressions. This extension requires the
user to annotate arrow types with effect information. It is achieved by delimiting and abstracting control, comparably to continuation-based specialization in direct style. It enables type-directed partial evaluation of programs with effects (e.g., a definitional lambda-interpreter for an imperative language) that are in direct style. The residual programs
are in A-normal form. A simple corollary yields CPS (continuation-passing style) terms instead. We illustrate both transformations with two interpreters for Paulson's Tiny language, a classical example in partial evaluation.
Downloads
Publiceret
1996-01-15
Citation/Eksport
Danvy, O. (1996). Pragmatic Aspects of Type-Directed Partial Evaluation. BRICS Report Series, 3(15). https://doi.org/10.7146/brics.v3i15.19977
Nummer
Sektion
Artikler
Licens
Authors who publish with this journal agree to the following terms:- Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).