article

A Polymorphic Environment Calculus and its Type-Inference Algorithm

Author:

Shin-Ya NishizakiAuthors Info & Claims

Higher-Order and Symbolic Computation, Volume 13, Issue 3

Pages 239 - 278

https://doi.org/10.1023/A:1010010314528

Published: 01 September 2000 Publication History

Abstract

The polymorphic environment calculus is a polymorphic lambda calculus which enables us to treat environments as first-class citizens. In the calculus, environments are formalized as explicit substitutions, and the substitutions are included in the set of terms of the calculus. First, we introduce an untyped environment calculus, and we present a semantics of the calculus as a translation into the lambda calculus. Second, we propose a polymorphic type system for the environment calculus based on Damas-Milner's ML-polymorphic type system. In ML, polymorphism is allowed only in let-expressions; in the polymorphic environment calculus, polymorphism is provided with environment compositions. We prove a subject-reduction theorem for the type system. Third, a type-inference algorithm is given to the polymorphic environment calculus, and we establish its soundness, termination, and principal-typing theorem.

References

[1]

1. Abadi, M., Cardelli, L., Curien, P.-L., and Lévy, J.-J. Explicit substitutions. Journal of Functional Programming 1(4) (1991) 375-416.]]

[2]

2. Barendregt, H.P. The Lambda Calculus. Elsevier, 1984.]]

[3]

3. Clinger, W. and Rees, J. Revised<sup>4</sup> report on the algorithmic language Scheme. ACM Lisp Pointers 4(3) (1991) 1-55.]]

Digital Library

[4]

4. Curien, P.-L. Categorical combinators. Information and Control 69 (1986) 188-254.]]

Digital Library

[5]

5. Curien, P.-L. An abstract framework for environment machines. Theoretical Computer Science 82 (1991) 389-402.]]

Digital Library

[6]

6. Curien, P.-L., Hardin, T., and Lévy, J.-J. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM 43(2) (1996) 362-397.]]

Digital Library

[7]

7. Dowek, G., Hardin, T., and Kirchner, C. Higher-order unification via explicit substitutions, extended abstract. In Proceedings of the Symposium on Logic in Computer Science, 1995, pp. 366-374.]]

Digital Library

[8]

8. Felleisen, M., Friedman, D.P., Kohlbecker, E., and Duba, B. A syntactic theory of sequential control. Theoretical Computer Science 52(3) (1987) 205-237.]]

Digital Library

[9]

9. Gallesio, E. STk Reference Manual Version 3.99. 1998.]]

[10]

10. Gelernter, D., Jagannathan, S., and London, T. Environments as first-class objects. In Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, 1987, pp. 98-110.]]

Digital Library

[11]

11. Girard, J.-Y. Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur. Thèse d' État, Université de Paris VII, Paris, France, 1972.]]

[12]

12. Girard, J.-Y., Taylor, P., and Lafont, Y. Cambridge Tracts in Computer Science, Vol. 7: Proofs and Types. Cambridge University Press, 1989.]]

Digital Library

[13]

13. Hanson, C. MIT Scheme Reference Manual, 1.62 ed. MIT, 1996.]]

[14]

14. Hardin, T. Confluence results for the pure strong categorical logic ccl, λ-calculi as subsystems of ccl. Theoretical Computer Science 65 (1989) 291-342.]]

Digital Library

[15]

15. Jagannathan, S. Metalevel building blocks for modular systems. ACM Transaction of Programming Languages and Systems 16(3) (1994) 456-492.]]

Digital Library

[16]

16. Jategaonkar, L.A. and Mitchell, J.C. Type inference with extended pattern matching and subtypes. Fundamenta Informaticae 19 (1993) 127-166.]]

Digital Library

[17]

17. Jouvelot, P. and Gifford, D.K. Algebraic reconstruction of types and effects. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, 1991, pp. 303-310.]]

Digital Library

[18]

18. Kelsey, R., Clinger, W., and Rees, J. (Eds.). Revised<sup>5</sup> report on the algorithmic language Scheme. Higher-Order and Symbolic Computation 11(1) (1998) 7-105. Also appears in ACM SIGPLAN Notices 33(9), September 1998.]]

