Pragmatics of Type-Directed Partial Evaluation

Abstract. Type-directed partial evaluation stems from the residualization of arbitrary static values in dynamic contexts, given their type. Its algorithm coincides with the one for coercing a subtype value into a supertype value, which itself coincides with the one of normalization in the -calculus. Type-directed partial evaluation is thus used to specialize compiled, closed programs, given their type. Since Similix, let-insertion is a cornerstone of partial evaluators for callby-value procedural programs with computational e ects. It prevents the duplication of residual computations, and more generally maintains the order of dynamic side e ects in residual programs. 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 e ect information. It is achieved by delimiting and ing control, comparably to continuation-based specialization in direct style. It enables type-directe...

• Type: Conference
• Year: 1996
• Where: DAGSTUHL
• Authors: Olivier Danvy
• Keywords: Arbitrary Static Values, DAGSTUHL 1996, DAGSTUHL 2007, Residual Programs, Type-directed Partial Evaluation