More Web Proxy on the site http://driver.im/

article

Public Access

Principal type inference for GADTs

Authors:

Martin ErwigAuthors Info & Claims

ACM SIGPLAN Notices, Volume 51, Issue 1

Pages 416 - 428

https://doi.org/10.1145/2914770.2837665

Published: 11 January 2016 Publication History

Abstract

We present a new method for GADT type inference that improves the precision of previous approaches. In particular, our approach accepts more type-correct programs than previous approaches when they do not employ type annotations. A side benefit of our approach is that it can detect a wide range of runtime errors that are missed by previous approaches. Our method is based on the idea to represent type refinements in pattern-matching branches by choice types, which facilitate a separation of the typing and reconciliation phases and thus support case expressions. This idea is formalized in a type system, which is both sound and a conservative extension of the classical Hindley-Milner system. We present the results of an empirical evaluation that compares our algorithm with previous approaches.

References

[1]

M. Blume, U. A. Acar, and W. Chae. Extensible programming with first-class cases. In ACM SIGPLAN International Conference on Functional Programming, pages 239–250, 2006.

Digital Library

[2]

S. Chen and M. Erwig. Counter-factual typing for debugging type errors. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 583–594, 2014.

Digital Library

[3]

S. Chen and M. Erwig. Guided type debugging. In Functional and Logic Programming, LNCS 8475, pages 35–51. 2014.

[4]

S. Chen, M. Erwig, and E. Walkingshaw. An error-tolerant type system for variational lambda calculus. In ACM SIGPLAN International Conference on Functional Programming, pages 29–40, 2012.

Digital Library

[5]

S. Chen, M. Erwig, and E. Walkingshaw. Extending type inference to variational programs. ACM Trans. Program. Lang. Syst., 36(1):1:1– 1:54, Mar. 2014.

Digital Library

[6]

J. Cheney and R. Hinze. A lightweight implementation of generics and dynamics. In ACM SIGPLAN Workshop on Haskell, pages 90– 104, 2002.

Digital Library

[7]

L. Damas and R. Milner. Principal Type-Schemes for Functional Programs. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 207–212, 1982.

Digital Library

[8]

M. Felleisen, R. B. Findler, M. Flatt, and S. Krishnamurthi. How to design programs. MIT Press Cambridge, 2001.

[9]

J. Garrigue and J. L. Normand. Adding gadts to ocaml: the direct approach. In Workshop on ML, 2011.

[10]

J. Garrigue and D. Rémy. Ambivalent types for principal type inference with GADTs. In Programming Languages and Systems, LNCS 8301, pages 257–272. 2013.

Digital Library

[11]

F. Henglein. Type inference with polymorphic recursion. ACM Trans. Program. Lang. Syst., 15(2):253–289, Apr. 1993.

Digital Library

[12]

G. Karachalias, T. Schrijvers, D. Vytiniotis, and S. P. Jones. Gadts meet their match: Pattern-matching warnings that account for gadts, guards, and laziness. In ACM SIGPLAN International Conference on Functional Programming, pages 424–436, 2015.

Digital Library

[13]

C. Kästner, P. G. Giarrusso, T. Rendel, S. Erdweg, K. Ostermann, and T. Berger. Variability-Aware Parsing in the Presence of Lexical Macros and Conditional Compilation. In ACM SIGPLAN Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications, pages 805–824, 2011.

Digital Library

[14]

A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. Type reconstruction in the presence of polymorphic recursion. ACM Trans. Program. Lang. Syst., 15(2):290–311, Apr. 1993.

Digital Library

[15]

J. Liebig, A. von Rhein, C. Kästner, S. Apel, J. Dörre, and C. Lengauer. Scalable analysis of variable software. In Foundations of Software Engineering, pages 81–91, 2013.

Digital Library

[16]

C.-k. Lin. Programming monads operationally with unimo. In ACM SIGPLAN International Conference on Functional Programming, pages 274–285, 2006.

Digital Library

[17]

C.-k. Lin. Practical Type Inference for the GADT Type System. PhD thesis, Portland State University, 2010.

