Type- and Control-Flow Directed Defunctionalization

被引:3
作者
Contractor, Maheen Riaz [1 ]
Fluet, Matthew [1 ]
机构
[1] Rochester Inst Technol, Rochester, NY 14623 USA
来源
PROCEEDINGS OF THE 32ND SYMPOSIUM ON IMPLEMENTATION AND APPLICATION OF FUNCTIONAL LANGUAGES, IFL 2020 | 2020年
基金
美国国家科学基金会;
关键词
defunctionalization; control-flow analysis; type-flow analysis;
D O I
10.1145/3462172.3462193
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Defunctionalization is a program transformation that removes all first-class functions from a source program, yielding an equivalent target program that contains only first-order functions. As originally described by Reynolds, defunctionalization transforms an untyped higher-order source program into an untyped first-order target program that uses a single, global dispatch function. In addition to being limited to untyped languages, a drawback of this approach is that obscures control flow, making it appear as though the code associated with every source function could be invoked at every call site of the target program. Subsequent work has extended defunctionalization to both simply-typed and polymorphicallytyped languages, but the latter continues to use a single, global dispatch function. Other work has extended defunctionalization to be guided by a control-flow analysis of a simply-typed source program, where the types of the target program exactly capture the results of the flow analysis and make it apparent which (limited) set of functions can be invoked at each call site. Our work draws inspiration from these previous approaches and proposes a novel flow-directed defunctionalization for a polymorphicallytyped source language. Guided by a type- and control-flow analysis, which exploits well-typedness of the source program to filter flows that are incompatible with static types, the transformation must construct evidence that filtered flows are impossible in order to ensure the well-typedness of the target program.
引用
收藏
页码:79 / 92
页数:14
相关论文
共 35 条
[1]  
Adsit Connor, 2014, IFL 14 P 26ND INT S
[2]  
Ager M. S., 2003, P 5 ACM SIGPLAN INT, P8, DOI DOI 10.1145/888251.888254
[3]  
AIKEN A, 1991, LECT NOTES COMPUT SC, V523, P427
[4]   Engineering Formal Metatheory [J].
Aydemir, Brian ;
Chargueraud, Arthur ;
Pierce, Benjamin C. ;
Pollack, Randy ;
Weirich, Stephanie .
POPL'08: PROCEEDINGS OF THE 35TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2008, :3-15
[5]   Type-driven defunctionalization [J].
Bell, JM ;
Bellegarde, F ;
Hook, J .
ACM SIGPLAN NOTICES, 1997, 32 (08) :25-37
[6]  
Boquist U, 1997, LECT NOTES COMPUT SC, V1268, P58
[7]   Combining Proofs and Programs in a Dependently Typed Language [J].
Casinghino, Chris ;
Sjoeberg, Vilhelm ;
Weirich, Stephanie .
ACM SIGPLAN NOTICES, 2014, 49 (01) :33-45
[8]  
Cejtin H, 2000, LECT NOTES COMPUT SC, V1782, P56
[9]   The Locally Nameless Representation [J].
Chargueraud, Arthur .
JOURNAL OF AUTOMATED REASONING, 2012, 49 (03) :363-408
[10]   Combining programming with theorem proving [J].
Chen, CY ;
Xi, HW .
ACM SIGPLAN NOTICES, 2005, 40 (09) :66-77