Article

A type system for well-founded recursion

Author:

Derek DreyerAuthors Info & Claims

POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 293 - 305

https://doi.org/10.1145/964001.964026

Published: 01 January 2004 Publication History

Get Access

Abstract

In the interest of designing a recursive module extension to ML that is as simple and general as possible, we propose a novel type system for general recursion over effectful expressions. The presence of effects seems to necessitate a backpatching semantics for recursion similar to that of Scheme. Our type system ensures statically that recursion is well-founded---that the body of a recursive expression will evaluate without attempting to access the undefined recursive variable---which avoids some unnecessary run-time costs associated with backpatching. To ensure well-founded recursion in the presence of multiple recursive variables and separate compilation, we track the usage of individual recursive variables, represented statically by "names". So that our type system may eventually be integrated smoothly into ML's, reasoning involving names is only required inside code that uses our recursive construct and need not infect existing ML code, although instrumentation of some existing code can help to improve the precision of our type system.

References

[1]

Samson Abramsky and Chris Hankin, editors. Abstract Interpretation of Declarative Languages. Ellis Horwood Limited, 1987.

Digital Library

Google Scholar

[2]

Davide Ancona, Sonia Fagorzi, Eugenio Moggi, and Elena Zucca. Mixin modules and computational effects. In 2003 International Colloquium on Languages, Automata and Programming, Eindhoven, The Netherlands, 2003.

Google Scholar

[3]

Davide Ancona and Elena Zucca. A primitive calculus for module systems. In International Conference on Principles and Practice of Declarative Programming, volume 1702 of Lecture Notes in Computer Science, pages 62--79. Springer-Verlag, 1999.

Digital Library

Google Scholar

[4]

Gerard Boudol. The recursive record semantics of objects revisited. Research report 4199, INRIA, 2001. To appear in the Journal of Functional Programming.

Digital Library

Google Scholar

[5]

Karl Crary, Robert Harper, and Sidd Puri. What is a recursive module? In 1999 Conference on Programming Language Design and Implementation (PLDI), pages 50--63, Atlanta, GA.

Digital Library

Google Scholar

[6]

Derek Dreyer, Karl Crary, and Robert Harper. A type system for higher-order modules. In 2003 ACM Symposium on Principles of Programming Languages, pages 236--249, 2003.

Digital Library

Google Scholar

[7]

Derek Dreyer, Robert Harper, and Karl Crary. A type system for well-founded recursion. Technical Report CMU-CS-03-163, Carnegie Mellon University, July 2003.

Google Scholar

[8]

Derek R. Dreyer, Robert Harper, and Karl Crary. Toward a practical type theory for recursive modules. Technical Report CMU-CS-01-112, School of Computer Science, Carnegie Mellon University, March 2001.

Google Scholar

[9]

Dominic Duggan and Constantinos Sourelis. Mixin modules. In 1996 ACM SIGPLAN International Conference on Functional Programming, pages 262--273, Philadelphia, Pennsylvania, June 1996.

Digital Library

Google Scholar

[10]

Dominic Duggan and Constantinos Sourelis. Parameterized modules, recursive modules, and mixin modules. In 1998 ACM SIGPLAN Workshop on ML, pages 87--96, Baltimore, Maryland, September 1998.

Digital Library

Google Scholar

[11]

Levent Erkök and John Launchbury. Recursive monadic bindings. In 2000 International Conference on Functional Programming, pages 174--185, Paris, France, 2000.

Digital Library

Google Scholar

[12]

Levent Erkök and John Launchbury. A recursive do for Haskell. In 2002 Haskell Workshop, October 2002.

Digital Library

Google Scholar

[13]

Matthew Flatt and Matthias Felleisen. Units: Cool modules for HOT languages. In 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 236--248, Montreal, Canada, June 1998.

Digital Library

Google Scholar

[14]

Daniel P. Friedman and Amr Sabry. Recursion is a computational effect. Technical Report TR546, Indiana University, December 2000.

Google Scholar

[15]

John Greiner. Weak polymorphism can be sound. Journal of Functional Programming, 6(1):111--141, 1996.

Crossref

Google Scholar

[16]

Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In Twenty-First ACM Symposium on Principles of Programming Languages, pages 123--137, Portland, OR, January 1994.

