Document Open Access Logo

Eta-Equivalence in Core Dependent Haskell

Authors Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, Stephanie Weirich

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2019.7.pdf
  • Filesize: 0.66 MB
  • 31 pages

Document Identifiers

Author Details

Anastasiya Kravchuk-Kirilyuk
  • Princeton University, NJ, USA
Antoine Voizard
  • University of Pennsylvania, Philadelphia, PA, USA
Stephanie Weirich
  • University of Pennsylvania, Philadelphia, PA, USA

Funding

This material is based upon work supported by the National Science Foundation under Grant No. 1521539 and Grant No. 1704041. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.

Cite AsGet BibTex

Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich. Eta-Equivalence in Core Dependent Haskell. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 7:1-7:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.TYPES.2019.7

Abstract

We extend the core semantics for Dependent Haskell with rules for η-equivalence. This semantics is defined by two related calculi, Systems D and DC. The first is a Curry-style dependently-typed language with nontermination, irrelevant arguments, and equality abstraction. The second, inspired by the Glasgow Haskell Compiler’s core language FC, is the explicitly-typed analogue of System D, suitable for implementation in GHC. Our work builds on and extends the existing metatheory for these systems developed using the Coq proof assistant.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Functional languages
  • Software and its engineering → Polymorphism
  • Theory of computation → Type theory
