article

Encoding types in ML-like languages

Author:

Zhe YangAuthors Info & Claims

Theoretical Computer Science, Volume 315, Issue 1

Pages 151 - 190

https://doi.org/10.1016/j.tcs.2003.11.017

Published: 05 May 2004 Publication History

Abstract

This 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 performs a case analysis on the input types and returns values of possibly different types. Such a case analysis on types seems to be prohibited by the Hindley-Milner type system. Our approaches solve the problem by using type encodings. The compile-time types of the type encodings reflect the types themselves, thereby making the approaches type-safe, in the sense that the underlying type system statically prevents any mismatch between the input type and the function arguments that depend on this type.A type encoding could be either value-dependent, meaning that the type encoding is tied to a specific type-indexed family, or value-independent, meaning that the type encoding can be shared by various type-indexed families. Our first approach is value-dependent: we simply interpret a type as its corresponding value. Our second approach provides value-independent type encodings through embedding and projection functions; they are universal type interpretations, in that they can be used to compute other type interpretations. We also present an alternative approach to value-independent type encodings, using higher-order functors.We demonstrate our techniques through applications such as C printf-like formatting, type-directed partial evaluation, and subtype coercions.

References

[1]

{1} M. Abadi, L. Cardelli, B. Pierce, G. Plotkin, Dynamic typing in a statically typed language, ACM Trans. Programming Languages and Systems 13 (2) (1991) 237-268.]]

Digital Library

[2]

{2} M. Abadi, L. Cardelli, B. Pierce, D. Rémy, Dynamic typing in polymorphic languages, J. Funct. Programming 5 (1) (1995) 111-130.]]

[3]

{3} A.W. Appel, D.B. MacQueen, Standard ML of New Jersey, in: J. Maluszynski, M. Wirsing (Eds.), Third Internat. Symp. on Programming Language Implementation and Logic Programming, Lecture Notes in Computer Science, Vol. 528 Passau, Germany, August 1991, Springer, Berlin, pp. 1-13.]]

[4]

{4} O. Danvy, Type-directed partial evaluation, in: G.L. Steele (Ed.), Proc. 23rd Annu. ACM Symp. on Principles of Programming Languages, St. Petersburg, Beach, FL, January 1996, pp. 242-257.]]

[5]

{5} O. Danvy, Private Communication, 1998.]]

[6]

{6} O. Danvy, Functional unparsing, J. Funct. Programming 8 (1998) 621-625.]]

Digital Library

[7]

{7} O. Danvy, A simple solution to type specialization, in: K.G. Larsen, S. Skyum, G. Winskel (Eds.), Proc. 25th Internat. Colloq. on Automata, Languages, and Programming, Lecture Notes in Computer Science, Vol. 1443, Springer, Berlin, 1998, pp. 908-917.]]

[8]

{8} O. Danvy, Type-directed partial evaluation, in: J. Hatcliff, T.E. Mogensen, P. Thiemann (Eds.), Partial Evaluation--Practice and Theory; Proc. 1998 DIKU Summer School, Lecture Notes in Computer Science. Vol. 1706, Copenhagen, Denmark, July 1998, Springer, Berlin, pp. 367-411.]]

[9]

{9} O. Danvy, P. Dybjer (Eds.), Preliminary Proc. 1998 APPSEM Workshop on Normalization by Evaluation. NBE '98, Güteborg, Sweden, May 8-9, 1998, BRICS Notes Series, Vol. NS-98-1, BRICS, Department of Computer Science, University of Aarhus, May 1998.]]

[10]

{10} R. Davies, F. Pfenning, A modal analysis of staged computation, in: G.L. Steele (Ed.), Proc. 23rd Annu. ACM Symp. on Principles of Programming Languages, St. Petersburg, Beach, FL, January 1996, pp. 258-283; Extended version, J. ACM 48 (2001) 555-604.]]

[11]

{11} A. Filinski, A semantic account of type-directed partial evaluation, in: G. Nadathur (Ed.), Internat. Conf. Principles and Practice of Declarative Programming, Lecture Notes in Computer Science, Vol. 1702, Paris, France, September 1999, pp. 378-395.]]

[12]

{12} J.-Y. Girard, The system F of variable types, fifteen years later. Theoret. Comput. Sci. 45 (2) (1986) 159-192.]]

Digital Library

[13]

{13} B. Grobauer, Z. Yang, The second Futamura projection for type-directed partial evaluation, in: J.L. Lawall (Ed.), Proc. ACM SIGPLAN Workshop on Partial Evaluation and Semantics--Based Program Manipulation, SIGPLAN Notices, Vol. 34 (11), Boston, MA, November 2000, ACM Press, pp. 22-32; Extended version, J. Higher-Order Symbolic Comput. 14 (2/3) (2001).]]

[14]

{14} C. Hall, K. Hammond, S. Peyton-Jones, P. Wadler, Type classes in Haskell, ACM Trans. Program. Languages Systems 18 (2) (1996) 109-138.]]

Digital Library

[15]

{15} R. Harper, G. Morrisett, Compiling polymorphism using intensional type analysis, in: P. Lee (Ed.), Proc. 22nd Annu. ACM Symp. on Principles of Programming Languages, San Francisco, California, January, 1995, pp. 130-141.]]

[16]

{16} F. Henglein, Dynamic typing: syntax and proof theory, Sci. Comput. Program. 22 (3) (1994) 197-230.]]

Digital Library

[17]

{17} J.R. Hindley, The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc. 146 (1969) 29-60.]]

[18]

{18} J. Hughes, The design of a pretty-printing library, in: J. Jeuring, E. Meijer (Eds.), Advanced Functional Programming, Lecture Notes in Computer Science, Vol. 925, Springer, Berlin, 1995, pp. 53-96.]]

[19]

{19} P. Jansson, J. Jeuring, PolyP--a polytypic programming language extension, in: N.D. Jones (Ed.), Proc. 24th Annu. ACM Symp. on Principles of Programming Languages, Paris, France, January 1997, pp. 470-482.]]

[20]

{20} M.P. Jones, A system of constructor classes: overloading and implicit higher-order polymorphism, J. Funct. Program. 5 (1) (1995) 1-35, An earlier version appeared in FPCA '93.]]

[21]

{21} M.P. Jones, First-class polymorphism with type inference, in: N.D. Jones (Ed.), Proc. 24th Annu. ACM Symp. on Principles of Programming Languages, Paris, France, January 1997, pp. 483-496.]]

[22]

{22} N.D. Jones (Ed.), Proc. 24th Annu. ACM Symp. on Principles of Programming Languages, Paris, France, January 1997.]]

[23]

{23} N.D. Jones, C.K. Gomard, P. Sestoft, Partial Evaluation and Automatic Program Generation, Prentice-Hall International, Englewood Cliffs, NJ, 1993, Available online at http://www.dina. kvl.dk/~sestoft/pebook/pebook.html.]]

[24]

{24} R. Kelsey, W. Clinger, J. Rees (Eds.), Revised5 Report on the algorithmic language Scheme, Higher-Order and Symbol. Comput. 11 (1) (1998) 7-105; Also appears in ACM SIGPLAN Notices 33 (9) (1998); Available online at http://www.brics.dk/~hosc/11-1/.]]

[25]

{25} A. Kennedy, Relational parametricity and units of measure, in: N.D. Jones (Ed.), Proc. 23rd Annu. ACM Symp. on Principles of Programming Languages, Paris, France, January 1997, pp. 442-455.]]

[26]

{26} R. Milner, A theory of type polymorphism in programming, J. Comput. System Sci. 17 (1978) 348-375.]]

[27]

{27} R. Milner, M. Tofte, R. Harper, D. MacQueen, The Definition of Standard ML (Revised), The MIT Press, Cambridge, MA, 1997.]]

[28]

{28} J.C. Mitchell, Coercion and type inference, in: K. Kennedy (Ed.), Proc. 11th Annu. ACM Symp. on Principles of Programming Languages, Salt Lake City, Utah, January 1984, pp. 175-185.]]

[29]

{29} E. Moggi, Computational lambda-calculus and monads, in: R. Parikh (Ed.), Proc. 4th Annu. IEEE Symp. on logic in Computer Science, Pacific Grove, California, June 1989, pp. 14-23.]]

[30]

{30} M. Odersky, K. Läufer, Putting type annotations to work, in: G.L. Steele (Ed.), Proc. 23rd Annu. ACM Symp. on Principles of Programming Languages, St. Petersburg, Beach, FL, January 1996, pp. 54-67.]]

[31]

{31} J. Peterson, K. Hammond, et al., Report on the programming language Haskell, a nonstrict purely-functional programming language, version 1.4; available at the Haskell homepage: http://www.haskell.org April 1997.]]

[32]

{32} J.C. Reynolds, Towards a theory of type structure, in: Programming Symp., Lecture Notes in Computer Science. Vol. 19, Springer, Berlin, Paris, France, April 1974, pp. 408-425.]]

[33]

{33} M. Rhiger, A study in higher-order programming languages, Master's Thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 1997.]]

[34]

{34} K. Rose, Type-directed partial evaluation in a pure functional language, in: O. Danvy, P. Dybjer (Eds.), Preliminary Proc. 1998 APPSEM Workshop on Normalization by Evaluation, NBE '98, Göteborg, Sweden, May 8-9, 1998, BRICS Notes Series, Vol. NS-98-1, BRICS, Department of Computer Science, University of Aarhus, May 1998.]]

[35]

{35} M. Shields, T. Sheard, S.P. Jones, Dynamic typing as staged type inference, in: L. Cardelli (Ed.), Proc. 25th Annu. ACM Symp. on Principles of Programming Languages, San Diego, California, January 1998, pp. 289-302.]]

[36]

{36} G.L. Steele (Ed.), Proc. 23rd Annu. ACM Symp. on Principles of Programming Languages. St. Petersburg, Beach, FL, January 1996.]]

[37]

{37} W. Taha, T. Sheard, Multi-stage programming, in: M. Tofte (Ed.), Proc. 1997 ACM SIGPLAN Internat. Conf. on Functional Programming, Amsterdam, The Netherlands, June 1997, pp. 321-321.]]

[38]

{38} M. Tofte, Principal signatures for higher-order program modules, J. Funct. Program. 4 (3) (1994) 285-335.]]

[39]

{39} R. Vestergaard, From proof normlization to compiler generation and type-directed change-of-representation. Master's Thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, May 1997.]]

Cited By

Carette JKiselyov OShan C(2018)Finally tagless, partially evaluatedJournal of Functional Programming10.1017/S095679680900720519:5(509-543)Online publication date: 24-Dec-2018
https://dl.acm.org/doi/10.1017/S0956796809007205
Rhiger M(2018)Type-safe pattern combinatorsJournal of Functional Programming10.1017/S095679680800708919:2(145-156)Online publication date: 24-Dec-2018
https://dl.acm.org/doi/10.1017/S0956796808007089
Lindley SSumii E(2008)Many holes in hindley-milnerProceedings of the 2008 ACM SIGPLAN workshop on ML10.1145/1411304.1411313(59-68)Online publication date: 21-Sep-2008
https://dl.acm.org/doi/10.1145/1411304.1411313

Index Terms

Encoding types in ML-like languages
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
      2. Language types
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Encoding types in ML-like languages
ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming

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

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 ...
Refinement types for ML

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Theoretical Computer Science

Theoretical Computer Science Volume 315, Issue 1

Mathematical foundations of programming semantics

5 May 2004

300 pages

ISSN:0304-3975

Issue’s Table of Contents

Publisher

Elsevier Science Publishers Ltd.

United Kingdom

Publication History

Published: 05 May 2004

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Carette JKiselyov OShan C(2018)Finally tagless, partially evaluatedJournal of Functional Programming10.1017/S095679680900720519:5(509-543)Online publication date: 24-Dec-2018
https://dl.acm.org/doi/10.1017/S0956796809007205
Rhiger M(2018)Type-safe pattern combinatorsJournal of Functional Programming10.1017/S095679680800708919:2(145-156)Online publication date: 24-Dec-2018
https://dl.acm.org/doi/10.1017/S0956796808007089
Lindley SSumii E(2008)Many holes in hindley-milnerProceedings of the 2008 ACM SIGPLAN workshop on ML10.1145/1411304.1411313(59-68)Online publication date: 21-Sep-2008
https://dl.acm.org/doi/10.1145/1411304.1411313

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents