{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:30:29Z","timestamp":1750221029582,"version":"3.41.0"},"reference-count":29,"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:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"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            Type family applications in Haskell must be fully saturated. This means that all type-level functions have to be first-order, leading to code that is both messy and longwinded. In this paper we detail an extension to GHC that removes this restriction. We augment Haskell\u2019s existing type arrow, |-&gt;|, with an\n            <jats:italic>unmatchable<\/jats:italic>\n            arrow, |\u00a0&gt;|, that supports partial application of type families without compromising soundness. A soundness proof is provided. We show how the techniques described can lead to substantial code-size reduction (circa 80%) in the type-level logic of commonly-used type-level libraries whilst simultaneously improving code quality and readability.\n          <\/jats:p>","DOI":"10.1145\/3341706","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Higher-order type-level programming in Haskell"],"prefix":"10.1145","volume":"3","author":[{"given":"Csongor","family":"Kiss","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Tony","family":"Field","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Susan","family":"Eisenbach","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Simon","family":"Peyton Jones","sequence":"additional","affiliation":[{"name":"Microsoft Research, UK"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"volume-title":"International Spring School on Datatype-Generic Programming","author":"Altenkirch Thorsten","key":"e_1_2_2_1_1","unstructured":"Thorsten Altenkirch , Conor McBride , and Peter Morris . 2006. Generic programming with dependent types . In International Spring School on Datatype-Generic Programming . Springer , 209\u2013257. Thorsten Altenkirch, Conor McBride, and Peter Morris. 2006. Generic programming with dependent types. In International Spring School on Datatype-Generic Programming. Springer, 209\u2013257."},{"key":"e_1_2_2_2_1","unstructured":"Maximilian C. Bolingbroke. 2011. Constraint Kinds for GHC. http:\/\/blog.omega- prime.co.uk\/2011\/09\/10\/constraint- kindsfor- ghc\/  Maximilian C. Bolingbroke. 2011. Constraint Kinds for GHC. http:\/\/blog.omega- prime.co.uk\/2011\/09\/10\/constraint- kindsfor- ghc\/"},{"key":"e_1_2_2_3_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_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086397"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062357"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633361"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535856"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_10"},{"key":"e_1_2_2_10_1","unstructured":"GHC. 2019. GHC User Manual on Type Families. https:\/\/downloads.haskell.org\/~ghc\/latest\/docs\/html\/users_guide\/ glasgow_exts.html#type- families Accessed: 2019-05-31.  GHC. 2019. GHC User Manual on Type Families. https:\/\/downloads.haskell.org\/~ghc\/latest\/docs\/html\/users_guide\/ glasgow_exts.html#type- families Accessed: 2019-05-31."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(73)90301-X"},{"key":"e_1_2_2_13_1","unstructured":"Chung-Kil Hur. 2010. Agda with the excluded middle is inconsistent? https:\/\/coq- club.inria.narkive.com\/iDuSeltD\/agdawith- the- excluded- middle- is- inconsistent . Accessed: 2019-03-01.  Chung-Kil Hur. 2010. Agda with the excluded middle is inconsistent? https:\/\/coq- club.inria.narkive.com\/iDuSeltD\/agdawith- the- excluded- middle- is- inconsistent . Accessed: 2019-03-01."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017488"},{"key":"e_1_2_2_15_1","volume-title":"Generic Deriving of Generic Traversals. In International Conference on Functional Programming (ICFP \u201918)","author":"Kiss Csongor","year":"2018","unstructured":"Csongor Kiss , Matthew Pickering , and Nicolas Wu . 2018 . Generic Deriving of Generic Traversals. In International Conference on Functional Programming (ICFP \u201918) . ACM. arXiv: arXiv:1805.06798 Csongor Kiss, Matthew Pickering, and Nicolas Wu. 2018. Generic Deriving of Generic Traversals. In International Conference on Functional Programming (ICFP \u201918). ACM. arXiv: arXiv:1805.06798"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604179"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863523.1863529"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"e_1_2_2_19_1","volume-title":"Haskell Implementors Workshop, St","author":"Nguyen My","year":"2018","unstructured":"My Nguyen . 2018 . Type-level visible type application. Talk , Haskell Implementors Workshop, St . Louis, MO, United States. My Nguyen. 2018. Type-level visible type application. Talk, Haskell Implementors Workshop, St. Louis, MO, United States."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581691"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180475.1180476"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804314"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_2_2_26_1","unstructured":"Anish Tondwalkar. 2018. Popularity of Haskell Extensions. https:\/\/gist.github.com\/atondwal\/ ee869b951b5cf9b6653f7deda0b7dbd8 . Accessed: 2019-02-24.  Anish Tondwalkar. 2018. Popularity of Haskell Extensions. https:\/\/gist.github.com\/atondwal\/ ee869b951b5cf9b6653f7deda0b7dbd8 . Accessed: 2019-02-24."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500599"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341705"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926411"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103795"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341706","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341706","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\/3341706"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":29,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341706"],"URL":"https:\/\/doi.org\/10.1145\/3341706","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"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"}}]}}