Digital Library

[18]

C.-k. Lin and T. Sheard. Pointwise generalized algebraic data types. In ACM SIGPLAN Workshop on Types in Language Design and Implementation, pages 51–62, 2010.

Digital Library

[19]

A. Mycroft. Polymorphic type schemes and recursive definitions. In International Symposium on Programming, LNCS 167, pages 217– 228, 1984.

Digital Library

[20]

M. Odersky, M. Sulzmann, and M. Wehr. Type Inference with Constrained Types. Theory and Practice of Object Systems, 5(1):35–55, 1999.

Digital Library

[21]

S. Peyton Jones, D. Vytiniotis, S. Weirich, and G. Washburn. Simple unification-based type inference for GADTs. In ACM SIGPLAN International Conference on Functional Programming, pages 50–61, 2006.

Digital Library

[22]

S. Peyton Jones, G. Washburn, and S. Weirich. Wobbly types: type inference for generalised algebraic data types. Technical Report MSCIS-05-26, University of Pennsylvania, July 2004.

[23]

B. C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, School of Computer Science, Carnegie Mellon University, 1991.

[24]

B. C. Pierce. Types and Programming Languages. MIT Press, 2002.

Digital Library

[25]

F. Pottier and Y. Régis-Gianas. Stratified type inference for generalized algebraic data types. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 232–244, 2006.

Digital Library

[26]

N. Ramsey. On teaching *how to design programs*: Observations from a newcomer. In ACM SIGPLAN International Conference on Functional Programming, pages 153–166, 2014.

Digital Library

[27]

T. Schrijvers, S. Peyton Jones, M. Sulzmann, and D. Vytiniotis. Complete and decidable type inference for GADTs. In ACM SIGPLAN International Conference on Functional Programming, pages 341–352, 2009.

Digital Library

[28]

T. Sheard. Generic programming in Omega. In Datatype-Generic Programming, LNCS 4719, pages 258–284, 2006.

[29]

T. Sheard and N. Linger. Programming in Omega. In CEFP, LNCS 5161, pages 158–227, 2007.

[30]

V. Simonet and F. Pottier. A constraint-based approach to guarded algebraic data types. ACM Trans. on Programming Languages and Systems, 29(1):1–38, 2007.

Digital Library

[31]

P. J. Stuckey and M. Sulzmann. Type inference for guarded recursive data types. CoRR, abs/cs/0507037:1–15, 2005.

[32]

M. Sulzmann, T. Schrijvers, and P. J. Stuckey. Type inference for GADTs via Herbrand constraint abduction. Technical Report CW507, University of Leuven, January 2008.

[33]

S. Vorobyov. An improved lower bound for the elementary theories of trees. In International Conference on Automated Deduction, LNCS 1104, pages 275–287. 1996.

Digital Library

[34]

D. Vytiniotis, S. Peyton Jones, T. Schrijvers, and M. Sulzmann. Outsidein(x) modular type inference with local assumptions. Journal of Functional Programming, 21(4-5):333–412, Sept. 2011.

Digital Library

[35]

S. Weirich. Depending on types. In ACM SIGPLAN International Conference on Functional Programming, pages 241–241, 2014.

Digital Library

[36]

H. Xi, C. Chen, and G. Chen. Guarded recursive datatype constructors. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 224–235, 2003.

Digital Library

Cited By

Chen SWu B(2020)Efficient Counter-factual Type Error DebuggingScience of Computer Programming10.1016/j.scico.2020.102544(102544)Online publication date: Sep-2020
https://doi.org/10.1016/j.scico.2020.102544
Peng YWang CWang WGao CLyu M(2023)Generative Type Inference for Python2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE)10.1109/ASE56229.2023.00031(988-999)Online publication date: 11-Sep-2023
https://doi.org/10.1109/ASE56229.2023.00031
CAMPORA JCHEN SERWIG MWALKINGSHAW E(2022)Migrating gradual typesJournal of Functional Programming10.1017/S095679682200008932Online publication date: 6-Oct-2022
https://doi.org/10.1017/S0956796822000089
Show More Cited By

Index Terms

Principal type inference for GADTs
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
      2. Language types
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs

Recommendations

Principal type inference for GADTs
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

We present a new method for GADT type inference that improves the precision of previous approaches. In particular, our approach accepts more type-correct programs than previous approaches when they do not employ type annotations. A side benefit of our ...
Simple unification-based type inference for GADTs
Proceedings of the 2006 ICFP conference

Generalized algebraic data types (GADTs), sometimes known as "guarded recursive data types" or "first-class phantom types", are a simple but powerful generalization of the data types of Haskell and ML. Recent works have given compelling examples of the ...
Complete and decidable type inference for GADTs
ICFP '09

GADTs have proven to be an invaluable language extension, for ensuring data invariants and program correctness among others. Unfortunately, they pose a tough problem for type inference: we lose the principal-type property, which is necessary for modular ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 51, Issue 1

POPL '16

January 2016

815 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2914770

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2016
815 pages
ISBN:9781450335492
DOI:10.1145/2837614
General Chair:
Rastislav Bodik
UC Berkeley, USA
,
Program Chair:
Rupak Majumdar
MPI-SWS, Germany

Copyright © 2016 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: 11 January 2016

Published in SIGPLAN Volume 51, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
1,197
Total Downloads

Downloads (Last 12 months)230
Downloads (Last 6 weeks)20

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chen SWu B(2020)Efficient Counter-factual Type Error DebuggingScience of Computer Programming10.1016/j.scico.2020.102544(102544)Online publication date: Sep-2020
https://doi.org/10.1016/j.scico.2020.102544
Peng YWang CWang WGao CLyu M(2023)Generative Type Inference for Python2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE)10.1109/ASE56229.2023.00031(988-999)Online publication date: 11-Sep-2023
https://doi.org/10.1109/ASE56229.2023.00031
CAMPORA JCHEN SERWIG MWALKINGSHAW E(2022)Migrating gradual typesJournal of Functional Programming10.1017/S095679682200008932Online publication date: 6-Oct-2022
https://doi.org/10.1017/S0956796822000089
Eisenberg RSchrijvers T(2020)Stitch: the sound type-indexed type checker (functional pearl)Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell10.1145/3406088.3409015(39-53)Online publication date: 27-Aug-2020
https://dl.acm.org/doi/10.1145/3406088.3409015
Osera PDarais DGibbons J(2019)Constraint-based type-directed program synthesisProceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3331554.3342608(64-76)Online publication date: 18-Aug-2019
https://dl.acm.org/doi/10.1145/3331554.3342608
Chen SWu B(2019)Efficient Counter-factual Type Error Debugging2019 International Symposium on Theoretical Aspects of Software Engineering (TASE)10.1109/TASE.2019.00-13(99-106)Online publication date: Jul-2019
https://doi.org/10.1109/TASE.2019.00-13
Moreira GVasconcellos CRibeiro RCamarão CSulzmann M(2018)Type inference for GADTs, outsidein and anti-unificationProceedings of the XXII Brazilian Symposium on Programming Languages10.1145/3264637.3264644(51-58)Online publication date: 20-Sep-2018
https://dl.acm.org/doi/10.1145/3264637.3264644
Ostermann KJabs J(2018)Dualizing Generalized Algebraic Data Types by Matrix TranspositionProgramming Languages and Systems10.1007/978-3-319-89884-1_3(60-85)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89884-1_3
Campora JChen SErwig MWalkingshaw E(2017)Migrating gradual typesProceedings of the ACM on Programming Languages10.1145/31581032:POPL(1-29)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158103
Hubbard SWalkingshaw ESeidl CTeixeira L(2016)Formula choice calculusProceedings of the 7th International Workshop on Feature-Oriented Software Development10.1145/3001867.3001873(49-57)Online publication date: 30-Oct-2016
https://dl.acm.org/doi/10.1145/3001867.3001873
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Media

Figures

Other

Tables

View Issue’s Table of Contents