{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:15:56Z","timestamp":1781892956874,"version":"3.54.5"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1704041,1521539"],"award-info":[{"award-number":["1704041,1521539"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"<jats:p>\n            Modern Haskell supports\n            <jats:italic>zero-cost<\/jats:italic>\n            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\n            <jats:italic>roles<\/jats:italic>\n            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\u2019s safe coercions feature.\n          <\/jats:p>","DOI":"10.1145\/3341705","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["A role for dependent types in Haskell"],"prefix":"10.1145","volume":"3","author":[{"given":"Stephanie","family":"Weirich","sequence":"first","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pritam","family":"Choudhury","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Antoine","family":"Voizard","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Richard A.","family":"Eisenberg","sequence":"additional","affiliation":[{"name":"Bryn Mawr College, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8, 1","author":"Abel Andreas","year":"2012","unstructured":"Andreas Abel and Gabriel Scherer . 2012. On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8, 1 ( 2012 ). Andreas Abel and Gabriel Scherer. 2012. On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8, 1 (2012)."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110277"},{"key":"e_1_2_2_3_1","volume-title":"Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016","author":"Altenkirch Thorsten","year":"2016","unstructured":"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\u201321:17. 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\u201321:17."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800020025"},{"key":"e_1_2_2_7_1","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt H. P.","unstructured":"H. P. Barendregt . 1984. The Lambda Calculus: Its Syntax and Semantics . Elsevier . H. P. Barendregt. 1984. The Lambda Calculus: Its Syntax and Semantics. Elsevier."},{"key":"e_1_2_2_8_1","volume-title":"Foundations of Software Science and Computational Structures","author":"Barras Bruno","unstructured":"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\u2013379. 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\u2013379."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500577"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242746"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122967"},{"key":"e_1_2_2_12_1","volume-title":"a general-purpose dependently typed programming language: Design and implementation. J. Funct. Prog. 23","author":"Brady Edwin","year":"2013","unstructured":"Edwin Brady . 2013. Idris , a general-purpose dependently typed programming language: Design and implementation. J. Funct. Prog. 23 ( 2013 ). Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Prog. 23 (2013)."},{"key":"e_1_2_2_13_1","volume-title":"Simon Peyton Jones, and Stephanie Weirich","author":"Breitner Joachim","year":"2016","unstructured":"Joachim Breitner , Richard A. Eisenberg , Simon Peyton Jones, and Stephanie Weirich . 2016 . Safe zero-cost coercions for Haskell. Journal of Functional Programming 26 (2016). Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. 2016. Safe zero-cost coercions for Haskell. Journal of Functional Programming 26 (2016)."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086397"},{"key":"e_1_2_2_17_1","volume-title":"21st International Conference on Types for Proofs and Programs (TYPES 2015) (Leibniz International Proceedings in Informatics (LIPIcs))","author":"Cohen Cyril","unstructured":"Cyril Cohen , Thierry Coquand , Simon Huber , and Anders M\u00f6rtberg . 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\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany , 5:1\u20135:34. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 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\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 5:1\u20135:34."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317906"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034796"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236799"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535856"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199475"},{"key":"e_1_2_2_27_1","unstructured":"Per Martin-L\u00f6f. 1971. A Theory of Types. (1971). Unpublished manuscript.  Per Martin-L\u00f6f. 1971. A Theory of Types. (1971). Unpublished manuscript."},{"key":"e_1_2_2_28_1","volume-title":"The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping","author":"Miquel Alexandre","unstructured":"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\u2013359. 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\u2013359."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792803.1792828"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209119"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110276"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411213"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871845"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_2_2_38_1","volume-title":"A simple type system with two identity types. Unpublished note","author":"Voevodsky Vladimir","year":"2013","unstructured":"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.pdf 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.pdf"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2631168"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009923"},{"key":"e_1_2_2_41_1","volume-title":"Eisenberg","author":"Weirich Stephanie","year":"2019","unstructured":"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.13706 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.13706"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500599"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926411"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242752"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"key":"e_1_2_2_47_1","volume-title":"Coercion Quantification. In Haskell Implementors\u2019 Workshop.","author":"Xie Ningning","unstructured":"Ningning Xie and Richard A. Eisenberg . 2018 . Coercion Quantification. In Haskell Implementors\u2019 Workshop. Ningning Xie and Richard A. Eisenberg. 2018. Coercion Quantification. In Haskell Implementors\u2019 Workshop."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341705","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341705","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341705","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:23Z","timestamp":1750207403000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341705"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":41,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341705"],"URL":"https:\/\/doi.org\/10.1145\/3341705","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}