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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

The Scenic Route to Deforestation

  • Vincent Robinson,
  • Steven Libby

摘要

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.