article

Tridirectional typechecking

Authors:

Frank PfenningAuthors Info & Claims

ACM SIGPLAN Notices, Volume 39, Issue 1

Pages 281 - 292

https://doi.org/10.1145/982962.964025

Published: 01 January 2004 Publication History

Abstract

In prior work we introduced a pure type assignment system that encompasses a rich set of property types, including intersections, unions, and universally and existentially quantified dependent types. This system was shown sound with respect to a call-by-value operational semantics with effects, yet is inherently undecidable.In this paper we provide a decidable formulation for this system based on bidirectional checking, combining type synthesis and analysis following logical principles. The presence of unions and existential quantification requires the additional ability to visit subterms in evaluation position before the context in which they occur, leading to a tridirectional type system. While soundness with respect to the type assignment system is immediate, completeness requires the novel concept of contextual type annotations, introducing a notion from the study of principal typings into the source program.

References

[1]

Alexander Aiken, Edward~L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In ACM Symp. Principles of Programming Languages, pages 163--173, 1994.]]

Digital Library

[2]

Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de'Liguoro. Intersection and union types: syntax and semantics. Inf. and Comp., 119:202--230, 1995.]]

Digital Library

[3]

R. Cartwright and M. Fagan. Soft typing. In SIGPLAN Conf. Programming Language Design and Impl. (PLDI), volume~26, pages 278--292, 1991.]]

Digital Library

[4]

M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Zeitschrift f. math. Logik und Grundlagen d. Math., 27:45--58, 1981.]]

[5]

Rowan Davies. A practical refinement-type checker for Standard ML. In Algebraic Methodology and Software Tech. (AMAST'97), pages 565--566. Springer LNCS 1349, 1997.]]

Digital Library

[6]

Rowan Davies. Practical refinement-type checking. PhD thesis proposal, Carnegie Mellon University, 1997.]]

Digital Library

[7]

Rowan Davies and Frank Pfenning. Intersection types and computational effects. In Int'l Conf. Functional Programming (ICFP '00), pages 198--208, 2000.]]

Digital Library

[8]

Jana Dunfield. Combining two forms of type refinements. Technical Report CMU-CS-02-182, Carnegie Mellon University, September 2002.]]

[9]

Jana Dunfield and Frank Pfenning. Type assignment for intersections and unions in call-by-value languages. In Found. Software Science and Computational Structures (FOSSACS '03), pages 250--266, Warsaw, Poland, April 2003. Springer LNCS 2620.]]

[10]

Tim Freeman. Refinement types for ML. PhD thesis, Carnegie Mellon University, 1994. CMU-CS-94-110.]]

Digital Library

[11]

Tim Freeman and Frank Pfenning. Refinement types for ML. In SIGPLAN Conf. Programming Language Design and Impl. (PLDI), volume 26, pages 268--277. ACM Press, 1991.]]

Digital Library

[12]

Haruo Hosoya and Benjamin~C. Pierce. How good is local type inference? Technical Report MS-CIS-99-17, University of Pennsylvania, June 1999.]]

[13]

Trevor Jim. What are principal typings and what are they good for? Technical memorandum MIT/LCS/TM-532, MIT, November 1995.]]

Digital Library

[14]

Yitzhak Mandelbaum, David Walker, and Robert Harper. An effective theory of type refinements. Technical Report TR-656-02, Princeton, December 2002.]]

[15]

Jens Palsberg and Christina Pavlopoulou. From polyvariant flow information to intersection and union types. J. Func. Prog., 11(3):263--317, 2001.]]

Digital Library

[16]

Benjamin C. Pierce. Programming with intersection types and bounded polymorphism. PhD thesis, Carnegie Mellon University, 1991. Technical Report CMU-CS-91-205.]]

[17]

Benjamin C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, 1991.]]

[18]

Benjamin C. Pierce and David N. Turner. Local type inference. In ACM Symp. Principles of Programming Languages, pages 252--265, 1998. Full version in ACM Trans. Prog. Lang. Sys., 22(1):1--44, 2000.]]

Digital Library

[19]

John C. Reynolds. Design of the programming language Forsythe. Technical Report CMU-CS-96-146, Carnegie Mellon University, 1996.]]

[20]

Fred Smith, David Walker, and Greg Morrisett. Alias types. In European Symp. on Programming (ESOP'00), pages 366--381, Berlin, Germany, March 2000.]]

Digital Library

[21]

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

Digital Library

[22]

Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Inf. and Comp., 132(2):109--176, 1997.]]

Digital Library

[23]

J. B. Wells and Christian Haack. Branching types. In European Symp. on Programming (ESOP'02), pages 115--132, 2002.]]

Digital Library

[24]

J.B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak. A calculus with polymorphic and polyvariant flow types. J. Func. Prog., 12(3):183--317, May 2002.]]

Digital Library

[25]

Joe Wells. The essence of principal typings. In Int'l Coll. Automata, Languages, and Programming, volume 2380 of LNCS, pages 913--925. Springer, 2002.]]

Digital Library

[26]

Hongwei Xi. Dependent types in practical programming. PhD thesis, Carnegie Mellon University, 1998.]]

Digital Library

[27]

Hongwei Xi. Dependently typed data structures. Revision superseding WAAAPL '99, February 2000.]]

[28]

Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In ACM Symp. Principles of Programming Languages, pages 214--227, 1999.]]

Digital Library

Cited By

Dunfield J(2017)Extensible Datasort RefinementsProgramming Languages and Systems10.1007/978-3-662-54434-1_18(476-503)Online publication date: 19-Mar-2017
https://doi.org/10.1007/978-3-662-54434-1_18
Liquori LStolze C(2017)A Decidable Subtyping Logic for Intersection and Union TypesTopics in Theoretical Computer Science10.1007/978-3-319-68953-1_7(74-90)Online publication date: 9-Dec-2017
https://doi.org/10.1007/978-3-319-68953-1_7
Frankle JOsera PWalker DZdancewic S(2016)Example-directed synthesis: a type-theoretic interpretationACM SIGPLAN Notices10.1145/2914770.283762951:1(802-815)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837629
Show More Cited By

Index Terms

Tridirectional typechecking
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation
  1. Formal languages and automata theory
  2. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

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

In prior work we introduced a pure type assignment system that encompasses a rich set of property types, including intersections, unions, and universally and existentially quantified dependent types. This system was shown sound with respect to a call-by-...
Refined typechecking with Stardust
PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification

We present Stardust, an implementation of a type system for a subset of ML with type refinements, intersection types, and union types, enabling programmers to legibly specify certain classes of program invariants that are verified at compile time. This ...
Gradual typing with union and intersection types

We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

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

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

Copyright © 2004 ACM.

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

Published in SIGPLAN Volume 39, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

62
Total Citations
View Citations
623
Total Downloads

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

Reflects downloads up to 06 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Dunfield J(2017)Extensible Datasort RefinementsProgramming Languages and Systems10.1007/978-3-662-54434-1_18(476-503)Online publication date: 19-Mar-2017
https://doi.org/10.1007/978-3-662-54434-1_18
Liquori LStolze C(2017)A Decidable Subtyping Logic for Intersection and Union TypesTopics in Theoretical Computer Science10.1007/978-3-319-68953-1_7(74-90)Online publication date: 9-Dec-2017
https://doi.org/10.1007/978-3-319-68953-1_7
Frankle JOsera PWalker DZdancewic S(2016)Example-directed synthesis: a type-theoretic interpretationACM SIGPLAN Notices10.1145/2914770.283762951:1(802-815)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837629
Lovas WPfenning F(2010)Refinement Types for Logical Frameworks and Their Interpretation as Proof IrrelevanceLogical Methods in Computer Science10.2168/LMCS-6(4:5)20106:4Online publication date: 5-Dec-2010
https://doi.org/10.2168/LMCS-6(4:5)2010
Dunfield JRossberg A(2009)Greedy bidirectional polymorphismProceedings of the 2009 ACM SIGPLAN workshop on ML10.1145/1596627.1596631(15-26)Online publication date: 30-Aug-2009
https://dl.acm.org/doi/10.1145/1596627.1596631
Zeilberger N(2008)On the unity of dualityAnnals of Pure and Applied Logic10.1016/j.apal.2008.01.001153:1-3(66-96)Online publication date: Apr-2008
https://doi.org/10.1016/j.apal.2008.01.001
Dunfield JStump AXi H(2007)Refined typechecking with StardustProceedings of the 2007 workshop on Programming languages meets program verification10.1145/1292597.1292602(21-32)Online publication date: 2-Oct-2007
https://dl.acm.org/doi/10.1145/1292597.1292602
Xue XOliveira B(2024)Contextual TypingProceedings of the ACM on Programming Languages10.1145/36746558:ICFP(880-908)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674655
DeYoung HMordido APfenning FDas A(2024)Parametric Subtyping for Structural Parametric PolymorphismProceedings of the ACM on Programming Languages10.1145/36329328:POPL(2700-2730)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632932
Parreaux LBoruch-Gruszecki AFan AChau C(2024)When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class PolymorphismProceedings of the ACM on Programming Languages10.1145/36328908:POPL(1418-1450)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632890
Show More Cited By

View Options

Get Access

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents