An open and shut typecase

ABSTRACT

Two different ways of defining ad-hoc polymorphic operations commonly occur in programming languages. With the first form polymorphic operations are defined inductively on the structure of types while with the second form polymorphic operations are defined for specific sets of types.In intensional type analysis operations are defined by induction on the structure of types. Therefore no new cases are necessary for user-defined types, because these types are eQuivalent to their underlying structure. However, intensional type analysis is "closed" to extension, as the behavior of the operations cannot be differentiated for the new types, thus destroying the distinctions that these types are designed to express.Haskell type classes on the other hand define polymorphic operations for sets of types. Operations defined by class instances are considered "open"---the programmer can add instances for new types without modifying existing code. However, the operations must be extended with specialized code for each new type, and it may be tedious or even impossible to add extensions that apply to a large universe of new types.Both approaches have their benefits, so it is important to let programmers decide which is most appropriate for their needs. In this paper, we define a language that supports both forms of ad-hoc polymorphism, using the same basic constructs.

REFERENCES

• 1: Martín Abadi , Luca Cardelli , Benjamin Pierce , Gordon Plotkin, Dynamic typing in a statically typed language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.2, p.237-268, April 1991 [doi>10.1145/103135.103138]
• 2: 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.
• 3: R. Cockett and T. Fukushima. About Charity. Yellow Series Report No. 92/480/18, Department of Computer Science, The University of Calgary, June 1992.
• 4: Karl Crary , Stephanie Weirich, Flexible type analysis, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.233-248, September 27-29, 1999, Paris, France
• 5: Karl Crary , Stephanie Weirich , Greg Morrisett, Intensional polymorphism in type-erasure semantics, Journal of Functional Programming, v.12 n.6, p.567-600, November 2002 [doi>10.1017/S0956796801004282]
• 6: Derek Dreyer , Karl Crary , Robert Harper, A type system for higher-order modules, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.236-249, January 15-17, 2003, New Orleans, Louisiana, USA
• 7: V. Gapeyev and B. Pierce. Regular object types. In Proc. 10th International Workshops on Foundations of Object-Oriented Languages, FOOL '03, New Orleans, LA, USA, Jan. 2003.
• 8: J. Garrigue. Programming with polymorphic variants. In ML Workshop, Sept. 1998.
• 9: J.-Y. Girard. Interprétation fonctionelle et élimination des coupures de l'arithmétiQue d'ordre supérieur. PhD thesis, Université Paris VII, 1972.
• 10: Neal Glew, Type dispatch for named hierarchical types, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.172-182, September 27-29, 1999, Paris, France
• 11: Dan Grossman , Greg Morrisett , Steve Zdancewic, Syntactic type abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.6, p.1037-1080, Nov. 2000 [doi>10.1145/371880.371887]
• 12: Robert Harper , Mark Lillibridge, A type-theoretic approach to higher-order modules with sharing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.123-137, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176927]
• 13: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• 14: R. Hinze. Polytypic values possess polykinded types. Science of Computer Programming, 43(2--3):129--159, 2002. MPC Special Issue.
• 15: R. Hinze and S. Peyton Jones. Derivable type classes. In G. Hutton, editor, Proceedings of the Fourth Haskell Workshop, Montreal, Canada, September 17, 2000, volume 41.1 of Electronic Notes in Theoretical Computer Science. Elsevier Science, Aug. 2000.
• 16: Haruo Hosoya , Benjamin C. Pierce, Regular expression pattern matching for XML, Journal of Functional Programming, v.13 n.6, p.961-1004, November 2003 [doi>10.1017/S0956796802004410]
• 17: Patrik Jansson , Johan Jeuring, PolyP—a polytypic programming language extension, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.470-482, January 15-17, 1997, Paris, France [doi>10.1145/263699.263763]
• 18: C. Jay. Programming in FISh. International Journal on Software Tools for Technology Transfer, 2:307--315, 1999.
• 19: C. B. Jay , G. Bellè , E. Moggi, Functorial ML, Journal of Functional Programming, v.8 n.6, p.573-619, November 1998 [doi>10.1017/S0956796898003128]
• 20: Ralf Lämmel , Simon Peyton Jones, Scrap your boilerplate: a practical design pattern for generic programming, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 21: James J. Leifer , Gilles Peskine , Peter Sewell , Keith Wansbrough, Global abstraction-safe marshalling with hash types, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.87-98, August 25-29, 2003, Uppsala, Sweden
• 22: Andres Löh , Dave Clarke , Johan Jeuring, Dependency-style generic haskell, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.141-152, August 25-29, 2003, Uppsala, Sweden
• 23: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 24: Greg Morrisett , Matthias Felleisen , Robert Harper, Abstract models of memory management, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.66-77, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224182]
• 25: S. Peyton Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, 2003.
• 26: D. Rémy, Type checking records and variants in a natural extension of ML, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.77-88, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75284]
• 27: Didier Rémy, Type inference for records in natural extension of ML, Theoretical aspects of object-oriented programming: types, semantics, and language design, MIT Press, Cambridge, MA, 1994
• 28: J. C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing '83, pages 513--523. North-Holland, 1983. Proceedings of the IFIP 9th World Computer Congress.
• 29: Andreas Rossberg, Generativity and dynamic opacity for abstract types, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.241-252, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888274]
• 30: Christopher A. Stone , Robert Harper, Deciding type equivalence in a language with singleton kinds, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325724]
• 31: 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
• 32: Joseph C. Vanderwaart , Derek Dreyer , Leaf Petersen , Karl Crary , Robert Harper , Perry Cheng, Typed compilation of recursive datatypes, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 33: D. Vytiniotis, G. Washburn, and S. Weirich. An open and shut typecase. Technical Report MS-CIS-04-26, University of Pennsylvania, 2004. Available from http://www.cis.upenn.edu/~dimitriv/itaname.
• 34: 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]
• 35: 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
• 36: 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]
• 37: M. Zenger and M. Odersky. Independently extensible solutions to the expression problem. Technical Report IC/2004/33, EPFL Lausanne, Switzerland, 2004.

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: Type structure; Program and recursion schemes; Functional constructs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Languages, Theory

Keywords:
ad-hoc polymorphism, generativity, intensional type analysis, reflexivity