Stephanie Weirich
ABSTRACT
In a language with non-parametric or ad-hoc polymorphism, it is possible to determine the identity of a type variable at run-time. With this facility, we can write a function to convert a term from one abstract type to another, if the two hidden types are identical. However, the naive implementation of this function requires that the term be destructed and rebuilt. In this paper, we show how to eliminate this overhead using higher-order type abstraction. We demonstrate this solution in two frameworks for ad-hoc polymorphism: intensional type analysis and type classes.
- 1.M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in a statically-typed language. ACM Transactions on Programming Languages and Systems, 13(2):237-268, April 1991. Google Scholar
Digital Library
- 2.K. Crary, S.Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. In 1998 ACM International Conference onFunctional Programming, pages 301-312, Baltimore, Sept. 1998. Extended version published as Cornell University technical report TR98-1721. Google ScholarDigital Library
- 3.C. Dubois, F. Rouaix, and P. Weis. Extensional polymorphism. In Twenty-Second ACM Symposium on Principles of Programming Languages, pages 118-129, San Francisco, Jan. 1995. Google ScholarDigital Library
- 4.J.-Y. Girard. Interpretation fonctionelle et elimination des coupures de l'arithmetique d'ordre superieur. PhD thesis, Universite Paris VII, 1972.Google Scholar
- 5.J. Gosling, B. Joy, and G. Steele. The Java Language Speci~cation. Addison-Wesley, 1996. Google ScholarDigital Library
- 6.R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Twenty-Second ACM Symposium on Principles of Programming Languages, pages 130-141, San Francisco, Jan. 1995. Google ScholarDigital Library
- 7.F. Henglein. Dynamic typing. In B. Krieg-Br? uckner, editor, Fourth European Symposium on Programming, number 582 in Lecture Notes in Computer Science, pages 233-253. Springer-Verlag, Feb. 1992. Google Scholar
- 8.M. P. Jones. A system of constructor classes: overloading and implicit higher-order polymorphism. Journal of Functional Programming, 5(1), Jan. 1995.Google ScholarCross Ref
- 9.X. Leroy and M. Mauny. Dynamics in ML. In J. Hughes, editor, Functional Programming Languages and Computer Architecture, number 523 in Lecture Notes in Computer Science, pages 406-426. Springer-Verlag, Aug. 1991. Google ScholarDigital Library
- 10.R. Milner, M. Tofte, R. Harper, and D. MacQueen. The De~nition of Standard ML(Revised). TheMIT Press, Cambridge, Massachusetts, 1997. Google ScholarDigital Library
- 11.Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 271{283, St. Petersburg, Florida, Jan. 1996. Google ScholarDigital Library
- 12.J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3):470{502, July 1988. Google ScholarDigital Library
- 13.S. Peyton Jones and J. Hughes (editors). Report on the programming language Haskell 98, a non-strict purely functional language. Technical Report YALEU/DCS/RR-1106, Yale University, Department of Computer Science, Feb. 1999. Available from http://www.haskell.org/definition/.Google Scholar
- 14.J. C. Reynolds. Towards a theory of type structure. In Programming Symposium, volume 19 of Lecture Notes in Computer Science, pages 408-425, 1974. Google ScholarDigital Library
- 15.P. Wadler. Theorems for free! In Fourth Conference on Functional Programming Languages and Computer Architecture, London, Sept. 1989. Google ScholarDigital Library
- 16.P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad-hoc. In Sixteenth ACM Symposium on Principles of Programming Languages, pages 60-76. ACM, 1989. Google ScholarDigital Library
- 17.S. Weeks. NJ PearLS dynamically extensible data structures in Standard ML. Talk presented at New Jersey Programming Languages and Systems Seminar, Sept. 1998. Transparencies available at http://www.star-lab.com/sweeks/talks.html. 65Google Scholar
Index Terms
- Type-safe cast: (functional pearl)
Recommendations
Type-safe cast: (functional pearl)
In a language with non-parametric or ad-hoc polymorphism, it is possible to determine the identity of a type variable at run-time. With this facility, we can write a function to convert a term from one abstract type to another, if the two hidden types ...
An open and shut typecase
TLDI '05: Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementationTwo 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 ...
Ad-hoc polymorphism and dynamic typing in a statically typed functional language
WGP '10: Proceedings of the 6th ACM SIGPLAN workshop on Generic programmingStatic typing in functional programming languages such as Clean, Haskell, and ML is highly beneficial: it prevents erroneous behaviour at run time and provides opportunities for optimisations. However, dynamic typing is just as important as sometimes ...
Comments