{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:49:56Z","timestamp":1775868596285,"version":"3.50.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T00:00:00Z","timestamp":1629331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1703835 and 1704041"],"award-info":[{"award-number":["1703835 and 1704041"]}],"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":[[2021,8,22]]},"abstract":"<jats:p>\n            Despite the great success of inferring and programming with universal types, their dual\u2014existential types\u2014are much harder to work with. Existential types are useful in building abstract types, working with indexed types, and providing first-class support for refinement types. This paper, set in the context of Haskell, presents a bidirectional type-inference algorithm that infers where to introduce and eliminate existentials without any annotations in terms, along with an explicitly typed, type-safe core language usable as a compilation target. This approach is backward compatible. The key ingredient is to use\n            <jats:italic>strong<\/jats:italic>\n            existentials, which support (lazily) projecting out the encapsulated data, not weak existentials accessible only by pattern-matching.\n          <\/jats:p>","DOI":"10.1145\/3473569","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["An existential crisis resolved: type inference for first-class existential types"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7669-9781","authenticated-orcid":false,"given":"Richard A.","family":"Eisenberg","sequence":"first","affiliation":[{"name":"Tweag, France"}]},{"given":"Guillaume","family":"Duboc","sequence":"additional","affiliation":[{"name":"ENS Lyon, France \/ Tweag, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6756-9168","authenticated-orcid":false,"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]},{"given":"Daniel","family":"Lee","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"Lennart Augustsson. 1994. Haskell B. user\u2019s manual. https:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.50.5800&rep=rep1&type=pdf  Lennart Augustsson. 1994. Haskell B. user\u2019s manual. https:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.50.5800&rep=rep1&type=pdf"},{"key":"e_1_2_2_2_1","unstructured":"Lennart Augustsson and Magnus Carlsson. 1999. An exercise in dependent types: A well-typed interpreter. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.39.2895&rep=rep1&type=pdf Unpublished manuscript.  Lennart Augustsson and Magnus Carlsson. 1999. An exercise in dependent types: A well-typed interpreter. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.39.2895&rep=rep1&type=pdf Unpublished manuscript."},{"key":"e_1_2_2_3_1","volume-title":"Term Rewriting and All That","author":"Baader Franz","unstructured":"Franz Baader and Tobias Nipkow . 1998. Term Rewriting and All That . Cambridge University Press . Franz Baader and Tobias Nipkow. 1998. Term Rewriting and All That. Cambridge University Press."},{"key":"e_1_2_2_4_1","volume-title":"ACM SIGPLAN Haskell Symposium.","author":"Bottu Gert-Jan","unstructured":"Gert-Jan Bottu and Richard A. Eisenberg . 2021. Seeking Stability by being Lazy and Shallow: Lazy and shallow instantiation is user friendly . In ACM SIGPLAN Haskell Symposium. Gert-Jan Bottu and Richard A. Eisenberg. 2021. Seeking Stability by being Lazy and Shallow: Lazy and shallow instantiation is user friendly. In ACM SIGPLAN Haskell Symposium."},{"key":"e_1_2_2_5_1","unstructured":"Luca Cardelli and Xavier Leroy. 1990. Abstract types and the dot notation. In IFIP TC2 working conference on programming concepts and methods. 479\u2013504.  Luca Cardelli and Xavier Leroy. 1990. Abstract types and the dot notation. In IFIP TC2 working conference on programming concepts and methods. 479\u2013504."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319847"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009892"},{"key":"e_1_2_2_8_1","volume-title":"Principal Type-schemes for Functional Programs. In Symposium on Principles of Programming Languages (POPL \u201982)","author":"Damas Luis","year":"1982","unstructured":"Luis Damas and Robin Milner . 1982 . Principal Type-schemes for Functional Programs. In Symposium on Principles of Programming Languages (POPL \u201982) . ACM. Luis Damas and Robin Milner. 1982. Principal Type-schemes for Functional Programs. In Symposium on Principles of Programming Languages (POPL \u201982). ACM."},{"key":"e_1_2_2_10_1","volume-title":"Complete and Easy Bidirectional Typechecking for Higher-rank Polymorphism. In International Conference on Functional Programming (ICFP \u201913)","author":"Dunfield Jana","unstructured":"Jana Dunfield and Neelakantan R. Krishnaswami . 2013 . Complete and Easy Bidirectional Typechecking for Higher-rank Polymorphism. In International Conference on Functional Programming (ICFP \u201913) . ACM. Jana Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and Easy Bidirectional Typechecking for Higher-rank Polymorphism. In International Conference on Functional Programming (ICFP \u201913). ACM."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290322"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3406088.3409015"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242753"},{"key":"e_1_2_2_15_1","volume-title":"Dependently Typed Programming with Singletons. In ACM SIGPLAN Haskell Symposium.","author":"Richard","unstructured":"Richard A. Eisenberg and Stephanie Weirich. 2012 . Dependently Typed Programming with Singletons. In ACM SIGPLAN Haskell Symposium. Richard A. Eisenberg and Stephanie Weirich. 2012. Dependently Typed Programming with Singletons. In ACM SIGPLAN Haskell Symposium."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227700"},{"key":"e_1_2_2_19_1","volume-title":"Pierce","author":"Harper Robert","year":"2005","unstructured":"Robert Harper and Benjamin C . Pierce . 2005 . Design Considerations for ML-Style Module Systems. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). The MIT Press , 293\u2013346. Robert Harper and Benjamin C. Pierce. 2005. Design Considerations for ML-Style Module Systems. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). The MIT Press, 293\u2013346."},{"key":"e_1_2_2_20_1","volume-title":"The Principal Type-Scheme of an Object in Combinatory Logic. Trans. Amer. Math. Soc., 146","author":"Hindley J. Roger","year":"1969","unstructured":"J. Roger Hindley . 1969. The Principal Type-Scheme of an Object in Combinatory Logic. Trans. Amer. Math. Soc., 146 ( 1969 ). J. Roger Hindley. 1969. The Principal Type-Scheme of an Object in Combinatory Logic. Trans. Amer. Math. Soc., 146 (1969)."},{"key":"e_1_2_2_21_1","volume-title":"The Formulae-as-types Notion of Construction. https:\/\/www.dcc.fc.up.pt\/~acm\/howard2.pdf Dedicated to H. B. Curry on the occasion of his 80th birthday","author":"Howard William Alvin","unstructured":"William Alvin Howard . 1969. The Formulae-as-types Notion of Construction. https:\/\/www.dcc.fc.up.pt\/~acm\/howard2.pdf Dedicated to H. B. Curry on the occasion of his 80th birthday . William Alvin Howard. 1969. The Formulae-as-types Notion of Construction. https:\/\/www.dcc.fc.up.pt\/~acm\/howard2.pdf Dedicated to H. B. Curry on the occasion of his 80th birthday."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/645389.651609"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001817"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186031"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/944746.944709"},{"key":"e_1_2_2_26_1","unstructured":"Daan Leijen. 2006. First-class polymorphism with existential types. Unpublished.  Daan Leijen. 2006. First-class polymorphism with existential types. Unpublished."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512670"},{"key":"e_1_2_2_28_1","volume-title":"Studies in Logic and the Foundations of Mathematics. 80","author":"Martin-L\u00f6f Per","unstructured":"Per Martin-L\u00f6f . 1975. An intuitionistic theory of types: Predicative part . In Studies in Logic and the Foundations of Mathematics. 80 , Elsevier , 73\u2013118. Per Martin-L\u00f6f. 1975. An intuitionistic theory of types: Predicative part. In Studies in Logic and the Foundations of Mathematics. 80, Elsevier, 73\u2013118."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628163"},{"key":"e_1_2_2_30_1","volume-title":"A Theory of Type Polymorphism in Programming. J. Comput. System Sci., 17","author":"Milner Robin","year":"1978","unstructured":"Robin Milner . 1978. A Theory of Type Polymorphism in Programming. J. Comput. System Sci., 17 ( 1978 ). Robin Milner. 1978. A Theory of Type Polymorphism in Programming. J. Comput. System Sci., 17 (1978)."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Stefan Monnier and David Haguenauer. 2010. Singleton types here singleton types there singleton types everywhere. In Programming languages meets program verification (PLPV \u201910). ACM.  Stefan Monnier and David Haguenauer. 2010. Singleton types here singleton types there singleton types everywhere. In Programming languages meets program verification (PLPV \u201910). ACM.","DOI":"10.1145\/1707790.1707792"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480926"},{"key":"e_1_2_2_34_1","volume-title":"Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory -","volume":"94","author":"Nakazawa Koji","year":"2009","unstructured":"Koji Nakazawa and Makoto Tatsuta . 2009 . Type Checking and Inference for Polymorphic and Existential Types . In Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94 (CATS \u201909). Australian Computer Society, Inc., AUS. 63\u201372. isbn:978 1920682750 Koji Nakazawa and Makoto Tatsuta. 2009. Type Checking and Inference for Polymorphic and Existential Types. In Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94 (CATS \u201909). Australian Computer Society, Inc., AUS. 63\u201372. isbn:9781920682750"},{"key":"e_1_2_2_35_1","volume-title":"Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence","author":"Nakazawa Koji","unstructured":"Koji Nakazawa , Makoto Tatsuta , Yukiyoshi Kameyama , and Hiroshi Nakano . 2008. Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence . In Computer Science Logic, Michael Kaminski and Simone Martini (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 478\u2013492. isbn:978-3-540-87531-4 Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano. 2008. Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence. In Computer Science Logic, Michael Kaminski and Simone Martini (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 478\u2013492. isbn:978-3-540-87531-4"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237729"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151632"},{"key":"e_1_2_2_40_1","volume-title":"LEAP: A language with eval and polymorphism. In TAPSOFT \u201989","author":"Pfenning Frank","year":"1989","unstructured":"Frank Pfenning and Peter Lee . 1989 . LEAP: A language with eval and polymorphism. In TAPSOFT \u201989 , J. D\u00edaz and F. Orejas (Eds.). Springer Berlin Heidelberg, Berlin , Heidelberg . 345\u2013359. isbn:978-3-540-46118-0 Frank Pfenning and Peter Lee. 1989. LEAP: A language with eval and polymorphism. In TAPSOFT \u201989, J. D\u00edaz and F. Orejas (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 345\u2013359. isbn:978-3-540-46118-0"},{"key":"e_1_2_2_41_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and Programming Languages . MIT Press , Cambridge, MA . Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, MA."},{"key":"e_1_2_2_42_1","volume-title":"Advanced Topics in Types and Programming Languages, Benjamin C","author":"Pottier Fran\u00e7ois","unstructured":"Fran\u00e7ois Pottier and Didier R\u00e9my . 2005. The Essence of ML Type Inference . In Advanced Topics in Types and Programming Languages, Benjamin C . Pierce (Ed.). The MIT Press , 387\u2013489. Fran\u00e7ois Pottier and Didier R\u00e9my. 2005. The Essence of ML Type Inference. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). The MIT Press, 387\u2013489."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784738"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408971"},{"key":"e_1_2_2_47_1","volume-title":"Simon Peyton Jones, and Kevin Donnelly","author":"Sulzmann Martin","year":"2007","unstructured":"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 \u201907). ACM. 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 \u201907). ACM."},{"key":"e_1_2_2_48_1","unstructured":"Ross Tate Juan Chen and Chris Hawblitzel. 2008. A Flexible Framework for Type Inference with Existential Quantification. https:\/\/www.microsoft.com\/en-us\/research\/publication\/a-flexible-framework-for-type-inference-with-existential-quantification\/  Ross Tate Juan Chen and Chris Hawblitzel. 2008. A Flexible Framework for Type Inference with Existential Quantification. https:\/\/www.microsoft.com\/en-us\/research\/publication\/a-flexible-framework-for-type-inference-with-existential-quantification\/"},{"key":"e_1_2_2_49_1","volume-title":"Refinement Types for Haskell. In International Conference on Functional Programming (ICFP \u201914)","author":"Vazou Niki","year":"2014","unstructured":"Niki Vazou , Eric L. Seidel , Ranjit Jhala , Dimitrios Vytiniotis , and Simon Peyton Jones . 2014 . Refinement Types for Haskell. In International Conference on Functional Programming (ICFP \u201914) . ACM. Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton Jones. 2014. Refinement Types for Haskell. In International Conference on Functional Programming (ICFP \u201914). ACM."},{"key":"e_1_2_2_50_1","doi-asserted-by":"crossref","unstructured":"Stephanie Weirich. 2018. Dependent Types in Haskell. Haskell eXchange keynote.  Stephanie Weirich. 2018. Dependent Types in Haskell. Haskell eXchange keynote.","DOI":"10.1145\/3341705"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_2_2_52_1","unstructured":"Hongwei Xi Chiyan Chen and Gang Chen. 2003. Guarded recursive datatype constructors. In Principles of Programming Languages (POPL \u201903). ACM.  Hongwei Xi Chiyan Chen and Gang Chen. 2003. Guarded recursive datatype constructors. In Principles of Programming Languages (POPL \u201903). ACM."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473569","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473569","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473569","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:15Z","timestamp":1750195695000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473569"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":47,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473569"],"URL":"https:\/\/doi.org\/10.1145\/3473569","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,19]]},"assertion":[{"value":"2021-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}