The Impact of seq on Free Theorems-Based Program Transformations

• Autorzy: Johann P. , Voigtländer J.
• Języki publikacji: EN

Abstrakty

EN

Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. Unfortunately, standard parametricity results - including so-called free theorems - fail for nonstrict languages supporting a polymorphic strict evaluation primitive such as Haskell's seq. A folk theorem maintains that such results hold for a subset of Haskell corresponding to a Girard-Reynolds calculus with fixpoints and algebraic datatypes even when seq is present provided the relations which appear in their derivations are required to be bottom-reflecting and admissible. In this paper we show that this folklore is incorrect, but that parametricity results can be recovered in the presence of seq by restricting attention to left-closed, total, and admissible relations instead. The key novelty of our approach is the asymmetry introduced by left-closedness, which leads to ``inequational'' versions of standard parametricity results together with preconditions guaranteeing their validity even when seq is present. We use these results to derive criteria ensuring that both equational and inequational versions of short cut fusion and related program transformations based on free theorems hold in the presence of seq.

Słowa kluczowe

EN

Haskell; control primitives; correctness proofs; denotational semantics; functional programming languages; logical relations; mixing strict and nonstrict evaluation; parametricity; polymorphism; program transformation; rank - 2 types; short cut fusion; theorems for free

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 69, nr 1,2
• Strony: 63--102
• Opis fizyczny: bibliogr. 37 poz.

Twórcy

autor

Johann P.

autor

Voigtländer J.

• Department of Computer Science Rutgers University, Camden, NJ 08102 USA,

Bibliografia

• [1] The Program TransformationWiki (http://program-transformation.org/Transform.)
• [2] http://wwwtcs.inf.tu-dresden.de/~voigt/Seq.lhs
• [3] The Haskell Mailing List Archive (http://www.mail-archive.com/[e-mail]
• [4] Special Issue on Program Transformation, Science of Computer Programming, 52, 2004, 1-371.
• [5] Abadi, M.:TT-closed relations and admissibility, Mathematical Structures in Computer Science, 10, 2000, 313-320.
• [6] Chitil, O.: Type inference builds a short cut to deforestation, International Conference on Functional Programming, Proceedings, pages 249-260, ACM Press, 1999.
• [7] Cosmadakis, S.,Meyer, A., Riecke, J.: Completeness for typed lazy inequalities, Logic in Computer Science, Proceedings, pages 312-320, IEEE Computer Society Press, 1990.
• [8] Czarnecki, K., Eisenecker, U.: Generative Programming: Methods, Tools, and Applications, Addison-Wesley, 2000.
• [9] Friedman, H.: Equality between functionals, Logic Colloquium '72-73, Proceedings, pages 22-37, Springer-Verlag, 1975.
• [10] Gill, A., Launchbury, J., Peyton Jones, S.: A short cut to deforestation, Functional Programming Languages and Computer Architecture, Proceedings, pages 223-232, ACM Press, 1993.
• [11] Girard, J.-Y.: Interprétation functionelle et élimination des coupures dans l'arithmétique d'ordre supérieure, Ph.D. Thesis, Université Paris VII, 1972.
• [12] Johann, P.: A generalization of short-cut fusion and its correctness proof, Higher-Order and Symbolic Computation, 15, 2002, 273-300.
• [13] Johann, P.: Short cut fusion is correct, Journal of Functional Programming, 13, 2003, 797-814.
• [14] Johann, P.: On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi, Mathematical Structures in Computer Science, 15, 2005, 201-229.
• [15] Johann, P., Voigtländer, J.: Free theorems in the presence of seq, Principles of Programming Languages, Proceedings, pages 99-110, ACM Press, 2004.
• [16] Kuo, T.-M.,Mishra, P.: Strictness analysis: A new perspective based on type inference, Functional Programming Languages and Computer Architecture, Proceedings, pages 260-272, ACM Press, 1989.
• [17] Launchbury, J., Paterson, R.: Parametricity and unboxing with unpointed types, European Symposium on Programming, Proceedings, pages 204-218, Springer-Verlag, 1996.
• [18] Leivant, D.: Polymorphic type inference, Principles of Programming Languages, Proceedings, pages 88-98, ACM Press, 1983.
• [19] Mycroft, A.: Abstract Interpretation and Optimising Transformations for Applicative Programs, Ph.D. Thesis, University of Edinburgh, 1981.
• [20] N¨ocker, E.: Strictness analysis using abstract reduction, Functional Programming Languages and Computer Architecture, Proceedings, pages 255-265, ACM Press, 1993.
• [21] Peyton Jones, S., Ed.: Haskell 98 Language and Libraries: The Revised Report, Cambridge University Press, 2003.
• [22] Peyton Jones, S., Jones, M., Meijer, E.: Type classes: An exploration of the design space, Haskell Workshop, Proceedings, 1997.
• [23] Peyton Jones, S., Launchbury, J., Shields, M., Tolmach, A.: Bridging the gulf: A common intermediate language for ML and Haskell, Principles of Programming Languages, Proceedings, pages 49-61, ACM Press, 1998.
• [24] Peyton Jones, S., Tolmach, A., Hoare, T.: Playing by the rules: Rewriting as a practical optimisation technique in GHC, Haskell Workshop, Proceedings, pages 203-233, 2001.
• [25] Pitts, A.: Parametric polymorphism and operational equivalence, Mathematical Structures in Computer Science, 10, 2000, 321-359.
• [26] Plotkin, G.: Lambda-definability in the full type hierarchy, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 363-373, Academic Press, 1980.
• [27] Reynolds, J.: Towards a theory of type structure, Colloque sur la Programmation, Proceedings, pages 408-423, Springer-Verlag, 1974.
• [28] Reynolds, J.: Types, abstraction and parametric polymorphism, Information Processing, Proceedings, pages 513-523, Elsevier Science Publishers B.V., 1983.
• [29] Schmidt, D.: Denotational Semantics: A Methodology for Language Development, Allyn and Bacon, 1986.
• [30] Sheard, T.: A pure language with default strict evaluation order and explicit laziness, presented at the Haskell Workshop, 2003, available from http://www.cs.pdx.edu/~sheard/papers/ExplicitLazy.ps
• [31] Statman, R.: Logical relations and the typed lambda-calculus, Information and Control, 65, 1985, 85-97.
• [32] Svenningsson, J.: Shortcut fusion for accumulating parameters & zip-like functions, International Conference on Functional Programming, Proceedings, pages 124-132, ACM Press, 2002.
• [33] Takano, A., Meijer, E.: Shortcut deforestation in calculational form, Functional Programming Languages and Computer Architecture, Proceedings, pages 306-313, ACM Press, 1995.
• [34] Trinder, P., Hammond, K., Loidl, H.-W., Peyton Jones, S.: Algorithm + Strategy = Parallelism, Journal of Functional Programming, 8, 1998, 23-60.
• [35] Voigtländer, J.: Concatenate, reverse and map vanish for free, International Conference on Functional Programming, Proceedings, pages 14-25, ACM Press, 2002.
• [36] Wadler, P.: Theorems for free!, Functional Programming Languages and Computer Architecture, Proceedings, pages 347-359, ACM Press, 1989.
• [37] Wadler, P., Blott, S.: How to make ad-hoc polymorphismless ad hoc, Principles of Programming Languages, Proceedings, pages 60-76, ACM Press, 1989.