research-article

Public Access

Stitch: the sound type-indexed type checker (functional pearl)

Author:

Richard A. EisenbergAuthors Info & Claims

Haskell 2020: Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell

Pages 39 - 53

https://doi.org/10.1145/3406088.3409015

Published: 09 August 2020 Publication History

Abstract

A classic example of the power of generalized algebraic datatypes (GADTs) to verify a delicate implementation is the type-indexed expression AST. This functional pearl refreshes this example, casting it in modern Haskell using many of GHC's bells and whistles. The Stitch interpreter is a full executable interpreter, with a parser, type checker, common-subexpression elimination, and a REPL. Making heavy use of GADTs and type indices, the Stitch implementation is clean Haskell code and serves as an existence proof that Haskell's type system is advanced enough for the use of fancy types in a practical setting. The paper focuses on guiding the reader through these advanced topics, enabling them to adopt the techniques demonstrated here.

Supplemental Material

MP4 File

Presentation Videos

Download
40.81 MB

References

[1]

Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. 2018. A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs. Proc. ACM Program. Lang. 2, ICFP, Article 90 ( July 2018 ), 30 pages. htps://doi.org/10.1145/3236785

Digital Library

[2]

Guillaume Allais, James Chapman, Conor McBride, and James McKinna. 2017. Type-and-scope Safe Programs and Their Proofs. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017 ). ACM, New York, NY, USA, 195-207. htps://doi.org/10.1145/3018610.3018613

Digital Library

[3]

Lennart Augustsson. 1998. Cayenne-a language with dependent types. In Proc. ACM SIGPLAN International Conference on Functional Programming (ICFP '98). ACM, 239-250.

Digital Library

[4]

Lennart Augustsson and Magnus Carlsson. 1999. An exercise in dependent types: A well-typed interpreter. ( 1999 ). htp://citeseerx.ist.psu. edu/viewdoc/download?doi=10.1.1.39.2895& rep=rep1&type=pdf Unpublished manuscript.

[5]

Nick Benton, Chung-Kil Hur, Andrew J. Kennedy, and Conor McBride. 2012. Strongly Typed Term Representations in Coq. Journal of Automated Reasoning 49, 2 ( 01 Aug 2012 ), 141-159. htps://doi.org/10. 1007/s10817-011-9219-0

Digital Library

[6]

Gert-Jan Bottu, Georgios Karachalias, Tom Schrijvers, Bruno C. d. S. Oliveira, and Philip Wadler. 2017. Quantified Class Constraints. In Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell (Haskell 2017 ). ACM, New York, NY, USA, 148-161. htps: //doi.org/10.1145/3122955.3122967

Digital Library

[7]

Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Prog. 23 ( 2013 ).

[8]

Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. 2016. Safe Zero-cost Coercions for Haskell. J. Funct. Program. 26 ( 2016 ), 1-79.

[9]

Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. 2009. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. J. Funct. Program. 19, 5 (Sept. 2009 ), 509-543.

Digital Library

[10]

Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyon Jones. 2005. Associated Type Synonyms. In International Conference on Functional Programming (ICFP '05). ACM.

[11]

Chiyan Chen and Hongwei Xi. 2003. Implementing Typeful Program Transformations. In Proceedings of the 2003 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM '03). ACM, New York, NY, USA, 20-28. htps://doi.org/10.1145/777388. 777392

Digital Library

[12]

Sheng Chen and Martin Erwig. 2016. Principal Type Inference for GADTs. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '16). ACM, New York, NY, USA, 416-428. htps://doi.org/10.1145/2837614.2837665

Digital Library

[13]

James Cheney and Ralf Hinze. 2003. First-Class Phantom Types. Technical Report. Cornell University.

[14]

David Raymond Christiansen. 2015. A Pretty Printer that Says What it Means. Talk, Haskell Implementors Workshop, Vancouver, BC, Canada. htps://www.youtube.com/watch?v=m7BBCcIDXSg

[15]

Nicolaas Govert de Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings) 75, 5 ( 1972 ), 381-392. htps://doi.org/10.1016/ 1385-7258 ( 72 ) 90034-0

[16]

Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. Ph.D. Dissertation. University of Pennsylvania.

[17]

Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie Weirich. 2014. Closed Type Families with Overlapping Equations. In Principles of Programming Languages (POPL '14). ACM.

[18]

Richard A. Eisenberg and Stephanie Weirich. 2012. Dependently Typed Programming with Singletons. In ACM SIGPLAN Haskell Symposium.

[19]

Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan Ahmed. 2016. Visible Type Application. In European Symposium on Programming (ESOP) (LNCS). Springer-Verlag.

[20]

Martin Erwig and Simon Peyton Jones. 2000. Pattern Guards and Transformational Patterns. In Haskell Workshop 2000 (haskell workshop 2000 ed.). htps://www.microsoft.com/en-us/research/publication/paternguards-and-transformational-paterns/

[21]

Matthías Páll Gissurarson. 2018. Suggesting Valid Hole Fits for Typed-Holes in Haskell. Master's thesis. Chalmers University of Technology, University of Gothenburg. htps://mpg.is/papers/ gissurarson2018suggesting-msc.pdf

[22]

Louis-Julien Guillemette and Stefan Monnier. 2008. A type-preserving compiler in Haskell. In Proc. 13th ACM SIGPLAN International Conference on Functional Programming (ICFP '08). ACM, 75-86.

Digital Library

[23]

Adam Gundry. 2013. Type Inference, Haskell and Dependent Types. Ph.D. Dissertation. University of Strathclyde.

[24]

Hiromi Ishii. 2014. Dependent Types in Haskell. School of Haskell blog. htps://www.schoolofhaskell.com/user/konn/prove-yourhaskell-for-great-safety/dependent-types-in-haskell

[25]

Mark P. Jones. 1995. Functional Programming with Overloading and Higher-Order Polymorphism. In Advanced Functional Programming, Johan Jeuring and Erik Meijer (Eds.). LNCS, Vol. 925. Springer Verlag.

[26]

Mark P. Jones. 2000. Type Classes with Functional Dependencies. In European Symposium on Programming.

[27]

Georgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis, and Simon Peyton Jones. 2015. GADTs meet their match. In International Conference on Functional Programming (ICFP '15). ACM.

[28]

Ralf Lämmel and Simon Peyton Jones. 2003. Scrap Your Boilerplate: A Practical Design Pattern for Generic Programming. In Workshop on Types in Languages Design and Implementation. ACM.

Digital Library

[29]

Ralf Lämmel and Simon Peyton Jones. 2005. Scrap Your Boilerplate With Class: Extensible Generic Functions. In ICFP.

[30]

Justin Le. 2018. Introduction to Singletons. ( 2018 ). htps://blog.jle.im/ entry/introduction-to-singletons-3.html

[31]

Daan Leijen. 2001. Parsec: a fast combinator parser. Technical Report UU-CS-2001-26. University of Utrecht.

[32]

Sam Lindley and Conor McBride. 2013. Hasochism: the pleasure and pain of dependently typed Haskell programming. In ACM SIGPLAN Haskell Symposium.

Digital Library

[33]

Andres Löh. 2012. lhs2TeX. Haskell package. htps://www.andresloeh.de/lhs2tex/

[34]

José Pedro Magalhães. 2012. The Right Kind of Generic Programming. ( 2012 ). To appear at WGP.

[35]

José Pedro Magalhães, Atze Dijkstra, Johan Jeuring, and Andres Löh. 2010. A generic deriving mechanism for Haskell. In Proceedings of the 3rd ACM Haskell Symposium on Haskell (Haskell '10). ACM.

Digital Library

[36]

Conor McBride. 2011. The Strathclyde Haskell Enhancement. htps: //personal.cis.strath.ac.uk/conor.mcbride/pub/she/.

[37]

Stefan Monnier and David Haguenauer. 2010. Singleton types here, singleton types there, singleton types everywhere. In Programming languages meets program verification (PLPV '10). ACM.

[38]

Dominic Orchard and Tom Schrijvers. 2010. Haskell Type Constraints Unleashed. In Functional and Logic Programming, Matthias Blume, Naoki Kobayashi, and Germán Vidal (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 56-71.

[39]

Emir Pašalić, Walid Taha, and Tim Sheard. 2002. Tagless Staged Interpreters for Typed Languages. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02). ACM, New York, NY, USA, 218-229. htps://doi.org/10.1145/ 581478.581499

Digital Library

[40]

Simon Peyton Jones. 2003. Wearing the Hair Shirt: A Retrospective on Haskell. Invited talk at POPL.

[41]

Simon Peyton Jones, Mark Jones, and Erik Meijer. 1997. Type classes: an exploration of the design space. In Haskell Workshop, John Launchbury (Ed.). Amsterdam, Netherlands.

[42]

Simon Peyton Jones and John Launchbury. 1991. Unboxed values as ifrst class citizens. In FPCA (LNCS), Vol. 523. 636-666.

[43]

Simon Peyton Jones and Mark Shields. 2004. Lexically-scoped type variables. ( 2004 ). htp://research.microsoft.com/en-us/um/people/ simonpj/papers/scoped-tyvars/ Draft.

[44]

Simon Peyton Jones, Andrew Tolmach, and Tony Hoare. 2001. Playing by the Rules: Rewriting as a practical optimisation technique in GHC. In Proceedings of the Haskell Workshop.

[45]

Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical type inference for arbitrary-rank types. Journal of Functional Programming 17, 1 (Jan. 2007 ).

Digital Library

[46]

Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geofrey Washburn. 2006. Simple unification-based type inference for GADTs. In International Conference on Functional Programming (ICFP '06). ACM.

[47]

Simon Peyton Jones, Geofrey Washburn, and Stephanie Weirich. 2004. Wobbly types: type inference for generalised algebraic data types. Technical Report MS-CIS-05-26. University of Pennsylvania.

[48]

Simon Peyton Jones, Stephanie Weirich, Richard A. Eisenberg, and Dimitrios Vytiniotis. 2016. A reflection on types. In A list of successes that can change the world. Springer. A festschrift in honor of Phil Wadler.

[49]

Frank Pfenning and Peter Lee. 1989. LEAP: A language with eval and polymorphism. In TAPSOFT '89, J. Díaz and F. Orejas (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 345-359.

[50]

Matthew Pickering, Gergő Érdi, Simon Peyton Jones, and Richard A. Eisenberg. 2016. Pattern Synonyms. In ACM SIGPLAN Haskell Symposium. ACM.

[51]

Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, MA.

Digital Library

[52]

Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. 2010. Ott: Efective tool support for the working semanticist. Journal of Functional Programming 20, 1 (Jan. 2010 ).

Digital Library

[53]

Jan Stolarek, Simon Peyon Jones, and Richard A. Eisenberg. 2015. Injective Type Families for Haskell. In Haskell Symposium (Haskell '15). ACM.

[54]

Walid Taha, Henning Makholm, and John Hughes. 2001. Tag elimination and Jones-optimality. In Programs as Data Objects, Olivier Danvy and Andrzej Filinski (Eds.). LNCS, Vol. 2053. Springer Verlag.

[55]

David Terei, Simon Marlow, Simon Peyton Jones, and David Mazières. 2012. Safe Haskell. In Proceedings of the 2012 Haskell Symposium (Haskell '12). Association for Computing Machinery, New York, NY, USA, 137-148. htps://doi.org/10.1145/2364506.2364524

Digital Library

[56]

The Idris Team. 2017. Example: The Well-Typed Interpreter. The Idris Tutorial. htp://docs.idris-lang.org/en/latest/tutorial/interp.html

[57]

Dimitrios Vytiniotis, Simon Peyton Jones, and Tom Schrijvers. 2010. Let Should Not Be Generalized. In Types in Language Design and Implementation (TLDI '10). ACM.

[58]

Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. 2011. OutsideIn(X): Modular Type Inference with Local Assumptions. Journal of Functional Programming 21, 4-5 ( Sept. 2011 ).

Digital Library

[59]

Philip Wadler. 1987. Views: A Way for Pattern Matching to Cohabit with Data Abstraction. In Proceedings of the 14th ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages (POPL '87). Association for Computing Machinery, New York, NY, USA, 307-313. htps://doi.org/10.1145/41625.41653

Digital Library

[60]

Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. 2013. System FC with Explicit Kind Equality. In International Conference on Functional Programming (ICFP '13). ACM.

[61]

Stephanie Weirich. 2017. The Influence of Dependent Types. Keynote, POPL '17. htps://www.youtube.com/watch?v=rflCw9bT4_0

Digital Library

[62]

Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A. Eisenberg. 2017. A Specification for Dependent Types in Haskell. Proc. ACM Program. Lang. 1, ICFP, Article 31 ( Aug. 2017 ), 29 pages. htps://doi.org/10.1145/3110275

Digital Library

[63]

Stephanie Weirich, Brent A. Yorgey, and Tim Sheard. 2011. Binders Unbound. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP '11). ACM, New York, NY, USA, 333-345. htps://doi.org/10.1145/2034773.2034818

Digital Library

[64]

Hongwei Xi. 2004. Applied Type System. In Types for Proofs and Programs, Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 394-408.

[65]

Hongwei Xi, Chiyan Chen, and Gang Chen. 2003. Guarded recursive datatype constructors. In Principles of Programming Languages (POPL '03). ACM.

Digital Library

[66]

Ningning Xie and Richard A. Eisenberg. 2018. Coercion Quantification. In Haskell Implementors' Workshop.

[67]

Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhães. 2012. Giving Haskell a promotion. In Types in Language Design and Implementation (TLDI '12). ACM.

Cited By

Liesnikov BCockx J(2024)Building a Correct-by-Construction Type Checker for a Dependently Typed Core LanguageProgramming Languages and Systems10.1007/978-981-97-8943-6_4(63-83)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_4
Boruch-Gruszecki AWaśko RXu YParreaux L(2022)A case for DOT: theoretical foundations for objects with pattern matching and GADT-style reasoningProceedings of the ACM on Programming Languages10.1145/35633426:OOPSLA2(1526-1555)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563342
Eisenberg RDuboc GWeirich SLee D(2021)An existential crisis resolved: type inference for first-class existential typesProceedings of the ACM on Programming Languages10.1145/34735695:ICFP(1-29)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473569
Show More Cited By

Index Terms

Stitch: the sound type-indexed type checker (functional pearl)

Recommendations

Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types

Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its applicability to a variety of type systems, its error reporting, and its ease of implementation. Following principles from ...
Dependently typed programming with singletons
Haskell '12: Proceedings of the 2012 Haskell Symposium

Haskell programmers have been experimenting with dependent types for at least a decade, using clever encodings that push the limits of the Haskell type system. However, the cleverness of these encodings is also their main drawback. Although the ideas ...
Dependently typed programming with singletons
Haskell '12

Haskell programmers have been experimenting with dependent types for at least a decade, using clever encodings that push the limits of the Haskell type system. However, the cleverness of these encodings is also their main drawback. Although the ideas ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

Haskell 2020: Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell

August 2020

150 pages

ISBN:9781450380508

DOI:10.1145/3406088

General Chair:
Tom Schrijvers

Copyright © 2020 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 August 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Available / v1.1

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Conference

ICFP '20

Sponsor:

SIGPLAN

ICFP '20: ACM SIGPLAN International Conference on Functional Programming

August 27, 2020

Virtual Event, USA

Acceptance Rates

Overall Acceptance Rate 57 of 143 submissions, 40%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
812
Total Downloads

Downloads (Last 12 months)235
Downloads (Last 6 weeks)29

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Liesnikov BCockx J(2024)Building a Correct-by-Construction Type Checker for a Dependently Typed Core LanguageProgramming Languages and Systems10.1007/978-981-97-8943-6_4(63-83)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_4
Boruch-Gruszecki AWaśko RXu YParreaux L(2022)A case for DOT: theoretical foundations for objects with pattern matching and GADT-style reasoningProceedings of the ACM on Programming Languages10.1145/35633426:OOPSLA2(1526-1555)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563342
Eisenberg RDuboc GWeirich SLee D(2021)An existential crisis resolved: type inference for first-class existential typesProceedings of the ACM on Programming Languages10.1145/34735695:ICFP(1-29)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473569
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

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 Table of Contents