Digital Library

[19]

19. Klop, J.W. Term rewriting systems. In Handbook of Logic in Computer Science, Vol. 2. Clarendon Press, 1992, pp. 1-116.]]

Digital Library

[20]

20. Lampson, B. and Burstall, R. Pebble, a kernel language for modules and abstract data types. Information and Computation 76 (1988) 278-346.]]

Digital Library

[21]

21. Laumann, O. Elk--The Extension Language Kit Scheme Reference. 1995.]]

[22]

22. Miller, J.S. and Rozas, G.J. Free variables and first-class environments. Lisp and Symbolic Computation 4(2) (1991) 107-141.]]

Digital Library

[23]

23. Nishizaki, S. ML with first-class environments and its type inference algorithm. In Lecture Notes in Computer Science, Vol. 792: Logic, Language and Computation. Springer, 1994, pp. 95-116.]]

[24]

24. Nishizaki, S. Simply typed lambda calculus with first-class environments. Publication of Research Institute for Mathematical Sciences Kyoto University 30(6) (1995) 1055-1121.]]

[25]

25. Nishizaki, S. Type inference for simply-typed environment calculus with shadowing. In Proceedings of the Fuji International Workshop on Functional and Logic Programming, 1995.]]

[26]

26. Nishizaki, S. and Akama, Y. Translations of first-class environments to records. In 1st International Workshop on Explicit Substitutions, 1998.]]

[27]

27. Ohori, A. A compilation method for ML-style polymorphic record calculi. In Conference Record of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, 1992, pp. 154-165.]]

Digital Library

[28]

28. Queinnec, C. and De Roure, D. Sharing code through first-class environments. In Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, 1996, pp. 251-261.]]

Digital Library

[29]

29. Rémy, D. Typechecking records and variants in a natural extention of ML. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989, pp. 60-67.]]

Digital Library

[30]

30. Sato, M., Sakurai, T., and Burstall, R. Explicit environments. In Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications, Jean-Yves Girard (Ed.). Springer-Verlag, L'Aquila, Italy, 1999. Lecture Notes in Computer Science 1581.]]

Digital Library

[31]

31. Seaman, J. and Iyer, S.P. An operational semantics of sharing in lazy evaluation. Science of Computer Programming 27(3) (1996) 286-322.]]

Digital Library

[32]

32. Talcott, C. Reasoning about functions with effects. In Higher-Order Operational Techniques in Semantics, A.D. Gordon and A.M. Pitts, (Eds). Cambridge University Press, 1996, pp. 347-390.]]

[33]

33. Talpin, J.-P. and Jouvelot, P. Polymorphic type, region and effect inference. Journal of Functional Programming 2(3) (1992) 245-271.]]

[34]

34. Tofte, M. Type inference for polymorphic references. Information and Computation 89(1) (1990) 1-34.]]

Digital Library

[35]

35. Wand, M. Type inference for record concatenation and multiple inheritance. Information and Computation 93 (1991) 1-15.]]

Digital Library

Cited By

Nishizaki S(2023)Transplanting of Environments between Closures in the lambda calculusProceedings of the 2023 12th International Conference on Software and Computer Applications10.1145/3587828.3587847(122-130)Online publication date: 23-Feb-2023
https://dl.acm.org/doi/10.1145/3587828.3587847
Kasuga RNishizaki S(2022)Formalizing dynamic-wind in the lambda calculusProceedings of the 2022 11th International Conference on Software and Computer Applications10.1145/3524304.3524318(90-96)Online publication date: 24-Feb-2022
https://dl.acm.org/doi/10.1145/3524304.3524318
Nishizaki STakayanagi Y(2022)Extracting Environments from Function ClosuresProceedings of the 2022 11th International Conference on Software and Computer Applications10.1145/3524304.3524313(61-68)Online publication date: 24-Feb-2022
https://dl.acm.org/doi/10.1145/3524304.3524313
Show More Cited By

Index Terms