Digital Library

Google Scholar

[17]

Tom Hirschowitz and Xavier Leroy. Mixin modules in a call-by-value setting. In 2002 European Symposium on Programming, volume 2305 of Lecture Notes in Computer Science, pages 6--20, 2002.

Digital Library

Google Scholar

[18]

Tom Hirschowitz, Xavier Leroy, and J. B. Wells. Compilation of extended recursion in call-by-value functional languages. In 2003 International Conference on Principles and Practice of Declarative Programming, Uppsala, Sweden.

Digital Library

Google Scholar

[19]

Richard Kelsey, William Clinger, and Jonathan Rees (eds.). Revised5 report on the algorithmic language Scheme. Higher-Order and Symbolic Computation, 11(1), September 1998.

Digital Library

Google Scholar

[20]

Xavier Leroy. A proposal for recursive modules in Objective Caml, May 2003. Available from the author's web site.

Google Scholar

[21]

Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

Digital Library

Google Scholar

[22]

Eugenio Moggi and Amr Sabry. An abstract monadic semantics for value recursion. In 2003 Workshop on Fixed Points in Computer Science, April 2003.

Google Scholar

[23]

Aleksandar Nanevski. Meta-programming with names and necessity. In 2002 International Conference on Functional Programming, pages 206--217, Pittsburgh, PA, 2002. A significant revision is available as a technical report CMU-CS-02-123R, Carnegie Mellon University.

Digital Library

Google Scholar

[24]

Aleksandar Nanevski. A modal calculus for effect handling. Technical Report CMU-CS-03-149, Carnegie Mellon University, June 2003.

Google Scholar

[25]

Objective Caml. http://www.ocaml.org+.

Google Scholar

[26]

Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998.

Crossref

Google Scholar

[27]

Andrew M. Pitts and Murdoch J. Gabbay. A metalanguage for programming with bound names modulo renaming. In Roland Backhouse and José Nuno Oliveira, editors, Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, pages 230--255. Springer, 2000.

Digital Library

Google Scholar

[28]

Claudio V. Russo. Recursive structures for Standard ML. In International Conference on Functional Programming, pages 50--61, Florence, Italy, September 2001.

Digital Library

Google Scholar

[29]

Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Information and Computation, 111(2):245--296, 1994.

Digital Library

Google Scholar

[30]

Mads Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, University of Edinburgh, 1988.

Google Scholar

[31]

Andrew K. Wright. Simple imperative polymorphism. Lisp and Symbolic Computation, 8(4):343--355, 1995.

Digital Library

Google Scholar

Cited By

View all

Chugh R(2015)IsoLATEProceedings of the 24th European Symposium on Programming on Programming Languages and Systems - Volume 903210.1007/978-3-662-46669-8_11(257-282)Online publication date: 11-Apr-2015
https://dl.acm.org/doi/10.1007/978-3-662-46669-8_11
Rossberg ADreyer D(2013)Mixin’ Up the ML Module SystemACM Transactions on Programming Languages and Systems10.1145/2450136.245013735:1(1-84)Online publication date: 1-Apr-2013
https://dl.acm.org/doi/10.1145/2450136.2450137
Liu YSkalka CSmith S(2011)Type-specialized staged programming with process separationHigher-Order and Symbolic Computation10.1007/s10990-012-9089-024:4(341-385)Online publication date: 1-Nov-2011
https://dl.acm.org/doi/10.1007/s10990-012-9089-0
Show More Cited By

Index Terms

A type system for well-founded recursion
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
    2. General programming languages
      1. Language features
        Modules / packages
        Recursion
2. Theory of computation
  1. Formal languages and automata theory
  2. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

A type system for well-founded recursion
POPL '04

In the interest of designing a recursive module extension to ML that is as simple and general as possible, we propose a novel type system for general recursion over effectful expressions. The presence of effects seems to necessitate a backpatching ...
Recursive type generativity
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

Existential types provide a simple and elegant foundation for understanding generative abstract data types, of the kind supported by the Standard ML module system. However, in attempting to extend ML with support for recursive modules, we have found ...
Recursive type generativity
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

Existential types provide a simple and elegant foundation for understanding generative abstract data types, of the kind supported by the Standard ML module system. However, in attempting to extend ML with support for recursive modules, we have found ...