Keywords
  • Dependent types
  • Haskell
  • Irrelevance
  • Eta-equivalence

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Andreas Abel and Thorsten Altenkirch. A partial type checking algorithm for Type:Type. Electronic Notes in Theoretical Computer Science, 229(5):3-17, 2011. Proceedings of the Second Workshop on Mathematically Structured Functional Programming (MSFP 2008). URL: https://doi.org/10.1016/j.entcs.2011.02.013.
  2. Andreas Abel, Thierry Coquand, and Peter Dybjer. Normalization by evaluation for Martin-Löf type theory with typed equality judgements. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pages 3-12. IEEE, 2007. Google Scholar
  3. Andreas Abel, Joakim Öhman, and Andrea Vezzosi. Decidability of conversion for type theory in type theory. Proceedings of the acm on programming languages, 2(POPL):23, 2017. Google Scholar
  4. Andreas Abel and Gabriel Scherer. On irrelevance and algorithmic equality in predicative type theory. Logical Methods in Computer Science, 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:29)2012.
  5. Andreas Abel, Andrea Vezzosi, and Théo Winterhalter. Normalization by evaluation for sized dependent types. PACMPL, 1(ICFP):33:1-33:30, 2017. URL: https://doi.org/10.1145/3110277.
  6. ROBIN ADAMS. Pure type systems with judgemental equality. Journal of Functional Programming, 16(2):219–246, 2006. URL: https://doi.org/10.1017/S0956796805005770.
  7. Robert Atkey. The syntax and semantics of quantitative type theory. In LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9-12, 2018, Oxford, United Kingdom, 2018. URL: https://doi.org/10.1145/3209108.3209189.
  8. Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering formal metatheory. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 3-15, January 2008. Google Scholar
  9. Brian Aydemir and Stephanie Weirich. LNgen: Tool support for locally nameless representations. Technical Report MS-CIS-10-24, Computer and Information Science, University of Pennsylvania, June 2010. Google Scholar
  10. H. P. Barendregt. Lambda Calculi with Types, page 117–309. Oxford University Press, Inc., USA, 1993. Google Scholar
  11. Hendrik Pieter Barendregt. The Lambda Calculus - its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985. Google Scholar
  12. Henk Barendregt. Introduction to generalized type systems. J. Funct. Program., 1(2):125-154, 1991. Google Scholar
  13. Bruno Barras and Bruno Bernardo. The implicit calculus of constructions as a programming language with dependent types. In Roberto Amadio, editor, Foundations of Software Science and Computational Structures, pages 365-379, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  14. Edwin Brady. Practical Implementation of a Dependently Typed Functional Programming Language. PhD thesis, Durham University, 2005. Google Scholar
  15. Luca Cardelli. A polymorphic λ-calculus with Type:Type. Technical report, DEC SRC, 1986. URL: http://lucacardelli.name/Papers/TypeType.A4.pdf.
  16. Thierry Coquand. A calculus of constructions. manuscript, November 1986. Google Scholar
  17. Thierry Coquand. An algorithm for testing conversion in type theory. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 255-279. Cambridge University Press, New York, NY, USA, 1991. Google Scholar
  18. Thierry Coquand. An algorithm for type-checking dependent types. Science of computer programming., 26(1-3):167,177, 1996-05. Google Scholar
  19. Thierry Coquand and Makoto Takeyama. An implementation of type: type. In International Workshop on Types for Proofs and Programs, pages 53-62. Springer, 2000. Google Scholar
  20. Richard A. Eisenberg. Dependent Types in Haskell: Theory and Practice. PhD thesis, University of Pennsylvania, 2016. Google Scholar
  21. Richard A. Eisenberg and Stephanie Weirich. Dependently typed programming with singletons. In ACM SIGPLAN Haskell Symposium, 2012. Google Scholar
  22. Adam Gundry. Type Inference, Haskell and Dependent Types. PhD thesis, University of Strathclyde, 2013. Google Scholar
  23. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. J. ACM, 40(1):143-184, January 1993. URL: https://doi.org/10.1145/138027.138060.
  24. Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Logic, 6(1):61-101, January 2005. URL: https://doi.org/10.1145/1042038.1042041.
  25. J. Roger Hindley. The Church-Rosser property and a result in combinatory logic. PhD thesis, University of Newcastle upon Tyne, 1964. Google Scholar
  26. Csongor Kiss, Tony Field, Susan Eisenbach, and Simon Peyton Jones. Higher-order type-level programming in haskell. Proc. ACM Program. Lang., 3(ICFP), July 2019. URL: https://doi.org/10.1145/3341706.
  27. Sam Lindley and Conor McBride. Hasochism: the pleasure and pain of dependently typed Haskell programming. In ACM SIGPLAN Haskell Symposium, 2013. Google Scholar
  28. Z. Luo. ECC, an extended calculus of constructions. In [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pages 386-395, 1989. Google Scholar
  29. Per Martin-Löf. A theory of types. Unpublished manuscript, 1971. Google Scholar
  30. Per Martin-Löf. An intuitionistic theory of types: predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, Proceedings of the Logic Colloquium, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. North-Holland, 1975. Google Scholar
  31. Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Bibliopolis, 1984. Google Scholar
  32. Alexandre Miquel. The implicit calculus of constructions: Extending pure type systems with an intersection type binder and subtyping. In Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications, TLCA'01, pages 344-359, Berlin, Heidelberg, 2001. Springer-Verlag. Google Scholar
  33. Nathan Mishra-Linger and Tim Sheard. Erasure and polymorphism in pure type systems. In Roberto M. Amadio, editor, 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, volume 4962 of Lecture Notes in Computer Science, pages 350-364. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78499-9_25.
  34. Andreas Nuyts and Dominique Devriese. Degrees of relatedness: A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 779-788. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209119.
  35. Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese. Parametric quantifiers for dependent type theory. Proc. ACM Program. Lang., 1(ICFP):32:1-32:29, August 2017. URL: https://doi.org/10.1145/3110276.
  36. Frank Pfenning. On the undecidability of partial polymorphic type reconstruction. Technical report, Carnegie Mellon University, Pittsburgh, PA, USA, 1992. Google Scholar
  37. Frank Pfenning. Intensionality, extensionality, and proof irrelevance in modal type theory. In J. Halpern, editor, Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS'01), pages 221-230, Boston, Massachusetts, June 2001. IEEE Computer Society Press. Google Scholar
  38. Barry K. Rosen. Tree-manipulating systems and Church-Rosser theorems. J. ACM, 20(1):160-187, January 1973. URL: https://doi.org/10.1145/321738.321750.
  39. Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones. Guarded impredicative polymorphism. In Jeffrey S. Foster and Dan Grossman, editors, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, pages 783-796. ACM, 2018. URL: https://doi.org/10.1145/3192366.3192389.
  40. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. Ott: Effective tool support for the working semanticist. Journal of Functional Programming, 20(1), January 2010. Google Scholar
  41. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. Coq coq correct! verification of type checking and erasure for coq, in coq. Proc. ACM Program. Lang., 4(POPL):8:1-8:28, 2020. URL: https://doi.org/10.1145/3371076.
  42. M. Sulzmann, M. Chakravarty, S. Peyton Jones, and K. Donnelly. System F with type equality coercions. In François Pottier and George C. Necula, editors, Proceedings of TLDI'07: 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Nice, France, January 16, 2007, pages 53-66. ACM, 2007. Google Scholar
  43. The Coq Development Team. The Coq proof assistant, version 8.8.0, April 2018. URL: https://doi.org/10.5281/zenodo.1219885.
  44. Dimitrios Vytiniotis, Simon L. Peyton Jones, Tom Schrijvers, and Martin Sulzmann. Outsidein(x) modular type inference with local assumptions. J. Funct. Program., 21(4-5):333-412, 2011. URL: https://doi.org/10.1017/S0956796811000098.
  45. Stephanie Weirich. Depending on types, 2014. Invited keynote given at ICFP 2014. Google Scholar
  46. Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. System FC with explicit kind equality. In Proceedings of The 18th ACM SIGPLAN International Conference on Functional Programming, ICFP '13, pages 275-286, Boston, MA, September 2013. Google Scholar
  47. Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, and Richard A. Eisenberg. A specification for dependent types in Haskell. Proc. ACM Program. Lang., 1(ICFP):31:1-31:29, August 2017. URL: https://doi.org/10.1145/3110275.
  48. J.B. Wells. Typability and type checking in System F are equivalent and undecidable. Annals of Pure and Applied Logic, 98(1):111-156, 1999. URL: https://doi.org/10.1016/S0168-0072(98)00047-5.
  49. A.K. Wright and M. Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38-94, November 1994. URL: https://doi.org/10.1006/inco.1994.1093.
  50. Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira. Kind inference for datatypes. Proc. ACM Program. Lang., 4(POPL):53:1-53:28, 2020. URL: https://doi.org/10.1145/3371121.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact