Extracting programs from type class proofs

ABSTRACT

Standard presentations of type class translation schemes exhibit some surprising problems when translating Haskell 98 programs. We suggests ways how to fix these problems based on a formal framework for extracting programs from type class proofs. Our description includes type improvement and recursive dictionaries -- something which has not been formally studied before. Thus, we are able to advance the state of art of translating type classes and open up the possibility for new type class applications.

REFERENCES

• 1: S. Abdennadher. Operational semantics and confluence of constraint propagation rules. In Proc. of CP'97, LNCS, pages 252--266. Springer-Verlag, 1997.
• 2: Lennart Augustsson, Implementing Haskell overloading, Proceedings of the conference on Functional programming languages and computer architecture, p.65-73, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165191]
• 3: Michael Brandt , Fritz Henglein, Coinductive axiomatization of recursive type equality and subtyping, Fundamenta Informaticae, v.33 n.4, p.309-338, April 1998
• 4: Manuel M. T. Chakravarty , Gabriele Keller , Simon Peyton Jones, Associated type synonyms, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 5: Bart Demoen , Maria J. García de la Banda , Warwick Harvey , Kim Marriott , Peter J. Stuckey, An Overview of HAL, Proceedings of the 5th International Conference on Principles and Practice of Constraint Programming, p.174-188, October 11-14, 1999
• 6: G. J. Duck, S. Peyton Jones, P. J. Stuckey, and M. Sulzmann. Sound and decidable type inference for functional dependencies. In Proc. of ESOP'04, volume 2986 of LNCS, pages 49--63. Springer-Verlag, 2004.
• 7: Karl-Filip Faxén, A static semantics for Haskell, Journal of Functional Programming, v.12 n.5, p.295-357, July 2002 [doi>10.1017/S0956796802004380]
• 8: T. Frühwirth. Constraint handling rules. In Constraint Programming: Basics and Trends, LNCS. Springer-Verlag, 1995.
• 9: Glasgow haskell compiler home page. http://www.haskell.org/ghc/.
• 10: Cordelia V. Hall , Kevin Hammond , Simon L. Peyton Jones , Philip L. Wadler, Type classes in Haskell, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.2, p.109-138, March 1996 [doi>10.1145/227699.227700]
• 11: R. Harper, F. Honsell, and G. Plotkin. A Framework for Defining Logics. In Proceedings 2nd Annual IEEE Symp. on Logic in Computer Science, LICS'87, pages 194--204. IEEE Computer Society Press, 1987.
• 12: F. Henderson et al. The Mercury language reference manual, 2001. http://www.cs.mu.oz.au/research/mercury/.
• 13: W.A. Howard. The formulae-as-types notion of construction. In J.P. Seldin and J.R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, λ Calculus and Formalism, pages 479--490. Academic Press, 1980.
• 14: Hugs home page. haskell.cs.yale.edu/hugs/.
• 15: D. Jeffery, F. Henderson, and Z. Somogyi. Type classes in Mercury. In Proc. Twenty-Third Australasian Computer Science Conf., volume 22 of Australian Computer Science Communications, pages 128--135. IEEE Computer Society Press, January 2000.
• 16: Mark P. Jones, A system of constructor classes: overloading and implicit higher-order polymorphism, Proceedings of the conference on Functional programming languages and computer architecture, p.52-61, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165190]
• 17: Mark P. Jones, Simplifying and improving qualified types, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.160-169, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224198]
• 18: 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
• 19: Stefan Kaes, Parametric Overloading in Polymorphic Programming Languages, Proceedings of the 2nd European Symposium on Programming, p.131-144, March 21-24, 1988
• 20: Ralf Lämmel , Simon Peyton Jones, Scrap your boilerplate with class: extensible generic functions, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 21: J.-L. Lassez , M. J. Maher , K. Marriott, Unification revisited, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• 22: K. Z. M. Lu and M. Sulzmann. An implementation of subtyping among regular expression types. In Proc. of APLAS'04, LNCS, pages 57--73. Springer-Verlag, 2004.
• 23: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Information and Control, v.71 n.1-2, p.95-130, Oct/Nov. 1986 [doi>10.1016/S0019-9958(86)80019-5]
• 24: R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348--375, Dec 1978.
• 25: John Peterson , Mark Jones, Implementing type classes, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.227-236, June 21-25, 1993, Albuquerque, New Mexico, United States
• 26: S. Peyton Jones. Haskell 98 Language and Libraries: The Revised Report, 2003. Also see http://www.haskell.org/definition/.
• 27: S. Peyton Jones, M. P. Jones, and E. Meijer. Type classes: an exploration of the design space. In Haskell Workshop, June 1997.
• 28: M.J. Plasmeijer and M.C.J.D. van Eekelen. Language report Concurrent Clean. Technical Report CSI-R9816, Computing Science Institute, University of Nijmegen, Nijmegen, The Netherlands, June 1998. ftp://ftp.cs.kun.nl/pub/Clean/Clean13/doc/refman13.ps.gz.
• 29: F. Pottier, 2004. personal communication.
• 30: Z. Shao. An overview of the FLINT/ML compiler. In Proc. of ACM SIGPLAN Workshop on Types in Compilation (TIC'97), 1997.
• 31: Zhong Shao , Valery Trifonov , Bratin Saha , Nikolaos Papaspyrou, A type system for certified binaries, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.1, p.1-45, January 2005 [doi>10.1145/1053468.1053469]
• 32: J.R. Shoenfield. Mathematical Logic. Addison-Wesley, 1967.
• 33: Peter J. Stuckey , Martin Sulzmann, A theory of overloading, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.6, p.1216-1269, November 2005 [doi>10.1145/1108970.1108974]
• 34: M. Sulzmann and J. Wazny. Chameleon. http://www.comp.nus.edu.sg/~sulzmann/chameleon.
• 35: Satish R. Thatté, Semantics of type classes revisited, Proceedings of the 1994 ACM conference on LISP and functional programming, p.208-219, June 27-29, 1994, Orlando, Florida, United States
• 36: P. Wadler , S. Blott, How to make ad-hoc polymorphism less ad hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.60-76, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75283]
• 37: S. Wehr, 2005. http://www.haskell.org//pipermail/haskell/2005-October/016695.html.
• 38: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]

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.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Theory

Keywords:
overloading, proofs are programs principle, type classes