Article

Tridirectional typechecking

Authors:

Frank PfenningAuthors Info & Claims

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

Pages 281 - 292

https://doi.org/10.1145/964001.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

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

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

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 Conferences

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

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]

Sponsors

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

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

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
Felicissimo T(2024)Generic bidirectional typing for dependent type theoriesProgramming Languages and Systems10.1007/978-3-031-57262-3_6(143-170)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_6
Lakhani ZDas ADeYoung HMordido APfenning F(2022)Polarized SubtypingProgramming Languages and Systems10.1007/978-3-030-99336-8_16(431-461)Online publication date: 29-Mar-2022
https://doi.org/10.1007/978-3-030-99336-8_16
Dunfield JKrishnaswami N(2021)Bidirectional TypingACM Computing Surveys10.1145/345095254:5(1-38)Online publication date: 25-May-2021
https://dl.acm.org/doi/10.1145/3450952
Pavlinovic ZSu YWies T(2021)Data flow refinement type inferenceProceedings of the ACM on Programming Languages10.1145/34343005:POPL(1-31)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434300
ALLAIS GATKEY RCHAPMAN JMCBRIDE CMCKINNA J(2021)A type- and scope-safe universe of syntaxes with binding: their semantics and proofsJournal of Functional Programming10.1017/S095679682000007631Online publication date: 19-Oct-2021
https://doi.org/10.1017/S0956796820000076
Moon BEades III HOrchard D(2021)Graded Modal Dependent Type TheoryProgramming Languages and Systems10.1007/978-3-030-72019-3_17(462-490)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_17
Orchard DLiepelt VEades III H(2019)Quantitative program reasoning with graded modal typesProceedings of the ACM on Programming Languages10.1145/33417143:ICFP(1-30)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341714
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 Table of Contents