{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:24:41Z","timestamp":1755998681641,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>\n            Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents\n            <jats:italic>match types<\/jats:italic>\n            , a type-level equivalent of pattern matching. Match types integrate seamlessly into programming languages with subtyping and, despite their simplicity, offer significant additional expressiveness. We formalize the feature of match types in a calculus based on System F sub and prove its soundness. We practically evaluate our system by implementing match types in the Scala 3 reference compiler, thus making type-level programming readily available to a broad audience of programmers.\n          <\/jats:p>","DOI":"10.1145\/3498698","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Type-level programming with match types"],"prefix":"10.1145","volume":"6","author":[{"given":"Olivier","family":"Blanvillain","sequence":"first","affiliation":[{"name":"EPFL, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9128-0391","authenticated-orcid":false,"given":"Jonathan Immanuel","family":"Brachth\u00e4user","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}]},{"given":"Maxime","family":"Kjaer","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}]},{"given":"Martin","family":"Odersky","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/103135.103138"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_14"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022243"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3317550.3321441"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_11"},{"key":"e_1_2_2_7_1","unstructured":"Olivier Blanvillain Jonathan Brachth\u00e4user Maxime Kjaer and Martin Odersky. 2021. Type-Level Programming with Match Types. 70. http:\/\/infoscience.epfl.ch\/record\/290019  Olivier Blanvillain Jonathan Brachth\u00e4user Maxime Kjaer and Martin Odersky. 2021. Type-Level Programming with Match Types. 70. http:\/\/infoscience.epfl.ch\/record\/290019"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5568850"},{"key":"e_1_2_2_9_1","unstructured":"Olivier Blanvillain Marios Iliofotou Adelbert Chang Gleb Kanterov and other open-source contributors. 2016\u20132021. Frameless. https:\/\/github.com\/typelevel\/frameless  Olivier Blanvillain Marios Iliofotou Adelbert Chang Gleb Kanterov and other open-source contributors. 2016\u20132021. Frameless. https:\/\/github.com\/typelevel\/frameless"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1013"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1090189.1086397"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3136000.3136001"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80490-0"},{"volume-title":"Dependent types in Haskell: Theory and practice","author":"Eisenberg Richard A","key":"e_1_2_2_14_1","unstructured":"Richard A Eisenberg . 2016. Dependent types in Haskell: Theory and practice . University of Pennsylvania . Richard A Eisenberg. 2016. Dependent types in Haskell: Theory and practice. University of Pennsylvania."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535856"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_14"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408996"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199475"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-020-2649-2"},{"key":"e_1_2_2_20_1","unstructured":"Austin Huang Sam Stites and Torsten Scholak. 2017\u20132021. HaskTorch. https:\/\/github.com\/hasktorch\/hasktorch  Austin Huang Sam Stites and Torsten Scholak. 2017\u20132021. HaskTorch. https:\/\/github.com\/hasktorch\/hasktorch"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706334"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017488"},{"key":"e_1_2_2_23_1","unstructured":"George Leontiev Eugene Burmako Jason Zaugg Adriaan Moors Paul Phillips Oron Port and Miles Sabin. 2014. SIP-23 - Literal-Based Singleton Types. https:\/\/docs.scala-lang.org\/sips\/42.type.html  George Leontiev Eugene Burmako Jason Zaugg Adriaan Moors Paul Phillips Oron Port and Miles Sabin. 2014. SIP-23 - Literal-Based Singleton Types. https:\/\/docs.scala-lang.org\/sips\/42.type.html"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2998392.2998401"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.25"},{"key":"e_1_2_2_26_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C.","year":"2091","unstructured":"Benjamin C. Pierce . 2002. Types and programming languages . MIT press . isbn:026216 2091 Benjamin C. Pierce. 2002. Types and programming languages. MIT press. isbn:0262162091"},{"key":"e_1_2_2_27_1","unstructured":"Michael Pilquist and Scodec open-source contributors. 2013\u20132021. Scodec. https:\/\/github.com\/scodec\/scodec  Michael Pilquist and Scodec open-source contributors. 2013\u20132021. Scodec. https:\/\/github.com\/scodec\/scodec"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133870"},{"key":"e_1_2_2_29_1","unstructured":"Alexander Rush. 2019. Tensor Considered Harmful. https:\/\/nlp.seas.harvard.edu\/NamedTensor  Alexander Rush. 2019. Tensor Considered Harmful. https:\/\/nlp.seas.harvard.edu\/NamedTensor"},{"key":"e_1_2_2_30_1","unstructured":"Miles Sabin and Shapeless open-source contributors. 2011\u20132021. Shapeless. https:\/\/github.com\/milessabin\/shapeless  Miles Sabin and Shapeless open-source contributors. 2011\u20132021. Shapeless. https:\/\/github.com\/milessabin\/shapeless"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411215"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325724"},{"key":"e_1_2_2_35_1","unstructured":"TypeScript development team. 2020. The TypeScript Handbook. https:\/\/www.typescriptlang.org\/  TypeScript development team. 2020. The TypeScript Handbook. https:\/\/www.typescriptlang.org\/"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926411"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133871"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_27"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498698","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498698","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498698"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":36,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498698"],"URL":"https:\/\/doi.org\/10.1145\/3498698","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}