skip to main content
research-article

Self-Representation in Girard's System U

Published: 14 January 2015 Publication History

Abstract

In 1991, Pfenning and Lee studied whether System F could support a typed self-interpreter. They concluded that typed self-representation for System F "seems to be impossible", but were able to represent System F in Fω. Further, they found that the representation of Fω requires kind polymorphism, which is outside Fω. In 2009, Rendel, Ostermann and Hofer conjectured that the representation of kind-polymorphic terms would require another, higher form of polymorphism. Is this a case of infinite regress? We show that it is not and present a typed self-representation for Girard's System U, the first for a λ-calculus with decidable type checking. System U extends System Fω with kind polymorphic terms and types. We show that kind polymorphic types (i.e. types that depend on kinds) are sufficient to "tie the knot" -- they enable representations of kind polymorphic terms without introducing another form of polymorphism. Our self-representation supports operations that iterate over a term, each of which can be applied to a representation of itself. We present three typed self-applicable operations: a self-interpreter that recovers a term from its representation, a predicate that tests the intensional structure of a term, and a typed continuation-passing-style (CPS) transformation -- the first typed self-applicable CPS transformation. Our techniques could have applications from verifiably type-preserving metaprograms, to growable typed languages, to more efficient self-interpreters.

Supplementary Material

MPG File (p471-sidebyside.mpg)

References

[1]
The webpage accompanying this paper is available at http://compilers.cs.ucla.edu/popl15/. The full paper with the appendix is available there, as are the source code for our implementation of System U and our operations.
[2]
Harold Abelson, Gerald Jay Sussman, and Julie Sussman. Structure and Interpretation of Computer Programs. MIT Press, 1985.
[3]
Emil Axelsson. A generic abstract syntax model for embedded languages. SIGPLAN Not., 47(9):323--334, September 2012.
[4]
Henk Barendregt. Self-interpretations in lambda calculus. J. Funct. Program, 1(2):229--233, 1991.
[5]
HP Barendregt. Handbook of Logic in Computer Science (vol. 2): Background: Computational Structures: Abramski, S. (ed), chapter Lambda Calculi with Types. Oxford University Press, Inc., New York, NY, 1993.
[6]
Gilles Barthe. Type-checking injective pure type systems. J. Funct. Program., 9(6):675--698, November 1999.
[7]
Michel Bel. A recursion theoretic self interpreter for the lambda- calculus. http://www.belxs.com/michel/#selfint.
[8]
Alessandro Berarducci and Corrado Böhm. A self-interpreter of lambda calculus having a normal form. In CSL, pages 85--99, 1992.
[9]
Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming, 19(5):509--543, 2009.
[10]
Chiyan Chen and Hongwei Xi. Meta-Programming through Typeful Code Representation. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pages 275--286, Uppsala, Sweden, August 2003.
[11]
Chiyan Chen and Hongwei Xi. Meta-Programming through Typeful Code Representation. Journal of Functional Programming, 15(6):797--835, 2005.
[12]
Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP '08, pages 143--156, New York, NY, USA, 2008. ACM.
[13]
Brendan Eich. Narcissus. http://mxr.mozilla.org/mozilla/ source/js/narcissus/jsexec.js, 2010.
[14]
Herman Geuvers and Mark-Jan Nederhof. Modular proof of strong normalization for the calculus of constructions. J. Funct. Program., 1(2):155--189, 1991.
[15]
Jan Herman Geuvers. Logics and type systems. 1993.
[16]
Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris VII, 1972.
[17]
Barry Jay and Jens Palsberg. Typed self-interpretation by pattern matching. In Proceedings of ICFP'11, ACM SIGPLAN International Conference on Functional Programming, pages 247--258, Tokyo, September 2011.
[18]
Stephen C. Kleene. definability and recursiveness. Duke Math. J., pages 340--353, 1936.
[19]
Oleg Mazonka and Daniel B. Cristofani. A very short self-interpreter. http://arxiv.org/html/cs/0311032v1, November 2003.
[20]
Conor McBride. Outrageous but meaningful coincidences: Dependent type-safe syntax and evaluation. In Proceedings of the 6th ACM SIGPLAN Workshop on Generic Programming, WGP '10, pages 1--12, New York, NY, USA, 2010. ACM.
[21]
John McCarthy. Recursive functions of symbolic expressions and their computation by machine, part i. Commun. ACM, 3(4):184--195, April 1960.
[22]
Torben Æ. Mogensen. Efficient self-interpretations in lambda calculus. Journal of Functional Programming, 2(3):345--363, 1992. See also DIKU Report D-128, Sep 2, 1994.
[23]
Torben Æ. Mogensen. Linear-time self-interpretation of the pure lambda calculus. Higher-Order and Symbolic Computation, 13(3):217--237, 2000.
[24]
Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. ACM Trans. Program. Lang. Syst., 21(3):527--568, May 1999.
[25]
Matthew Naylor. Evaluating Haskell in Haskell. The Monad.Reader, 10:25--33, 2008.
[26]
Frank Pfenning and Peter Lee. Metacircularity in the polymorphic-calculus. Theoretical Computer Science, 89(1):137--159, 1991.
[27]
Tillmann Rendel, Klaus Ostermann, and Christian Hofer. Typed self-representation. In Proceedings of PLDI'09, ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 293--303, June 2009.
[28]
John C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of 25th ACM National Conference, pages 717--740. ACM Press, 1972. The paper later appeared in Higher-Order and Symbolic Computation, 11, 363--397 (1998).
[29]
Andreas Rossberg. HaMLet. http://www.mpi-sws.org/ rossberg/hamlet, 2010.
[30]
Bratin Saha, Valery Trifonov, and Zhong Shao. Intensional analysis of quantified types. ACM Trans. Program. Lang. Syst., 25(2):159--209, 2003.
[31]
Fangmin Song, Yongsen Xu, and Yuechen Qian. The self-reduction in lambda calculus. Theoretical Computer Science, 235(1):171--181, March 2000.
[32]
John Tromp. Binary lambda calculus and combinatory logic. In Kolmogorov Complexity and Applications, 2006. A Revised Version is available at http://homepages.cwi.nl/ tromp/cl/LC.pdf.
[33]
Philip Wadler. The expression problem. http://www.daimi.au.dk/madst/tool/papers/expression.txt.
[34]
Alessandro Warth and Ian Piumarta. Ometa: An object-oriented language for pattern matching. In Proceedings of the 2007 Symposium on Dynamic Languages, DLS '07, pages 11--19, New York, NY, USA, 2007. ACM.
[35]
Geoffrey Washburn and Stephanie Weirich. Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP '03, pages 249--262, New York, NY, USA, 2003. ACM.
[36]
Wikipedia. PyPy. http://en.wikipedia.org/wiki/PyPy, 2010.
[37]
Wikipedia. Rubinius. http://en.wikipedia.org/wiki/Rubinius, 2010.
[38]
Tetsuo Yokoyama and Robert Glück. A reversible programming language and its invertible self-interpreter. In Proceedings of PEPM'07, ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2007.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 50, Issue 1
POPL '15
January 2015
682 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2775051
  • Editor:
  • Andy Gill
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
    January 2015
    716 pages
    ISBN:9781450333009
    DOI:10.1145/2676726
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: 14 January 2015
Published in SIGPLAN Volume 50, Issue 1