Reviews

Reviewer: David R Naugler

ML's module system-consisting of structures, signatures, and functors-is strictly hierarchical, forcing mutually recursive types and functions to be defined in the same module. The author uses a type-theoretical approach to design a type system for general recursion over effectful expressions. The proposed type system is designed to be as simple and as general as possible, and to be the basis for a future recursive module extension to ML. The work is limited to the dynamic components of recursive modules, and statically insures that recursion for these is well founded, namely, that the body of a recursive expression will evaluate without trying to access the undefined recursive variable. The type system is presented in the context of the (pure) simply typed &lgr;-calculus. Dreyer indicates how the results in this paper relate to other work in the field, and indicates directions for future work. This is a well-written technical and theoretical paper, in an active research area. It illustrates nicely how type theory can inform design and implementation in programming languages. The paper is appropriate for those with a solid background in both a functional language of the ML family and in type theory.

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2004

364 pages

ISBN:158113729X

DOI:10.1145/964001

General Chair:
Neil D. Jones
DIKU, University of Copenhagen
,
Program Chair:
Xavier Leroy
INRIA Rocquencourt

ACM SIGPLAN Notices Volume 39, Issue 1
POPL '04
January 2004
352 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/982962
Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL04

Sponsor:

POPL04: The 31st Annual ACM Symposium on Principles of Programming Languages

January 14 - 16, 2004

Venice, Italy

Acceptance Rates

POPL '04 Paper Acceptance Rate 29 of 176 submissions, 16%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
560
Total Downloads

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

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Chugh R(2015)IsoLATEProceedings of the 24th European Symposium on Programming on Programming Languages and Systems - Volume 903210.1007/978-3-662-46669-8_11(257-282)Online publication date: 11-Apr-2015
https://dl.acm.org/doi/10.1007/978-3-662-46669-8_11
Rossberg ADreyer D(2013)Mixin’ Up the ML Module SystemACM Transactions on Programming Languages and Systems10.1145/2450136.245013735:1(1-84)Online publication date: 1-Apr-2013
https://dl.acm.org/doi/10.1145/2450136.2450137
Liu YSkalka CSmith S(2011)Type-specialized staged programming with process separationHigher-Order and Symbolic Computation10.1007/s10990-012-9089-024:4(341-385)Online publication date: 1-Nov-2011
https://dl.acm.org/doi/10.1007/s10990-012-9089-0
Nordlander JCarlsson MGill ASumii E(2008)Unrestricted pure call-by-value recursionProceedings of the 2008 ACM SIGPLAN workshop on ML10.1145/1411304.1411309(23-34)Online publication date: 21-Sep-2008
https://dl.acm.org/doi/10.1145/1411304.1411309
Dreyer DRossberg AHook JThiemann P(2008)Mixin' up the ML module systemProceedings of the 13th ACM SIGPLAN international conference on Functional programming10.1145/1411204.1411248(307-320)Online publication date: 20-Sep-2008
https://dl.acm.org/doi/10.1145/1411204.1411248
Dreyer DRossberg A(2008)Mixin' up the ML module systemACM SIGPLAN Notices10.1145/1411203.141124843:9(307-320)Online publication date: 20-Sep-2008
https://dl.acm.org/doi/10.1145/1411203.1411248
Fahndrich MXia S(2007)Establishing object invariants with delayed typesACM SIGPLAN Notices10.1145/1297105.129705242:10(337-350)Online publication date: 21-Oct-2007
https://dl.acm.org/doi/10.1145/1297105.1297052
Fahndrich MXia SGabriel RBacon DLopes CSteele G(2007)Establishing object invariants with delayed typesProceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applications10.1145/1297027.1297052(337-350)Online publication date: 21-Oct-2007
https://dl.acm.org/doi/10.1145/1297027.1297052
DREYER D(2007)Recursive type generativityJournal of Functional Programming10.1017/S095679680700642917:4-5(433-471)Online publication date: 1-Jul-2007
https://dl.acm.org/doi/10.1017/S0956796807006429
Owens SFlatt M(2006)From structures and functors to modules and unitsACM SIGPLAN Notices10.1145/1160074.115981541:9(87-98)Online publication date: 16-Sep-2006
https://dl.acm.org/doi/10.1145/1160074.1159815
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations