Parametricity and local variables

ABSTRACT

We propose that the phenomenon of local state may be understood in terms of Strachey's concept of parametric (i.e., uniform) polymorphism. The intuitive basis for our proposal is the following analogy: a non-local procedure is independent of locally-declared variables in the same way that a parametrically polymorphic function is independent of types to which it is instantiated.A connection between parametricity and representational abstraction was first suggested by J.C. Reynolds. Reynolds used logical relations to formalize this connection in languages with type variables and user-defined types. We use relational parametricity to construct a model for an Algol-like language in which interactions between local and non-local entities satisfy certain relational criteria. Reasoning about local variables essentially involved proving properties of polymorphic functions. The new model supports straightforward validations of all the test equivalences that have been proposed in the literature for local-variable semantics, and encompasses standard methods of reasoning about data representations. It is not known whether our techniques yield fully abstract semantics. A model based on partial equivalence relations on the natural numbers is also briefly examined.

REFERENCES

• 1: Samson Abramsky , Thomas P. Jensen, A relational approach to strictness analysis for higher-order polymorphic functions, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-54, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99593]
• 2: Roberto M. Amadio, Recursion over realizability structures, Information and Computation, v.91 n.1, p.55-85, March 1991 [doi>10.1016/0890-5401(91)90074-C]
• 3: Michael Barr , Charles Wells, Category theory for computing science, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 4: William R. Cook, Object-Oriented Programming Versus Abstract Data Types, Proceedings of the REX School/Workshop on Foundations of Object-Oriented Languages, p.151-178, May 28-June 01, 1990
• 5: FREYD, P. J., MULRY, P., ROSOLINI, G., AND Scorn, D. S. 1990. Extensional PERs. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Sczence (Philadelphia, Pa.). IEEE Computer Society Press, Los Alamitos, Calif., pp. 346-354.
• 6: FREYD, P. J., ROBINSON, E. P., AND ROSOLINL G. 1992a. Dinaturality for free. In Appkcuttons of Categories in Computer Science, M. P. Fourman, P. T. Johnstone, and A. M. Phts, eds. London Mathematical Society Lecture Note Series, vol. 177. Cambridge Univershy Press, Cambridge, England, pp. 107-118.
• 7: FREYD, P. J., ROBINSON, E. P., AND ROSOLINI, G. 1992b. Functorial parametricity. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Sclellce (Santa Cruz, Calif). IEEE Computer Society Press, Los Alamitos, Calif., pp. 444-452.
• 8: Andreas Goerdt, A Hoare Calculus for Functions Defined by Recursion on Higher Types, Proceedings of the Conference on Logic of Programs, p.106-117, June 17-19, 1985
• 9: HOARE, C. A. R. 1972/ 1978. Proof of correctness of data representations. Acts Inf 1,271-281. (Reprinted in D. Gries, ed. programming Methodology, A Collection of Articles by IFIP WG2.3. Springer-Verlag, New York, 1978.)
• 10: Furio Honsell , Ian A. Mason , Scott Smith , Carolyn Talcott, A variable typed logic of effects, Information and Computation, v.119 n.1, p.55-90, May 15, 1995 [doi>10.1006/inco.1995.1077 ]
• 11: HYLAND, J. M. E. 1988. A small complete category. Ann. Pure Appl. Logic 40, 135-165.
• 12: J. M. E. Hyland , E. P. Robinson , G. Rosolini, Algebraic types in PER models, Proceedings of the fifth international conference on Mathematical foundations of programming semantics, p.333-350, July 1990, New Orleans, Louisiana, United States
• 13: JOHNSTONE, P. T. 1989. Affine categories and naturally Malcev categories. J. Pare Appl. A/g. 61, 251-256.
• 14: KELLY, G. M., AND STREET, R. H. 1974. Review of the basic elements of 2-categories. In Categoty Seminar: Proceedings of the Sydney Category Theory Seminar, 1972/1973, Lecture Notes in Mathematics, vol. 420, Springer-Verlag, Berlin, pp. 75-103.
• 15: J. Lambek , P. J. Scott, Introduction to higher order categorical logic, Cambridge University Press, New York, NY, 1986
• 16: LAWVERE, F. W. 1989. Qualitative distinctions between some toposes of generalized graphs. In Categories in Computer Science and Logic, vol. 92 of Contemporary Mathematics, J. W. Gray and A. Scedrov, eds. Providence, R. I., pp. 261-300.
• 17: LONGO, G., AND MOGGI, E. 1991. Constructive natural deduction and its "o-set" interpretation. Math. Struct. in Comput. Scl. 1, 2.
• 18: QingMing Ma , John C. Reynolds, Types, Abstractions, and Parametric Polymorphism, Part 2, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, p.1-40, March 25-28, 1991
• 19: MAC LANE, S. 1971. Categories for the Working Mathematiclun. Springer-Verlag, New York.
• 20: MASON, I. A., AND TALCOTT, C. L. 1992. References, local variables, and operational reasoning. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science (Santa Cruz, Calif). IEEE Computer Society Press, Los Alamitos, Calif., pp. 186-197.
• 21: A. R. Meyer , K. Sieber, Towards fully abstract semantics for local variables, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-203, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73577]
• 22: John C. Mitchell, Representation independence and data abstraction, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.263-276, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512669]
• 23: John C. Mitchell, Type systems for programming languages, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 24: John C. Mitchell , Andre Scedrov, Notes on Sconing and Relators, Selected Papers from the Workshop on Computer Science Logic, p.352-378, September 28-October 02, 1992
• 25: MOGGI, E. 1988. The maximum consistent theory of the second-order bn lambda calculus. Unpublished note.
• 26: J. W. Backus , F. L. Bauer , J. Green , C. Katz , J. McCarthy , A. J. Perlis , H. Rutishauser , K. Samelson , B. Vauquois , J. H. Wegstein , A. van Wijngaarden , M. Woodger , P. Naur, Revised report on the algorithm language ALGOL 60, Communications of the ACM, v.6 n.1, p.1-17, Jan. 1963 [doi>10.1145/366193.366201]
• 27: O'HEARN, P. W., AND REDDY, U. S. 1995. Objects, interference, and the Yoneda embedding. Proceedings of the 22th Conference on Math Foundations of Program Semantics. Electronic Notes in Computer Science, vol. 1 Elsewer Science B. V., to appear.
• 28: O'HEARN, P. W., AND TTENNET, R. D. 1992. Semantics of local variables. In Applications of Categories in Computer Science. M. P. Fourman, P. T. Johnstone, and A. M. Pitts, eds. London Mathematical Society Lecture Notes Series, vol. 177, Cambridge University Press, Cambridge, England, pp. 217-238.
• 29: P. W. O'Hearn , R. D. Tennent, Relational parametricity and local variables, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-184, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158624]
• 30: P. W. O'Hearn , R. D. Tennent, Semantical analysis of specification logic, 2, Information and Computation, v.107 n.1, p.25-57, Nov. 1993 [doi>10.1006/inco.1993.1060 ]
• 31: Frank Joseph Oles, A category-theoretic approach to the semantics of programming languages, 1982
• 32: F J Oles, Type algebras, functor categories and block structure, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 33: PHOA, W. 1990. Effective domams and mtrmslc structure. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (Philadelphia, Pa.). IEEE Computer Society Press, Los Alamitos, Calif., pp. 366-377.
• 34: Wesley Phoa, Two Results on Set-Theoretic Polymorphism, Proceedings of the 4th International Conference on Category Theory and Computer Science, p.219-235, September 03-06, 1991
• 35: PITTS, A. M. 1993. Relational properties of recursively defmed domains. In Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science (Montreal, Canada). IEEE Computer Society Press, Los Alamitos, Calif., pp. 86-97.
• 36: Andrew M. Pitts , Ian D. B. Stark, Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new?, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, p.122-141, August 30-September 03, 1993
• 37: Andrew M. Pitts , Ian D. B. Stark, Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new?, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, p.122-141, August 30-September 03, 1993
• 38: PLOTKIN, G. D. 1980. Lambda-definabdity in the full type hierarchy. In To H. B. Cuny: Essays in Combination Logic, Lambda Calculus and Formalism, J. P. Seldin and J. R. Hindley, eds. Academic Press, Orlando, Fla., pp. 363-373.
• 39: Gordon D. Plotkin , Martín Abadi, A Logic for Parametric Polymorphism, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.361-375, March 16-18, 1993
• 40: REDDY, U. S. 1993. Global state considered unnecessary: semantics of interference-free imperative programming. In ACM SIGPLAN Workshop on State in Programming Languages (Copenhagen, Denmark, June 12). ACM, New York, and Technical report YALEU/DCS/RR- 968, Department of Computer Science, Yale University, New Haven, Conn., pp. 120-135.
• 41: REDDY, U. S. 1994. Passivity and independence. In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (Paris, France). IEEE Computer Society Press, Los Alamitos, Calif., pp. 342-352.
• 42: REDDY, U. S. 1995. Global state considered unnecessaqu Object-based semantics of interference-free imperative programs. Lisp Symb. Computation (special issue on State in Programming Languages), to appear.
• 43: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 44: REYNOLDS, J. C. 1978a. User-defined types and procedural data structures as complementary approaches to data abstraction. In D. Gries, ed. Programming Methodology, A Collection of Articles by IFIP WG 2.3. Springer-Verlag, New York, 1978., pp. 309-317.
• 45: John C. Reynolds, Syntactic control of interference, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.39-46, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512766]
• 46: John C. Reynolds, The Craft of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 47: REYNOLDS, J. C. 1981b. The essence of Algol. In Algotithmic Languages, J. W. de Bakker, and J. C. van Vliet, eds. North-Holland, AmstercIam, pp. 345-372.
• 48: REYNOLDS, J. C. 1983. Types, abstraction and parametric polymorphism. In Information Processing 83, R. E. A. Mason, ed. North-Holland, Amsterdam, pp. 513-523.
• 49: John C. Reynolds , Gordon D. Plotkin, On functors expressible in the polymorphic typed lambda calculus, Information and Computation, v.105 n.1, p.1-29, July 1993 [doi>10.1006/inco.1993.1037 ]
• 50: E. Robinson, How complete is PER?, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.106-111, June 1989, Pacific Grove, California, United States
• 51: ROBINSON, E. P., AND ROSOLINI, G. 1994. Reflexive graphs and parametric polymorphism. In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (Paris, France). IEEE Computer Society Press, Los Alamltos, Calif.
• 52: David A. Schmidt, Detecting global variables in denotational specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.2, p.299-310, April 1985 [doi>10.1145/3318.3323]
• 53: SIEBER, K. 1992. Reasoning about sequential functions via logical relations. In Applications of Categories in Computer Science, M. P. Fourman, P. T. Johnstone, and A. M. Pitts, eds. London Mathematical Society Lecture Note Series, vol. 177. Cambridge University Press, Cambridge, England, pp. 258-269.
• 54: SIEBER, K. 1993. New steps towards full abstraction for local variables. In ACM SIGPLAN Workshop on State in Programming Languages (Copenhagen, Denmark, June 12). ACM, New York, and Technical report YALEU/DCS/RR-968, Department of Computer Science, Yale University, New Haven, Comp., pp. 88-100.
• 55: SIEBER, K, 1994. Full abstraction for the second order subset of an Algol-like language (preliminary report). Technischer Bericht A 01/94, Universitaet des Saarlandes, Feb.
• 56: STRACHEY, C. 1967. Fundamental Concepty in Programming Languages. Unpublished lecture notes, International Summer School in Computer Programming, Copenhagen.
• 57: R. D. Tennent, Elementary data structures in Algol-like languages, Science of Computer Programming, v.13 n.1, p.73-110, December 1989 [doi>10.1016/0167-6423(89)90016-6 ]
• 58: R. D. Tennent, Semantical analysis of specification logic, Information and Computation, v.85 n.2, p.135-162, April 1990 [doi>10.1016/0890-5401(90)90045-J]
• 59: TENNENT, R. D. 1991. Semantics of Programming Languages. Prentice-Hall International, London, England.
• 60: Philip Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.347-359, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99404]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics

General Terms:
Languages, Theory

Keywords:
algol-like languages, local state, logical relations, parametric polymorphism