Patrik Jansson
Johan Jeuring
ABSTRACT
Many functions have to be written over and over again for different datatypes, either because datatypes change during the development of programs, or because functions with similar functionality are needed on different datatypes. Examples of such functions are pretty printers, debuggers, equality functions, unifiers, pattern matchers, rewriting functions, etc. Such functions are called polytypic functions. A polytypic function is a function that is defined by induction on the structure of user-defined datatypes. This paper extends a functional language (a subset of Haskell) with a construct for writing polytypic functions. The extended language type checks definitions of polytypic functions, and infers the types of all other expressions using an extension of Jones' theories of qualified types and higher-order polymorphism. The semantics of the programs in the extended language is obtained by adding type arguments to functions in a dictionary passing style. Programs in the extended language are translated to Haskell.
- 1.Timothy C. Bell, John G. Cleary, and lanH. Witten. Text Compression. PrenticeHail, 1990, Google Scholar
Digital Library
- 2.G. Bell#, C.B. Jay, and E. Moggi. Functorial ML. In PLILP '96. Springer-Verlag, 1996. LNCS Google ScholarDigital Library
- 3.C. BShm and A. Berarducci. Automatic synthesis of type :A-programs on term algebras. Theoretical Compeer Science, 39:135-154,1 1985,Google ScholarCross Ref
- 4.Robert D. Cameron. Source encoding using syntactic information source models. IEEE Transactions on Information Theory, 34(4):843-850, 1988.Google ScholarCross Ref
- 5.J.F. Contla. Compact coding of synt#tically correct source programs. Software-Practice and Experience, 15(7) :625,636, 1985. Google ScholarDigital Library
- 6.L. Damas and R. Milner. Principal type,schemes for functional programs. In gth Symposium on Priciples of Prograraming Languages, POPL '82, pages 207-212, 1982.# .. Google ScholarDigital Library
- 7.N. Dershowitz. A note on simplification orderings. Information Processing Letters, 9(5):212-215, 1979.Google ScholarCross Ref
- 8.J.H. Fasel, P, Hudak, S Peyton Jones, and P. Wadler. Sigplan Notices special issue on the Functional Programming Language H#kell. A CM SIGPLAN notices, 27(5), 1992.Google Scholar
- 9.P. Freyd. Recursive types reduced to inductive types. In Proceedings Logic in Computer Science, LICS '90, pages 498-507, 1990.Google ScholarCross Ref
- 10.Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In#2#ndSymposium on Priciples of Programming Languages, POPL '95, pages 130-141, 1995. Google ScholarDigital Library
- 11.P. Jansson. Polytypism and polytypic unification. Master's thesis, Chalmers University of Technology and University of GSteborg,# 1995.Google Scholar
- 12.P. Jansson and J. Jeuring. Polytypic unification -- implementing polytypic functions with constructor classes. In preparation, see http://www, cs. chalmers se/'johanj, 1996.Google Scholar
- 13.C. Barry Jay. Polynomial polymorphism. In Proceedings of the Eighteenth Australasian Computer Science Conference, pages 237-243, 1995.Google Scholar
- 14.C. Barry Jay, A semantics for shape. Science of Computer Programming, 25:251-283, 1995. Google ScholarDigital Library
- 15.J. Jeuring. Polytypic pattern matching. In Conference Record of FPCA '95, 8IGPLAN-SIGARGH- WG2.8 Conference on Functional Programming Languages and Computer Architecture, pages 238- 248, 1995. Google ScholarDigital Library
- 16.J. Jeuring and P. Jansson. Polytypic programming. In J. Launchbury, E. Meijer, and T. Sheard, editors, Proceedings of the Second International Summer School on Advanced Functional Programming Techniques, pages 68-114. Springer-Verlag, 1996. LNCS 1129. Google ScholarDigital Library
- 17.Mark P. Jones. Dictionary-free overloading by partial evaluation, in A CM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, Orlando, Florida, June 1994.Google Scholar
- 18.Mark P. Jones. Qualified Types: Theory and!Practice. Cambridge University Press, 1994. Google ScholarDigital Library
- 19.Mark P. Jones. Functional programming with overloading and higher-order p01ymorphism. In J. Jeuring and E. Meijer, editors, Advan#d Functional Programming, LNCS 925, pages 97-136. Springer- Verlag, 1995. Google ScholarDigital Library
- 20.Mark P. Jones. A system of constructor closes: overloading and implicit higher-order polymorphism. Journal of Functional Programming, pages 1-35, 1995.Google Scholar
- 21.J.W. Klop. Term rewriting systems. In Handbook of Logic in Computer Science, pages 1-116. Oxford University Press, 1992. # Google ScholarDigital Library
- 22.D.E. Knuth and P.B.# Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263-29?. Pergamon Press, 1970.Google Scholar
- 23.K.J. Lieberherr, I. Silva-Lepe, and C. Xiao. Adaptive object-oriented programming -- using graphbased customization. Communications of the A CM, pages 94-101, 1994. Google ScholarDigital Library
- 24.G. Malcolm. Data structures and program transformation. Science of Computer Programming, 14:255-279, 1990. Google ScholarDigital Library
- 25.A. MarteUi, C. Moiso, and C.F. Rossi. An algorithm for unification in equational theories. In Proc. Symposium on Logic Programming, pages 180-186, 1986.Google Scholar
- 26.L. Meertens. Param0rphisms. Formal Aspects of Computing, 4(5):413-425, 1992.Google ScholarCross Ref
- 27.E. Meijer, M. Fokkinga, and R. Paterson. Fhnctional programming with b#manas, lenses, ei#- velopes, and barbed .wire. In J, Hughes, editor, Proceedings of the 5th A CM Conference on #Func. tional Programming Languages and Computer Architecture, FPCA '91, pages 124-144, 1991. Google ScholarDigital Library
- 28.E. Meijer and G. Hutton. Bananas in space" Extending fold and unfold to exponenti~ types. In Conference Record of FPCA '95, SIGPLAN- SIGARCH- WG#.8 Conference on Functional Programming Languages and Computer Architecture, pages 324-333, 1995. Google ScholarDigital Library
- 29.j. Palsberg, C. Xiao, and K. Lieberherr. Efficient implementation of adaptive software. TOPLAS, 1995. Google ScholarDigital Library
- 30.T. Sheard and':N: Nelson' Type safe abstractions using program generat0rs.# Unpublished manuscript, 1995. # #Google Scholar
- 31.Tim Sheard. Automatic generation anduse of abstract structure operators. A GM Transactions on Programming Languages and Systems, 13 (4):531- 557, 1991. .. Google ScholarDigital Library
- 32.J. Ziv and A, Lempel. A universal algorithm for sequential datacompressi0n, iEEE Transactions on# Information Theory, 23(3):337-343, 1977.Google Scholar
Index Terms
- PolyP—a polytypic programming language extension
Recommendations
Type-safe run-time polytypic programming
Polytypic programming is a way of defining type-indexed operations, such as map, fold and zip, based on type information. Run-time polytypic programming allows that type information to be dynamically computed – this support is essential in modern ...
Polytypic programming in haskell
IFL'03: Proceedings of the 15th international conference on Implementation of Functional LanguagesA polytypic (or generic) program captures a common pattern of computation over different datatypes by abstracting over the structure of the datatype. Examples of algorithms that can be defined polytypically are equality tests, mapping functions and ...
Formal polytypic programs and proofs
The aim of our work is to be able to do fully formal, machine verified proofs over Generic Haskell-style polytypic programs. In order to achieve this goal, we embed polytypic programming in the proof assistant Coq and provide an infrastructure for ...
Comments