Stephanie Weirich
Pritam Choudhury
Richard A. Eisenberg
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Modern Haskell supports zero-cost coercions, a mechanism where types that share the same run-time representation may be freely converted between. To make sure such conversions are safe and desirable, this feature relies on a mechanism of roles to prohibit invalid coercions. In this work, we show how to incorporate roles into dependent types systems and prove, using the Coq proof assistant, that the resulting system is sound. We have designed this work as a foundation for the addition of dependent types to the Glasgow Haskell Compiler, but we also expect that it will be of use to designers of other dependently-typed languages who might want to adopt Haskell’s safe coercions feature.
Supplemental Material
- Andreas Abel and Gabriel Scherer. 2012. On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8, 1 (2012).Google Scholar
- Andreas Abel, Andrea Vezzosi, and Théo Winterhalter. 2017. Normalization by evaluation for sized dependent types. PACMPL 1, ICFP (2017), 33:1–33:30. Google ScholarDigital Library
- Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. 2016. Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France (LIPIcs), Jean-Marc Talbot and Laurent Regnier (Eds.), Vol. 62. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 21:1–21:17.Google Scholar
- Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. 2008. Engineering Formal Metatheory. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 3–15. Google ScholarDigital Library
- Brian Aydemir and Stephanie Weirich. 2010. LNgen: Tool Support for Locally Nameless Representations. Technical Report MS-CIS-10-24. Computer and Information Science, University of Pennsylvania.Google Scholar
- Henk Barendregt. 1991. Introduction to generalized type systems. J. Funct. Program. 1, 2 (1991), 125–154.Google ScholarCross Ref
- H. P. Barendregt. 1984. The Lambda Calculus: Its Syntax and Semantics. Elsevier.Google Scholar
- Bruno Barras and Bruno Bernardo. 2008. The Implicit Calculus of Constructions as a Programming Language with Dependent Types. In Foundations of Software Science and Computational Structures, Roberto Amadio (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 365–379. Google ScholarDigital Library
- Jean-Philippe Bernardy and Guilhem Moulin. 2013. Type-theory in color. In ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013, Greg Morrisett and Tarmo Uustalu (Eds.). ACM, 61–72. Google ScholarDigital Library
- Baldur Blöndal, Andres Löh, and Ryan Scott. 2018. Deriving via: or, how to turn hand-written instances into an anti-pattern. In Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2018, St. Louis, MO, USA, September 27-17, 2018, Nicolas Wu (Ed.). ACM, 55–67. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Prog. 23 (2013).Google Scholar
- Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. 2016. Safe zero-cost coercions for Haskell. Journal of Functional Programming 26 (2016).Google Scholar
- Paolo Capriotti. 2016. Models of type theory with strict equality. Ph.D. Dissertation. School of Computer Science, University of Nottingham, Nottingham, UK. http://arxiv.org/abs/1702.04912Google Scholar
- Luca Cardelli. 1986. A Polymorphic Lambda Calculus with Type:Type. Technical Report 10. Digital Equipment Corporation, SRC.Google Scholar
- Manuel M. T. Chakravarty, Gabriele Keller, and Simon L. Peyton Jones. 2005. Associated type synonyms. In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005, Olivier Danvy and Benjamin C. Pierce (Eds.). ACM, 241–253. Google ScholarDigital Library
- Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015) (Leibniz International Proceedings in Informatics (LIPIcs)), Tarmo Uustalu (Ed.), Vol. 69. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 5:1–5:34.Google Scholar
- Karl Crary and Stephanie Weirich. 1999. Flexible Type Analysis. In Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP). Paris, France, 233–248. Google ScholarDigital Library
- Dominique Devriese and Frank Piessens. 2011. On the bright side of type classes: instance arguments in Agda. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy (Eds.). ACM, 143–155. Google ScholarDigital Library
- Larry Diehl, Denis Firsov, and Aaron Stump. 2018. Generic zero-cost reuse for dependent types. PACMPL 2, ICFP (2018), 104:1–104:30. Google ScholarDigital Library
- Richard A. Eisenberg. 2015. An Overabundance of Equality: Implementing Kind Equalities into Haskell. Technical Report MS-CIS-15-10. University of Pennsylvania. http://www.cis.upenn.edu/~eir/papers/2015/equalities/equalities.pdfGoogle Scholar
- Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. Ph.D. Dissertation. University of Pennsylvania.Google Scholar
- 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. Google ScholarDigital Library
- Adam Gundry. 2013. Type Inference, Haskell and Dependent Types. Ph.D. Dissertation. University of Strathclyde.Google Scholar
- Robert Harper, Furio Honsell, and Gordon Plotkin. 1993. A Framework for Defining Logics. J. ACM 40, 1 (Jan. 1993), 143–184. Google ScholarDigital Library
- Robert Harper and J. Gregory Morrisett. 1995. Compiling Polymorphism Using Intensional Type Analysis. In Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, Ron K. Cytron and Peter Lee (Eds.). ACM Press, 130–141. Google ScholarDigital Library
- Per Martin-Löf. 1971. A Theory of Types. (1971). Unpublished manuscript.Google Scholar
- Alexandre Miquel. 2001. The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping. Springer Berlin Heidelberg, Berlin, Heidelberg, 344–359. Google ScholarDigital Library
- Nathan Mishra-Linger and Tim Sheard. 2008. Erasure and Polymorphism in Pure Type Systems. In Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings (Lecture Notes in Computer Science), Roberto M. Amadio (Ed.), Vol. 4962. Springer, 350–364. Google ScholarDigital Library
- Andreas Nuyts and Dominique Devriese. 2018. Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, Anuj Dawar and Erich Grädel (Eds.). ACM, 779–788. Google ScholarDigital Library
- Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese. 2017. Parametric quantifiers for dependent type theory. PACMPL 1, ICFP (2017), 32:1–32:29. Google ScholarDigital Library
- Nicolas Oury and Wouter Swierstra. 2008. The power of Pi. In Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, James Hook and Peter Thiemann (Eds.). ACM, 39–50. Google ScholarDigital Library
- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. 2006. Simple unification-based type inference for GADTs. In International Conference on Functional Programming (ICFP ’06). ACM. Google ScholarDigital Library
- Frank Pfenning. 2001. Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. In Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS’01), J. Halpern (Ed.). IEEE Computer Society Press, Boston, Massachusetts, 221–230. Google ScholarDigital Library
- Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. 2010. Ott: Effective tool support for the working semanticist. Journal of Functional Programming 20, 1 (Jan. 2010). Google ScholarDigital Library
- Matthieu Sozeau and Nicolas Oury. 2008. First-Class Type Classes. In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings (Lecture Notes in Computer Science), Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar (Eds.), Vol. 5170. Springer, 278–293. Google ScholarDigital Library
- Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. 2007. System F with type equality coercions. In Types in languages design and implementation (TLDI ’07). ACM. Google ScholarDigital Library
- Vladimir Voevodsky. 2013. A simple type system with two identity types. Unpublished note (2013), 8 pages. https: //www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdfGoogle Scholar
- Stephanie Weirich. 2014. Depending on Types. Invited keynote given at ICFP 2014. Google ScholarDigital Library
- Stephanie Weirich. 2017. The Influence of Dependent Types. Invited keynote given at POPL 2017. Google ScholarDigital Library
- Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard A. Eisenberg. 2019. A Role for Dependent Types in Haskell (Extended Version). https://arxiv.org/abs/1905.13706Google Scholar
- Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. 2013. System FC with explicit kind equality. In Proceedings of The 18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13). Boston, MA, 275–286. Google ScholarDigital Library
- Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo 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. Google ScholarDigital Library
- Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve Zdancewic. 2011. Generative Type Abstraction and Type-level Computation. In POPL 11: 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, January 26–28, 2011. Austin, TX, USA. 227–240. Google ScholarDigital Library
- Thomas Winant and Dominique Devriese. 2018. Coherent explicit dictionary application for Haskell. In Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2018, St. Louis, MO, USA, September 27-17, 2018, Nicolas Wu (Ed.). ACM, 81–93. Google ScholarDigital Library
- Hongwei Xi, Chiyan Chen, and Gang Chen. 2003. Guarded recursive datatype constructors. In Principles of Programming Languages (POPL ’03). ACM. Google ScholarDigital Library
- Ningning Xie and Richard A. Eisenberg. 2018. Coercion Quantification. In Haskell Implementors’ Workshop.Google Scholar
Index Terms
- A role for dependent types in Haskell
Recommendations
A specification for dependent types in Haskell
We propose a core semantics for Dependent Haskell, an extension of Haskell with full-spectrum dependent types. Our semantics consists of two related languages. The first is a Curry-style dependently-typed language with nontermination, irrelevant ...
Depending on types
ICFP '14Is Haskell a dependently typed programming language? Should it be? GHC's many type-system features, such as Generalized Algebraic Datatypes (GADTs), datatype promotion, multiparameter type classes, and type families, give programmers the ability to ...
Depending on types
ICFP '14: Proceedings of the 19th ACM SIGPLAN international conference on Functional programmingIs Haskell a dependently typed programming language? Should it be? GHC's many type-system features, such as Generalized Algebraic Datatypes (GADTs), datatype promotion, multiparameter type classes, and type families, give programmers the ability to ...
Comments