The Scenic Route to Deforestation
摘要
Parametricity and free theorems are a powerful tool for proving the correctness of optimizations. There has been some investigation of incorporating free theorems for functional logic languages, including a proof of the parametricity theorem for a sub-language of Curry. In this paper we explore the consequences of adding one optimization, shortcut deforestation, to a Curry compiler. We describe the optimization and give a proof of correctness. While proving the correctness of the optimization, we explore the application of parametricity and free theorems to Curry. This leads to some of the more surprising aspects of functional logic programming.