Check for updates

Author Tags

  1. lambda calculus
  2. languages
  3. self representation
  4. theory
  5. types

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)17
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2018)Incorporating quotation and evaluation into Church's type theoryInformation and Computation10.1016/j.ic.2018.03.001260:C(9-50)Online publication date: 1-Jun-2018
  • (2016)Type theory in type theory using quotient inductive typesACM SIGPLAN Notices10.1145/2914770.283763851:1(18-29)Online publication date: 11-Jan-2016
  • (2016)Type theory in type theory using quotient inductive typesProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2837614.2837638(18-29)Online publication date: 11-Jan-2016
  • (2016)Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesundefinedOnline publication date: 11-Jan-2016
  • (2025)Typed Program Analysis without EncodingsProceedings of the 2025 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation10.1145/3704253.3706138(54-65)Online publication date: 10-Jan-2025
  • (2023)Expressive Authorization Policies using Computation PrincipalsProceedings of the 28th ACM Symposium on Access Control Models and Technologies10.1145/3589608.3593834(107-119)Online publication date: 24-May-2023
  • (2018)Self-Quotation in a Typed, Intensional Lambda-CalculusElectronic Notes in Theoretical Computer Science10.1016/j.entcs.2018.03.024336(207-222)Online publication date: Apr-2018
  • (2017)Jones-optimal partial evaluation by specialization-safe normalizationProceedings of the ACM on Programming Languages10.1145/31581022:POPL(1-28)Online publication date: 27-Dec-2017
  • (2017)Typed self-evaluation via intensional type functionsACM SIGPLAN Notices10.1145/3093333.300985352:1(415-428)Online publication date: 1-Jan-2017
  • (2017)Typed self-evaluation via intensional type functionsProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009853(415-428)Online publication date: 1-Jan-2017
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media