×
Johann, Patricia; Voigtländer, Janis

A family of syntactic logical relations for the semantics of Haskell-like languages. (English) Zbl 1165.68024

Inf. Comput. 207, No. 2, 341-368 (2009).
Summary: Logical relations are a fundamental and powerful tool for reasoning about programs in languages with parametric polymorphism. Logical relations suitable for reasoning about observational behavior in polymorphic calculi supporting various programming language features have been introduced in recent years. Unfortunately, the calculi studied are typically idealized, and the results obtained for them offer only partial insight into the impact of such features on observational behavior in implemented languages. In this paper we show how to bring reasoning via logical relations closer to bear on real languages by deriving results that are more pertinent to an intermediate language for the (mostly) lazy functional language Haskell like GHC Core. To provide a more fine-grained analysis of program behavior than is possible by reasoning about program equivalence alone, we work with an abstract notion of relating observational behavior of computations which has among its specializations both observational equivalence and observational approximation.
We take selective strictness into account, and we consider the impact of different kinds of computational failure, e.g., divergence versus failed pattern matching, because such distinctions are significant in practice. Once distinguished, the relative definedness of different failure causes needs to be considered, because different orders here induce different observational relations on programs (including the choice between equivalence and approximation). Our main contribution is the construction of an entire family of logical relations, parameterized over a definedness order on failure causes, each member of which characterizes the corresponding observational relation. Although we deal with properties very much tied to types, we base our results on a type-erasing semantics since this is more faithful to actual implementations.

Cited in 1 Document

MSC:

68N18 Functional programming and lambda calculus
68N15 Theory of programming languages
68Q55 Semantics in the theory of computing

Keywords:

languages with parametric polymorphism; GHC Core

Software:

Haskell
PDFBibTeX XMLCite
\textit{P. Johann} and \textit{J. Voigtländer}, Inf. Comput. 207, No. 2, 341--368 (2009; Zbl 1165.68024)
Full Text: DOI Link

References:

[1] A. Ahmed, Step-indexed syntactic logical relations for recursive and quantified types, in: European Symposium on Programming, Proceedings, LNCS, vol. 3924, Springer-Verlag, Berlin, 2006, pp. 69-83.; A. Ahmed, Step-indexed syntactic logical relations for recursive and quantified types, in: European Symposium on Programming, Proceedings, LNCS, vol. 3924, Springer-Verlag, Berlin, 2006, pp. 69-83. · Zbl 1178.68146
[2] Cardelli, L., Typeful programming, (Neuhold, E.; Paul, M., Formal Description of Programming Concepts, IFIP State of the Art Reports Series (1991), Springer-Verlag: Springer-Verlag Berlin), 431-507 · Zbl 0743.68028
[3] Cardelli, L.; Wegner, P., On understanding types, data abstraction, and polymorphism, ACM Computing Surveys, 17, 4, 471-522 (1985)
[4] Chitil, O., Type inference builds a short cut to deforestation, (International Conference on Functional Programming, Proceedings (1999), ACM Press), 249-260 · Zbl 1345.68043
[5] K. Crary, R. Harper, Syntactic logical relations for polymorphic and recursive types, in: Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin, ENTCS, vol. 172, Elsevier, 2007, pp. 259-299.; K. Crary, R. Harper, Syntactic logical relations for polymorphic and recursive types, in: Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin, ENTCS, vol. 172, Elsevier, 2007, pp. 259-299. · Zbl 1277.68119
[6] M. Eekelen, M. Mol, Proof tool support for explicit strictness, in: Implementation and Application of Functional Languages 2005, Selected Papers, LNCS, vol. 4015, Springer-Verlag, Berlin, 2006, pp. 37-54.; M. Eekelen, M. Mol, Proof tool support for explicit strictness, in: Implementation and Application of Functional Languages 2005, Selected Papers, LNCS, vol. 4015, Springer-Verlag, Berlin, 2006, pp. 37-54. · Zbl 1236.68033
[7] Friedman, H., Equality between functionals, (Logic Colloquium ’72-73, Proceedings (1975), Springer-Verlag: Springer-Verlag Berlin), 22-37 · Zbl 0311.02040
[8] Ghani, N.; Johann, P., Monadic augment and generalised short cut fusion, Journal of Functional Programming, 17, 6, 731-776 (2007) · Zbl 1130.68039
[9] Gill, A.; Launchbury, J.; Peyton Jones, S., A short cut to deforestation, (Functional Programming Languages and Computer Architecture, Proceedings (1993), ACM Press), 223-232
[10] J.-Y. Girard, Interprétation functionelle et élimination des coupures dans l’arithmétique d’ordre supérieure, Ph.D. thesis, Université Paris VII, 1972.; J.-Y. Girard, Interprétation functionelle et élimination des coupures dans l’arithmétique d’ordre supérieure, Ph.D. thesis, Université Paris VII, 1972.
[11] Johann, P., Short cut fusion is correct, Journal of Functional Programming, 13, 4, 797-814 (2003) · Zbl 1111.68406
[12] Johann, P.; Voigtländer, J., Free theorems in the presence of seq, (Principles of Programming Languages, Proceedings (2004), ACM Press), 99-110 · Zbl 1325.68047
[13] Johann, P.; Voigtländer, J., The impact of seq on free theorems-based program transformations, Fundamenta Informaticae, 69, 1-2, 63-102 (2006) · Zbl 1096.68026
[14] Mitchell, J.; Plotkin, G., Abstract types have existential type, ACM Transactions on Programming Languages and Systems, 10, 3, 470-502 (1988)
[15] R. Mógelberg, Interpreting polymorphic FPC into domain theoretic models of parametric polymorphism, in: International Colloquium on Automata, Languages and Programming, Proceedings, LNCS, vol. 4052, Springer-Verlag, Berlin, 2006, 372-383.; R. Mógelberg, Interpreting polymorphic FPC into domain theoretic models of parametric polymorphism, in: International Colloquium on Automata, Languages and Programming, Proceedings, LNCS, vol. 4052, Springer-Verlag, Berlin, 2006, 372-383. · Zbl 1133.68310
[16] A. Moran, S. Lassen, S. Peyton Jones, Imprecise exceptions, Co-inductively, Higher Order Operational Techniques in Semantics, Proceedings, ENTCS, vol. 26, Elsevier, 1999, 122-141.; A. Moran, S. Lassen, S. Peyton Jones, Imprecise exceptions, Co-inductively, Higher Order Operational Techniques in Semantics, Proceedings, ENTCS, vol. 26, Elsevier, 1999, 122-141. · Zbl 0958.68040
[17] (Peyton Jones, S., Haskell 98 Language and Libraries: The Revised Report (2003), Cambridge University Press: Cambridge University Press Cambridge) · Zbl 1067.68041
[18] Peyton Jones, S.; Reid, A.; Hoare, C.; Marlow, S.; Henderson, F., A semantics for imprecise exceptions, (Programming Language Design and Implementation, Proceedings (1999), ACM Press), 25-36
[19] Pitts, A., Parametric polymorphism and operational equivalence, Mathematical Structures in Computer Science, 10, 3, 321-359 (2000) · Zbl 0955.68024
[20] Pitts, A., Typed operational reasoning, (Pierce, B., Advanced Topics in Types and Programming Languages (2005), MIT Press), 245-289 · Zbl 1080.68009
[21] G. Plotkin, Lambda-definability and logical relations, memorandum SAI-RM-4, University of Edinburgh, 1973.; G. Plotkin, Lambda-definability and logical relations, memorandum SAI-RM-4, University of Edinburgh, 1973.
[22] Reynolds, J., Towards a theory of type structure, (Colloque sur la Programmation, Proceedings (1974), Springer-Verlag: Springer-Verlag Berlin), 408-423 · Zbl 0309.68016
[23] Reynolds, J., Types, abstraction and parametric polymorphism, (Information Processing, Proceedings (1983), Elsevier), 513-523
[24] C. Strachey, Fundamental concepts in programming languages, Lecture notes for a course at the International Summer School in Computer Programming, 1967, Reprint appeared in Higher-Order and Symbolic Computation 13 (1-2) (2000) 11-49.; C. Strachey, Fundamental concepts in programming languages, Lecture notes for a course at the International Summer School in Computer Programming, 1967, Reprint appeared in Higher-Order and Symbolic Computation 13 (1-2) (2000) 11-49. · Zbl 0949.68510
[25] Svenningsson, J., Shortcut fusion for accumulating parameters & zip-like functions, (International Conference on Functional Programming, Proceedings (2002), ACM Press), 124-132 · Zbl 1322.68050
[26] A. Tolmach, An external representation for the GHC core language, Draft, 2001.; A. Tolmach, An external representation for the GHC core language, Draft, 2001.
[27] Voigtländer, J., Concatenate, reverse and map vanish for free, (International Conference on Functional Programming, Proceedings (2002), ACM Press), 14-25 · Zbl 1322.68051
[28] J. Voigtländer, P. Johann, Selective Strictness and Parametricity in Structural Operational Semantics, Technical Report TUD-FI06-02, Technische Universität Dresden, 2006.; J. Voigtländer, P. Johann, Selective Strictness and Parametricity in Structural Operational Semantics, Technical Report TUD-FI06-02, Technische Universität Dresden, 2006.
[29] Voigtländer, J.; Johann, P., Selective strictness and parametricity in structural operational semantics, inequationally, Theoretical Computer Science, 388, 1-3, 290-318 (2007) · Zbl 1143.68041
[30] Wadler, P., Theorems for free, (Functional Programming Languages and Computer Architecture, Proceedings (1989), ACM Press), 347-359
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.