skip to main content
10.1145/2676726.2676992acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Principal Type Schemes for Gradual Programs

Published: 14 January 2015 Publication History

Abstract

Gradual typing is a discipline for integrating dynamic checking into a static type system. Since its introduction in functional languages, it has been adapted to a variety of type systems, including object-oriented, security, and substructural. This work studies its application to implicitly typed languages based on type inference. Siek and Vachharajani designed a gradual type inference system and algorithm that infers gradual types but still rejects ill-typed static programs. However, the type system requires local reasoning about type substitutions, an imperative inference algorithm, and a subtle correctness statement.
This paper introduces a new approach to gradual type inference, driven by the principle that gradual inference should only produce static types. We present a static implicitly typed language, its gradual counterpart, and a type inference procedure. The gradual system types the same programs as Siek and Vachharajani, but has a modular structure amenable to extension. The language admits let-polymorphism, and its dynamics are defined by translation to the Polymorphic Blame Calculus.
The principal types produced by our initial type system mask the distinction between static parametric polymorphism and polymorphism that can be attributed to gradual typing. To expose this difference, we distinguish static type parameters from gradual type parameters and reinterpret gradual type consistency accordingly. The resulting extension enables programs to be interpreted using either the polymorphic or monomorphic Blame Calculi.

Supplementary Material

MPG File (p303-sidebyside.mpg)

References

[1]
A. Ahmed, R. B. Findler, J. Matthews, and P. Wadler. Blame for all. In Proc. 1st Workshop on Script to Program Evolution, STOP '09, pages 1--13, New York, NY, USA, 2009. ACM. 10.1145/1570506.1570507.
[2]
A. Ahmed, R. B. Findler, J. G. Siek, and P. Wadler. Blame for all. In Proc. Symposium on Principles of Programming Languages, POPL '11, pages 201--214, New York, NY, USA, 2011. ACM. 10.1145/1926385.1926409.
[3]
G. Bierman, E. Meijer, and M. Torgersen. Adding dynamic types to C$^\#$. In T. D'Hondt, editor, Proc. 24th European Conference on Object-oriented Programming (ECOOP 2010), number 6183 in Lecture Notes in Computer Science, pages 76--100, Maribor, Slovenia, June 2010. Springer-Verlag.
[4]
R. Cartwright and M. Fagan. Soft typing. In Proc. Conference on Programming Language Design and Implementation, PLDI '91, pages 278--292, New York, NY, USA, 1991. ACM.
[5]
D. Crystal. A dictionary of linguistics and phonetics. Blackwell, 2008.
[6]
S. K. Debray and D. S. Warren. Automatic mode inference for logic programs. Journal of Logic Programming, 5 (3): 207--229, Sept. 1988.
[7]
J.-Y. Girard. Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris VII, 1972.
[8]
J. Gronski, K. Knowles, A. Tomb, S. N. Freund, and C. Flanagan. Sage: Hybrid checking for flexible specifications. In Proc. Scheme and Functional Programming Workshop, pages 93--104, 2006.
[9]
J. Matthews and A. Ahmed. Parametric polymorphism through run-time sealing or, theorems for low, low prices! In Proc. European Conference on Programming Languages and Systems, ESOP'08/ETAPS'08, pages 16--31, Berlin, Heidelberg, 2008. Springer-Verlag.
[10]
J. Matthews and R. B. Findler. Operational semantics for multi-language programs. ACM Transactions on Programming Languages and Systems, 31 (3): 12:1--12:44, Apr. 2009.
[11]
R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17: 348--375, Aug. 1978.
[12]
A. Ohori. A simple semantics for ml polymorphism. In Proc. International Conference on Functional Programming Languages and Computer Architecture, FPCA '89, pages 281--292, New York, NY, USA, 1989. ACM. 10.1145/99370.99393.
[13]
S. Peyton Jones, D. Vytiniotis, S. Weirich, and M. Shields. Practical type inference for arbitrary-rank types. Journal of Functional Programming, 17 (1): 1--82, Jan. 2007. 10.1017/S0956796806006034.
[14]
B. C. Pierce. Types and programming languages. MIT Press, Cambridge, MA, USA, 2002.
[15]
A. Rastogi, A. Chaudhuri, and B. Hosmer. The ins and outs of gradual type inference. In Proc. Symposium on Principles of Programming Languages, pages 481--494, New York, NY, USA, 2012. ACM. 10.1145/2103656.2103714.
[16]
J. C. Reynolds. Towards a theory of type structure. In Programming Symposium, Proceedings Colloque Sur La Programmation, pages 408--423, London, UK, UK, 1974. Springer-Verlag.
[17]
J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12 (1): 23--41, Jan. 1965. ISSN 0004--5411. 10.1145/321250.321253.
[18]
I. Sergey and D. Clarke. Gradual ownership types. In H. Seidl, editor, Proc. European Symposium on Programming Languages and Systems, volume 7211 of ESOP '12, pages 579--599, Tallinn, Estonia, 2012. Springer-Verlag.
[19]
J. Siek and W. Taha. Gradual typing for objects. In E. Ernst, editor, Proc. European Conference on Object-oriented Programming, number 4609 in ECOOP '07, pages 2--27, Berlin, Germany, July 2007. Springer-Verlag.
[20]
J. Siek, R. Garcia, and W. Taha. Exploring the design space of higher-order casts. In Proc. European Symposium on Programming Languages, ESOP '09, pages 17--31, Berlin, 2009. Springer-Verlag.
[21]
J. G. Siek and W. Taha. Gradual typing for functional languages. In Proc. Scheme and Functional Programming Workshop, pages 81--92, Sept. 2006.
[22]
J. G. Siek and M. Vachharajani. Gradual typing with unification-based inference. In Proc. 2008 Symposium on Dynamic Languages, DLS '08, pages 7:1--7:12, New York, NY, USA, 2008. ACM. 10.1145/1408681.1408688.
[23]
N. Swamy, C. Fournet, A. Rastogi, K. Bhargavan, J. Chen, P.-Y. Strub, and G. Bierman. Gradual typing embedded securely in JavaScript. In Proc. 41st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2014), pages 425--437, San Diego, CA, USA, Jan. 2014. ACM Press.
[24]
S. Tobin-Hochstadt and M. Felleisen. Interlanguage migration: From scripts to programs. In Companion to the 21st ACM SIGPLAN Symposium on Object-oriented Programming Systems, Languages, and Applications, OOPSLA '06, pages 964--974, New York, NY, USA, 2006. ACM. ISBN 1--59593--491-X.
[25]
S. Tobin-Hochstadt and M. Felleisen. The design and implementation of Typed Scheme. In Proc. 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008), pages 395--406, San Francisco, CA, USA, Jan. 2008. ACM Press.
[26]
P. Wadler and R. B. Findler. Well-typed programs can't be blamed. In Proc. European Symposium on Programming Languages, ESOP '09, pages 1--16, Berlin, 2009. Springer-Verlag.
[27]
M. Wand. A simple algorithm and proof for type inference. Fundamenta Infomaticae, 10: 115--122, 1987\natexlaba.
[28]
M. Wand. Complete type inference for simple objects. In Proc. 2nd IEEE Symposium on Logic in Computer Science, pages 37--44, 1987\natexlabb.
[29]
R. Wolff, R. Garcia, É. Tanter, and J. Aldrich. Gradual typestate. In M. Mezini, editor, Proc. European Conference on Object-oriented Programming, volume 6813 of Lecture Notes in Computer Science, pages 459--483, Lancaster, UK, July 2011. Springer-Verlag.
[30]
A. K. Wright. Simple imperative polymorphism. Lisp Symb. Comput., 8 (4): 343--355, Dec. 1995. ISSN 0892--4635. 10.1007/BF01018828.
[31]
A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Journal of Information and Computation, 115 (1): 38--94, Nov. 1994.
[32]
T. Wrigstad, F. Zappa Nardelli, S. Lebresne, J. Östlund, and J. Vitek. Integrating typed and untyped code in a scripting language. In Proc. 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2010), pages 377--388, Madrid, Spain, Jan. 2010. ACM Press.

Cited By

View all
  • (2024)QuAC: Quick Attribute-Centric Type Inference for PythonProceedings of the ACM on Programming Languages10.1145/36897838:OOPSLA2(2040-2069)Online publication date: 8-Oct-2024
  • (2024)Type-Based Gradual Typing Performance OptimizationProceedings of the ACM on Programming Languages10.1145/36329318:POPL(2667-2699)Online publication date: 5-Jan-2024
  • (2024)Total Type Error Localization and Recovery with HolesProceedings of the ACM on Programming Languages10.1145/36329108:POPL(2041-2068)Online publication date: 5-Jan-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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
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 the author(s) 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].

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. gradual typing
  2. type inference

Qualifiers

  • Research-article

Funding Sources

Conference

POPL '15
Sponsor:

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

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

Other Metrics

Citations

Cited By

View all
  • (2024)QuAC: Quick Attribute-Centric Type Inference for PythonProceedings of the ACM on Programming Languages10.1145/36897838:OOPSLA2(2040-2069)Online publication date: 8-Oct-2024
  • (2024)Type-Based Gradual Typing Performance OptimizationProceedings of the ACM on Programming Languages10.1145/36329318:POPL(2667-2699)Online publication date: 5-Jan-2024
  • (2024)Total Type Error Localization and Recovery with HolesProceedings of the ACM on Programming Languages10.1145/36329108:POPL(2041-2068)Online publication date: 5-Jan-2024
  • (2024)Type-directed operational semantics for gradual typingJournal of Functional Programming10.1017/S095679682400007834Online publication date: 26-Sep-2024
  • (2024)Static Blame for gradual typingJournal of Functional Programming10.1017/S095679682400002934Online publication date: 25-Mar-2024
  • (2023)Gradual Typing for Effect HandlersProceedings of the ACM on Programming Languages10.1145/36228607:OOPSLA2(1758-1786)Online publication date: 16-Oct-2023
  • (2023)How Profilers Can Help Navigate Type MigrationProceedings of the ACM on Programming Languages10.1145/36228177:OOPSLA2(544-573)Online publication date: 16-Oct-2023
  • (2023)How to Evaluate Blame for Gradual Types, Part 2Proceedings of the ACM on Programming Languages10.1145/36078367:ICFP(159-186)Online publication date: 31-Aug-2023
  • (2022)A Typed Lambda Calculus with Gradual Intersection TypesProceedings of the 24th International Symposium on Principles and Practice of Declarative Programming10.1145/3551357.3551382(1-13)Online publication date: 20-Sep-2022
  • (2022)Tierkreis: a Dataflow Framework for Hybrid Quantum-Classical Computing2022 IEEE/ACM Third International Workshop on Quantum Computing Software (QCS)10.1109/QCS56647.2022.00007(12-21)Online publication date: Nov-2022
  • 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