Olaf Chitil
ABSTRACT
Deforestation optimises a functional program by transforming it into another one that does not create certain intermediate data structures. Short cut deforestation is a deforestation method which is based on a single, local transformation rule. In return, short cut deforestation expects both producer and consumer of the intermediate structure in a certain form. Warm fusion wan proposed to automatically transform functions into this form. Unfortunately, it is costly and hard to implement. Starting from the fact that short cut deforestation is based on a parametricity theorem of the second-order typed λ-calculus, we show how the required form of a list producer can be derived by the use of type inference. Typability for the second-order typed λ-calculus is undecidable. However, we present a linear-time algorithm that solves a partial type inference problem and that, together with controlled inlining and polymorphic type instantiation, suffices for deforestation. The resulting new short cut deforestation algorithm is efficient and removes more intermediate lists than the original.
- Chi97.Olaf Chitil. Adding an optimisation pass to the Glasgow Haskell compiler. Available from http'//w~-i2, informatik, rwth-aachen. de/~ chit il, November 1997.Google Scholar
- Feg96.Leonidas Fegaras. Fusion for free! Technical Report CSE-96-001, Oregon Graduate Institute of Science and Technology, january 8, 1996. Google ScholarDigital Library
- GHC.The Glasgow Haskell compiler. Availabel from http'//research.microsoft.com} users/t-simonm/ghc/.Google Scholar
- Gil96.Andrew Gill. Cheap Deforestation for Nonstrict Functional Languages. PhD thesis, Glasgow University, 1996.Google Scholar
- GLP93.Andrew Gill, John Launchbury, and Simon L. Peyton Jones. A Short Cut to Deforestation. In FPCA '93, Conference on Functional Programming Languages and Computer Architecture, pages 223-232, Copenhagen, Denmark, June 9-11, 1993. ACM Press. Google ScholarDigital Library
- HIT96.Zhenjiang Hu, Hideya Iwasaki, and Masato Takeichi. Deriving structural hylomorphisms from recursive definitions. In Proceedings 1st A CM SIGPLAN Intl. Conf. on Functional Programming, ICFP'96, Philadelphia, PA, USA, 2d-26 May 1996, pages 73-82, New York, 1996. ACM Press. Google ScholarDigital Library
- Hug89.J. Hughes. Why Functional Programming Matters. Computer journal, 32(2)'98-107, 1989. Google ScholarDigital Library
- LS95.John Launchbury and Tim Sheard. Warm fusion' Deriving build-catas from recursive definitions. In Conf. Record 7th A CM SIG- PLAN/$IGARCH Intl. Conf. on Functional Programming Languages and Computer Architecture, FPCA '95, La Jolla, San Diego, CA, USA, 25-28 June 1995, pages 314-323. ACM Press, New York, 1995. Google ScholarDigital Library
- LY98.Oukseh Lee and Kangkeun Yi. Proofs about a folklore let-polymorphic type inference algorithm. A CM Transactions on Programming Languages and Systems, 20(4)'707-723, July 1998. Google ScholarDigital Library
- Mar95.Simon Marlow. Deforestation for Higher-Order Functional Programs. PhD thesis, Glasgow University, 1995.Google Scholar
- MFP91.Erik Meijer, Maarten Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In John Hughes, editor, Functional Programming Languages and Computer Architecture, pages 124- 144. Springer Verlag, June 1991. Google ScholarDigital Library
- MH95.Erik Meijer and Graham Hutton. Bananas in space: Extending fold and unfold to exponential types. In Proceedings of the Seventh international Conference on Functional Progrumming Languages and Computer Architecture (FPCA 'g5), pages 324-333, La Jolla, California, June 25-28, 1995. ACM SIG- PLAN/SIGARCH and iFIP WG2.8, ACM Press. Google ScholarDigital Library
- MOTW95.John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call.by-name, callby-value, call-by-need, and the linear lambda calculus. In 11 'th International Conference on the Mathematical Foundations of Programming Semantics, New Orleans, Lousiana, March- April 1995.Google Scholar
- NP98.L~zl6 N~meth and Simon Peyton Jones. A design for warm fusion. In Proceedings of the l Oth International Workshop on Implementa~ tion of Functional Languages, }pages 381-393, 1998.Google Scholar
- PH+99.Simon L. Peyton Jones, John Hughes, et aI. Haskell 98: A non-strict, purely functional language, http: //m~ .ha~kell. org, February 1999.Google Scholar
- Pit98.A.M. Pitts. Parametric polymorphism and operational equivalence. Technical Report 453, Cambridge University Computer Laboratory, 1998. A preliminary version appeared in Proceedings, Second Workshop on Higher Order Operational Techniques in Semantics (HOOTS II), Stanford 6'.4, December 1997, Electronic Notes in Theoretical Computer Science 10, 1998.Google Scholar
- San95.Andr~ Santos. Compilation by Transformation in Non-Strict Functional Languages. Phi) thesis, Glasgow University, Department of Computing Science, 1995.Google Scholar
- San96.D. Sands. Proving the correctness of recursionbased automatic program transformations. Theoretical Computer Science, 167(1-2):193- 233, October 1996. Google ScholarDigital Library
- TM95.Akihiko Takano and Erik Meijer. Shortcut deforestation in calculational form. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture (FPCA'95), pages 306-313, La Jolla, California, June 25--28, 1995. ACM SIGPLAN/SIGARCH and IFIP WG2.8, ACM Press. Google ScholarDigital Library
- Tüf98.Christian Triflers. Erweiterung des Glasgow- Haskell-Compilers um die Erkennung yon Hylomorphismen. Master's thesis, RWTH Aachen, 1998.Google Scholar
- Wad89.Philip Wadler. Theorems for flee. In Functional Programming Languages and Computer Architecture, pages 347-359. ACM, 1989. Google ScholarDigital Library
- Wad90.Philip Wadler. Deforestation: transforming programs to eliminate trees. Theoretical Computer Science, 73(2):231-248, June 1990. Google ScholarDigital Library
- Wel94.J.B. Wells. Typability and type-checking in the second-order A-calculus are equivalent and undecidable. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 176-185, Paris, France, 4-7 july 1994. IEEE Computer Society Press.Google ScholarCross Ref
- WP99.Keith Wansbrough and Simon Peytoa Jones. Once upon a polymorphic type. In Conference Record of POPL '99: The 26nd A CM SIGPLAN-SiGACT Symposium on Principles of Programming Languages, 1999. Google ScholarDigital Library
Index Terms
- Typer inference builds a short cut to deforestation
Recommendations
Typer inference builds a short cut to deforestation
Deforestation optimises a functional program by transforming it into another one that does not create certain intermediate data structures. Short cut deforestation is a deforestation method which is based on a single, local transformation rule. In ...
TypEr: a type annotator of Erlang code
ERLANG '05: Proceedings of the 2005 ACM SIGPLAN workshop on ErlangWe describe and document the techniques used in TOOL, a fully automatic type annotator for Erlang programs based on constraint-based type inference of success typings (a notion closely related to principal typings). The inferred typings are fine-grained ...
On Some Problems of Efficient Inference Search in First-Order Cut-Free Modal Sequent Calculi
SYNASC '08: Proceedings of the 2008 10th International Symposium on Symbolic and Numeric Algorithms for Scientific ComputingA unified approach is developed for constructing first-order cut-free sequent calculi without equality representing two classes of modal logics in dependence of whether classical logic or intuitionistic one is taken as a basis. It uses the original ...
Comments