ABSTRACT
A Hindley-Milner type system such as ML's seems to prohibit type-indexed values, i.e., functions that map a family of types to a family of values. Such functions generally perform case analysis on the input types and return values of possibly different types. The goal of our work is to demonstrate how to program with type-indexed values within a Hindley-Milner type system.Our first approach is to interpret an input type as its corresponding value, recursively. This solution is type-safe, in the sense that the ML type system statically prevents any mismatch between the input type and function arguments that depend on this type.Such specific type interpretations, however, prevent us from combining different type-indexed values that share the same type. To meet this objection, we focus on finding a value-independent type encoding that can be shared by different functions. We propose and compare two solutions. One requires first-class and higher-order polymorphism, and, thus, is not implementable in the core language of ML, but it can be programmed using higher-order functors in Standard ML of New Jersey. Its usage, however, is clumsy. The other approach uses embedding/projection functions. It appears to be more practical.We demonstrate the usefulness of type-indexed values through examples including type-directed partial evaluation, C printf-like formatting, and subtype coercions. Finally, we discuss the tradeoffs between our approach and some other solutions based on more expressive typing disciplines.
- 1.Martin Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. Dynamic typing in a statically typed language. A CM Transactions on Programming Language.s and Systems, t3(2):237-268., April 1991. Google ScholarDigital Library
- 2.Martin Abadi, Luca Cardelli, Benjamin Pierce, and Didiet R~m,~. Dynamic typing in polymorphic languages. J o'w.,nal ofFunctional Programming, 5(1): 111-130, Janu ary 1995Google Scholar
- 3.Andrew W. Appel and David B. MacQueen. Standard ML of New Jersey. In Jan Maluszyfiski and Martin Wirsing, editors, Third International Symposium on Programming Language Implementation and Logic Programming, number 528 in Lecture Notes in Computer Science, pages 1-13, Passau, Germany, August 1991. Springer-Verlag.Google Scholar
- 4.William Clinger and Jonathan Rees, editors. Revised4 report on the algorithmic language Scheme. LISP Pointers, IV(3):1-55, July-September 199t. Google ScholarDigital Library
- 5.Olivier Danvy. Type-directed partial evaluation. In Google ScholarDigital Library
- 6.Olivier Danvy. Formatting strings in ML. Research Series RS-98-5, BRICS, Department of Computer Science, University of Aarhus, March 1998. To appear in the Journal of Functional Programming.Google Scholar
- 7.Olivier Danvy. A simple solution to type specialization. Research Series RS-98-1, BRICS, Department of Computer Science, University of Aarhus, January 1998. To appear in the Proceedings of the ~5th International Colloquium on Automata, Languages, and Programming. Google ScholarDigital Library
- 8.Olivier Danvy and Peter Dybjer, editors. Preliminary Proceedings of the 1998 A PPSEM Workshop on Normalization by Evaluation, NBE '98, (GSteborg, Sweden, May 8-9, 1998), number NS-98-1 in BRICS Notes Series, BRICS, Department of Computer Science, University of Aarhus, May 1998.Google Scholar
- 9.Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Steele {29}, pages 258-283. Google Scholar
- 10.Jean-Yves Girard. The system F of variable types, fifteen years later. Theoretical Computer Science, 45(2):159-192, 1986. Google ScholarDigital Library
- 11.Cordelia Hall, Kevin Hammond, Simon Peyton-Jones, and Philip Wadler. Type classes in Haskell. A CM Transactions on Programming Languages and Systems, 18(2):109-138, March 1996. Google ScholarDigital Library
- 12.Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In Peter Lee, editor, Proceedings of the Twenty-Second Annual A CM Symposium on Principles of Programming Lan. guages, pages 130-141, San Francisco, California, January 1995. ACM Press. Google ScholarDigital Library
- 13.Fritz Henglein. Dynamic typing: syntax and proof theory. Science of Computer Programming, 22(3):197-230, June 1994. Google ScholarDigital Library
- 14.J. Roger Hindley. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29-60, 1969.Google Scholar
- 15.Mark P. Jones. A system of constructor classes: overloading and implicit higher-order polymorphism. Journal of Functional Programming, 5(1):1-35, January 1995. An earlier version appeared in FPCA '93. Google ScholarDigital Library
- 16.Mark P. Jones. First-class polymorphism with type inference. In Jones {17}, pages 483-496. Google Scholar
- 17.Nell D. Jones, editor. Proceedings of the Twenty. Fourth Annual A CM Symposium on Principles of Programming Languages, Paris, France, January 1997. ACM Press.Google Scholar
- 18.Nell D. L ones, Carsten K. Gomard, and Peter Sestoft. Pa'c~ial Evaluation and Automatic Program Generation. Prentice Hall International, International Series in Computer Science, June 1993. Google ScholarDigital Library
- 19.Andrew Kennedy. Relational parametricity and units of measure. In Jones {17}, pages 442-455. Google Scholar
- 20.Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, December 1978.Google ScholarCross Ref
- 21.Robin Milner, Mads Torte, Robert Harper, and David MacQuee:,. The Definition of Standard ML (Revised). The MIT Press, 1997. Google ScholarDigital Library
- 22.John C. Mitchell. Coercion and type inference. In Ken Kennedy, editor, Proceedings of the Eleventh Annual A CM Symposium on Principles of Programming Languages, pages 175-185, Salt Lake City, Utah, January 1984. Google ScholarDigital Library
- 23.Martin Odersky and Konstantin L~ufer. Putting type annotations to work. In Steele {29}, pages 54-67. Google Scholar
- 24.John Peterson, Kevin Hammond, et al. Report on the programming language Haskell, a non-strict purelyfunction.m programming language, version 1.4. Available at the Haskell homepage: http://www.haskell.org, April 1997.Google Scholar
- 25.John C. Reynolds. Towards a theory of type structure. In Programming Symposium, number 19 in Lecture Notes in Computer Science, pages 408-425, Paris, France, April 1974. Springer-Verlag. Google ScholarDigital Library
- 26.Morten Rhiger. A study in higher-order programming languages. Master's thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 1997.Google Scholar
- 27.Kristoffe~ Fcose. Type-directed partial evaluation in a pure filncdonal language. In Danvy and Dybjer {8}.Google Scholar
- 28.Mark Shields, Tim Sheard, and Simon Peyton Jones. Dynamic wping as staged type inference. In Luca Cardetl}, editor, Proceedings of the Twenty. Fifth Annual A 6L~4 Symposium on Principles of Programming Languages, pages 289-302, San Diego, California, January 1998. ACM Press. Google ScholarDigital Library
- 29.Guy L. Steele, editor. Proceedings of the Twenty. Third Annual /! CM Symposium on Principles of Programruing Languages, St. Petersburg Beach, Florida, January 199~ ACM Press.Google Scholar
- 30.Walid Taha and Tim Sheard. Multi-stage programming. In Mads Torte, editor, Proceedings of the 1997 A CM SIOPLAN International Conference on P~nctional Programming, pages 321-321, Amsterdam, The Netherlands, June 1997. ACM Press. Google ScholarDigital Library
- 31.Mads Torte. Principal signatures for higher-order program modules. Journal of Functional Programming, 4(3):285-.335, July 1994.Google Scholar
- 32.R.en6 V~tergaard. From proof normalization to compiler generation and type-directed change-ofrepresentation. Master's thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, May 1997.Google Scholar
Index Terms
- Encoding types in ML-like languages
Recommendations
Encoding types in ML-like languages
A Hindley-Milner type system such as ML's seems to prohibit type-indexed values, i.e., functions that map a family of types to a family of values. Such functions generally perform case analysis on the input types and return values of possibly different ...
Encoding types in ML-like languages
Mathematical foundations of programming semanticsThis article presents several general approaches to programming with type-indexed families of values within a Hindley-Milner type system. A type-indexed family of values is a function that maps a family of types to a family of values. The function ...
Comments