Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism

ABSTRACT

Higher-order abstract syntax is a simple technique for implementing languages with functional programming. Object variables and binders are implemented by variables and binders in the host language. By using this technique, one can avoid implementing common and tricky routines dealing with variables, such as capture-avoiding substitution. However, despite the advantages this technique provides, it is not commonly used because it is difficult to write sound elimination forms (such as folds or catamorphisms) for higher-order abstract syntax. To fold over such a datatype, one must either simultaneously define an inverse operation (which may not exist) or show that all functions embedded in the datatype are parametri.In this paper, we show how first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax. With this restriction, we implement a library of iteration operators over data-structures containing functionals. From this implementation, we derive "fusion laws" that functional programmers may use to reason about the iteration operator. Finally, we show how this use of parametric polymorphism corresponds to the Schürmann, Despeyroux and Pfenning method of enforcing parametricity through modal types. We do so by using this library to give a sound and complete encoding of their calculus into System F?. This encoding can serve as a starting point for reasoning about higher-order structures in polymorphic languages.

REFERENCES

• 1: Umut A. A. Acar , Guy E. Blelloch , Robert Harper, Selective memoization, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-25, January 15-17, 2003, New Orleans, Louisiana, USA
• 2: Simon Ambler , Roy L. Crole , Alberto Momigliano, Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, p.13-30, August 20-23, 2002
• 3: C. Böhm and A. Berarducci. Automatic synthesis of typed ?-programs on term algebras. Theoretical Computer Science, 39:135--154, 1985.
• 4: A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56--68, 1940.
• 5: D. Clarke, R. Hinze, J. Jeuring, A. Löh, and J. de Wit. The Generic Haskell user's guide. Technical Report UU-CS-2001-26, Utrecht University, 2001.
• 6: O. Danvy and A. Filinski. Representing control: a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361--391, Dec. 1992.
• 7: Rowan Davies , Frank Pfenning, A modal analysis of staged computation, Journal of the ACM (JACM), v.48 n.3, p.555-604, May 2001 [doi>10.1145/382780.382785]
• 8: Joëlle Despeyroux , Pierre Leleu, Recursion over objects of functional type, Mathematical Structures in Computer Science, v.11 n.4, p.555-572, August 2001 [doi>10.1017/S0960129501003346]
• 9: Leonidas Fegaras , Tim Sheard, Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space), Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.284-294, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237792]
• 10: J.-Y. Girard. Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination de coupures dans l'analyse et la théorie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 63--92. North-Holland Publishing Co., 1971.
• 11: R. Hinze. Polytypic values possess polykinded types. Science of Computer Programming, 43(2--3):129--159, 2002. MPC Special Issue.
• 12: Patricia Johann, A Generalization of Short-Cut Fusion and its Correctness Proof, Higher-Order and Symbolic Computation, v.15 n.4, p.273-300, December 2002 [doi>10.1023/A:1022982420888]
• 13: M. P. Jones. A system of constructor classes: overloading and implicit higher-order polymorphism. Journal of Functional Programming, 5(1), Jan. 1995.
• 14: Mark P. Jones, Type Classes with Functional Dependencies, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.230-244, April 02, 2000
• 15: Erik Meijer , Maarten Fokkinga , Ross Paterson, Functional programming with bananas, lenses, envelopes and barbed wire, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.124-144, June 1991, Cambridge, Massachusetts, United States
• 16: Erik Meijer , Graham Hutton, Bananas in space: extending fold and unfold to exponential types, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.324-333, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224225]
• 17: D. Miller. An extension to ML to handle bound variables in data structures: Preliminary report. In Proceedings of the Logical Frameworks BRA Workshop, May 1990.
• 18: Aleksandar Nanevski, Meta-programming with names and necessity, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.206-217, October 04-06, 2002, Pittsburgh, PA, USA
• 19: S. Peyton Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, 2003.
• 20: Frank Pfenning , Rowan Davies, A judgmental reconstruction of modal logic, Mathematical Structures in Computer Science, v.11 n.4, p.511-540, August 2001 [doi>10.1017/S0960129501003322]
• 21: F. Pfenning , C. Elliot, Higher-order abstract syntax, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.199-208, June 20-24, 1988, Atlanta, Georgia, United States
• 22: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 23: Andrew M. Pitts , Murdoch Gabbay, A Metalanguage for Programming with Bound Names Modulo Renaming, Proceedings of the 5th International Conference on Mathematics of Program Construction, p.230-255, July 03-05, 2000
• 24: Carsten Schurmann , Joelle Despeyroux , Frank Pfenning, Primitive recursion for higher-order abstract syntax, Theoretical Computer Science, v.266 n.1-2, p.1-57, 09/06/2001 [doi>10.1016/S0304-3975(00)00418-7]
• 25: C. Schürmann, R. Fontana, and Y. Liao. Delphin: Functional programming with deductive systems. Available at http://cs-www.cs.yale.edu/homes/carsten/, 2002.
• 26: Eijiro Sumii , Naoki Kobayashi, A Hybrid Approach to Online and Offline Partial Evaluation, Higher-Order and Symbolic Computation, v.14 n.2-3, p.101-142, September 2001 [doi>10.1023/A:1012984529382]
• 27: Valery Trifonov , Bratin Saha , Zhong Shao, Fully reflexive intensional type analysis, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.82-93, September 2000
• 28: 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]
• 29: G. Washburn. Modal typing for specifying run-time code generation. Available from http://www.cis.upenn.edu/~geoffw/research/, 2001.
• 30: Stephanie Weirich, Higher-Order Intensional Type Analysis, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.98-114, April 08-12, 2002
• 31: Hongwei Xi , Chiyan Chen , Gang Chen, Guarded recursive datatype constructors, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.224-235, January 15-17, 2003, New Orleans, Louisiana, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism; Control structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs; Program and recursion schemes; Type structure
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Modal logic; Lambda calculus and related systems

General Terms:
Languages

Keywords:
catamorphism, higher-order abstract syntax, modal type system, parametric polymorphism, parametricity