A Polymorphic Environment Calculus and its Type-Inference Algorithm
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
      1. Lambda calculus
  2. Mathematical analysis
    1. Calculus
      1. Lambda calculus
2. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types

Recommendations

Nested proof search as reduction in the Lambda-calculus
PPDP '11: Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming

We present a system for propositional implicative intuitionistic logic in the calculus of structures, which is a generalisation of the sequent calculus to the deep inference methodology. We show that it is sound and complete with respect to the usual ...
Proof-term synthesis on dependent-type systems via explicit substitutions

Typed λ-terms are used as a compact and linear representation of proofs in intuitionistic logic. This is possible since the Curry-Howard isomorphism relates proof-trees with typed λ-terms. The proofs-as-terms principle can be used to verify the validity ...
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94

This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Higher-Order and Symbolic Computation

Higher-Order and Symbolic Computation Volume 13, Issue 3

Sept. 2000

119 pages

ISSN:1388-3690

Editors:
Olivier Danvy
Univ. of Aarhus, Aarhus C, Denmark
,
Carolyn Talcott
Stanford Univ., Stanford, CA

Issue’s Table of Contents

Copyright © Copyright © 2000 Kluwer Academic Publishers.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 September 2000

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 17 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nishizaki S(2023)Transplanting of Environments between Closures in the lambda calculusProceedings of the 2023 12th International Conference on Software and Computer Applications10.1145/3587828.3587847(122-130)Online publication date: 23-Feb-2023
https://dl.acm.org/doi/10.1145/3587828.3587847
Kasuga RNishizaki S(2022)Formalizing dynamic-wind in the lambda calculusProceedings of the 2022 11th International Conference on Software and Computer Applications10.1145/3524304.3524318(90-96)Online publication date: 24-Feb-2022
https://dl.acm.org/doi/10.1145/3524304.3524318
Nishizaki STakayanagi Y(2022)Extracting Environments from Function ClosuresProceedings of the 2022 11th International Conference on Software and Computer Applications10.1145/3524304.3524313(61-68)Online publication date: 24-Feb-2022
https://dl.acm.org/doi/10.1145/3524304.3524313
Nishizaki SKasuga R(2021)Untyped lambda calculus with functionally referable environmentsProceedings of the 2021 10th International Conference on Software and Computer Applications10.1145/3457784.3457798(100-104)Online publication date: 23-Feb-2021
https://dl.acm.org/doi/10.1145/3457784.3457798
Nishizaki S(2019)ML Polymorphism of Linear Lambda Calculus with First-class ContinuationsProceedings of the 2019 8th International Conference on Software and Computer Applications10.1145/3316615.3316668(189-193)Online publication date: 19-Feb-2019
https://dl.acm.org/doi/10.1145/3316615.3316668
Nishizaki SMezhuyev VBenedicenti L(2017)Linear lambda calculus with non-linear first-class continuationsProceedings of the 6th International Conference on Software and Computer Applications10.1145/3056662.3056693(28-32)Online publication date: 26-Feb-2017
https://dl.acm.org/doi/10.1145/3056662.3056693
Cave APientka BMomigliano APientka BPollack R(2013)First-class substitutions in contextual type theoryProceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice10.1145/2503887.2503889(15-24)Online publication date: 23-Sep-2013
https://dl.acm.org/doi/10.1145/2503887.2503889
Nishizaki SFujii M(2012)Strong reduction for typed lambda calculus with first-class environmentsProceedings of the Third international conference on Information Computing and Applications10.1007/978-3-642-34062-8_82(632-639)Online publication date: 14-Sep-2012
https://dl.acm.org/doi/10.1007/978-3-642-34062-8_82
Pientka B(2008)A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutionsACM SIGPLAN Notices10.1145/1328897.132848343:1(371-382)Online publication date: 7-Jan-2008
https://dl.acm.org/doi/10.1145/1328897.1328483
Pientka BNecula GWadler P(2008)A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutionsProceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1328438.1328483(371-382)Online publication date: 7-Jan-2008
https://dl.acm.org/doi/10.1145/1328438.1328483

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents