Article

Stratified type inference for generalized algebraic data types

Authors:

François Pottier,

Yann Régis-GianasAuthors Info & Claims

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 232 - 244

https://doi.org/10.1145/1111037.1111058

Published: 11 January 2006 Publication History

Get Access

Abstract

Stratified type inference for generalized algebraic data types.

References

[1]

James Cheney and Ralf Hinze. A lightweight implementation of generics and dynamics. In Haskell workshop, 2002.

Digital Library

Google Scholar

[2]

James Cheney and Ralf Hinze. First-class phantom types. Technical Report 1901, Cornell University, 2003.

Google Scholar

[3]

Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type erasure semantics. Journal of Functional Programming, 12(6):567--600, November 2002.

Digital Library

Google Scholar

[4]

Fritz Henglein. Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):253--289, April 1993.

Digital Library

Google Scholar

[5]

Ralf Hinze. Fun with phantom types. In Jeremy Gibbons and Oege de~Moor, editors, The Fun of Programming, pages 245--262. Palgrave Macmillan, March 2003.

Google Scholar

[6]

Gérard Huet. Résolution d'équations dans des langages d'ordre 1, 2, .., ω. PhD thesis, Université Paris 7, September 1976.

Google Scholar

[7]

Martin Odersky, Martin Sulzmann, and Martin Wehr. Type inference with constrained types. Theory and Practice of Object Systems, 5(1):35--55, 1999.

Digital Library

Google Scholar

[8]

Martin Odersky, Matthias Zenger, and Christoph Zenger. Colored local type inference. In ACM Symposium on Principles of Programming Languages (POPL), pages 41--53, 2001.

Digital Library

Google Scholar

[9]

Christine Paulin-Mohring. Inductive definitions in the system Coq: rules and properties. Research Report RR1992-49, ENS Lyon, 1992.

Google Scholar

[10]

Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types. Manuscript, July 2005.

Google Scholar

[11]

Simon Peyton Jones, Geoffrey Washburn, and Stephanie Weirich. Wobbly types: type inference for generalised algebraic data types. Manuscript, July 2004.

Google Scholar

[12]

Benjamin C. Pierce and David N. Turner. Local type inference. ACM Transactions on Programming Languages and Systems, 22(1):1--44, January 2000.

Digital Library

Google Scholar

[13]

François Pottier and Nadji Gauthier. Polymorphic typed defunctionalization. In ACM Symposium on Principles of Programming Languages (POPL), pages 89--98, January 2004.

Digital Library

Google Scholar

[14]

François Pottier and Yann Régis-Gianas. Towards efficient, typed LR parsers. Manuscript, April 2005.

Google Scholar

[15]

François Pottier and Didier Rémy. The essence of ML type inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389--489. MIT Press, 2005.

Google Scholar

[16]

Yann Régis-Gianas. A prototype typechecker for ML with generalized algebraic data types. http://cristal.inria.fr/~regisgia/software/, July 2005.

Google Scholar

[17]

Didier Rémy. Simple, partial type inference for system $F$ based on type containment. In ACM International Conference on Functional Programming (ICFP), September 2005.

Digital Library

Google Scholar

[18]

Tim Sheard. Languages of the future. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 116--119, October 2004.

Digital Library

Google Scholar

[19]

Tim Sheard and Emir Pašaliý. Meta-programming with built-in type equality. In Workshop on Logical Frameworks and Meta-Languages (LFM), July 2004.

Google Scholar

[20]

Vincent Simonet and François Pottier. Constraint-based type inference for guarded algebraic data types. Research Report 5462, INRIA, January 2005.

Google Scholar

[21]

Peter J. Stuckey and Martin Sulzmann. Type inference for guarded recursive data types. Manuscript, February 2005.

Google Scholar

[22]

Sergei G. Vorobyov. An improved lower bound for the elementary theories of trees. In International Conference on Automated Deduction (CADE), volume 1104 of Lecture Notes in Computer Science, pages 275--287. Springer Verlag, 1996.

Digital Library

Google Scholar

[23]

Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In ACM Symposium on Principles of Programming Languages (POPL), pages 224--235, January 2003.

Digital Library

Google Scholar

Cited By

View all

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
Sieczkowski FStepanenko SSterling JBirkedal L(2024)The Essence of Generalized Algebraic Data TypesProceedings of the ACM on Programming Languages10.1145/36328668:POPL(695-723)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632866
Cagne PGhiorzi EJohann P(2024)GADTs are not (Even partial) functorsMathematical Structures in Computer Science10.1017/S0960129524000161(1-24)Online publication date: 27-Aug-2024
https://doi.org/10.1017/S0960129524000161
Show More Cited By

Index Terms

Stratified type inference for generalized algebraic data types
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
        Polymorphism
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Stratified type inference for generalized algebraic data types
Proceedings of the 2006 POPL Conference

Stratified type inference for generalized algebraic data types.
Pointwise generalized algebraic data types
TLDI '10: Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation

In the GADT (Generalized Algebraic Data Types) type system, a pattern-matching branch can draw type information from both the scrutinee type and the data constructor type. Even though the type system can handle complex interactions between the two types,...
Polymorphic type inference and abstract data types

Many statically typed programming languages provide an abstract data type construct, such as the module in Modula-2. However, in most of these languages, implementations of abstract data types are not first-class values. Thus, they cannot be assigned to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2006

432 pages

ISBN:1595930272

DOI:10.1145/1111037

General Chair:
Greg Morrisett
Harvard University, USA
,
Program Chair:
Simon Peyton Jones
Microsoft Research, UK

ACM SIGPLAN Notices Volume 41, Issue 1
Proceedings of the 2006 POPL Conference
January 2006
421 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1111320
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 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: 11 January 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL06

Sponsor:

POPL06: The 33rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2006

January 11 - 13, 2006

South Carolina, Charleston, USA

Acceptance Rates

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

40
Total Citations
View Citations
459
Total Downloads

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

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

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
Sieczkowski FStepanenko SSterling JBirkedal L(2024)The Essence of Generalized Algebraic Data TypesProceedings of the ACM on Programming Languages10.1145/36328668:POPL(695-723)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632866
Cagne PGhiorzi EJohann P(2024)GADTs are not (Even partial) functorsMathematical Structures in Computer Science10.1017/S0960129524000161(1-24)Online publication date: 27-Aug-2024
https://doi.org/10.1017/S0960129524000161
Castagna GLaurent MNguyễn KLutze M(2022)On type-cases, union elimination, and occurrence typingProceedings of the ACM on Programming Languages10.1145/34986746:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498674
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
Serrano AHage JPeyton Jones SVytiniotis D(2020)A quick look at impredicativityProceedings of the ACM on Programming Languages10.1145/34089714:ICFP(1-29)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408971
Dunfield JKrishnaswami N(2019)Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed typesProceedings of the ACM on Programming Languages10.1145/32903223:POPL(1-28)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290322
Chen SErwig M(2016)Principal type inference for GADTsACM SIGPLAN Notices10.1145/2914770.283766551:1(416-428)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837665
Chen SErwig MBodik RMajumdar R(2016)Principal type inference for GADTsProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2837614.2837665(416-428)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2837614.2837665
Williams TDagand PRémy DMagalhäes JRompf T(2014)Ornaments in practiceProceedings of the 10th ACM SIGPLAN workshop on Generic programming10.1145/2633628.2633631(15-24)Online publication date: 26-Aug-2014
https://dl.acm.org/doi/10.1145/2633628.2633631
Show More Cited By

View Options

Login options

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

Cited By

Index Terms

Recommendations

Stratified type inference for generalized algebraic data types

Pointwise generalized algebraic data types

Polymorphic type inference and abstract data types