{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:55:07Z","timestamp":1760043307814,"version":"3.41.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T00:00:00Z","timestamp":1503964800000},"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":[[2017,8,29]]},"abstract":"<jats:p>We present an approach to support partiality in type-level computation without compromising expressiveness or type safety. Existing frameworks for type-level computation either require totality or implicitly assume it. For example, type families in Haskell provide a powerful, modular means of defining type-level computation. However, their current design implicitly assumes that type families are total, introducing nonsensical types and significantly complicating the metatheory of type families and their extensions. We propose an alternative design, using qualified types to pair type-level computations with predicates that capture their domains. Our approach naturally captures the intuitive partiality of type families, simplifying their metatheory. As evidence, we present the first complete proof of consistency for a language with closed type families.<\/jats:p>","DOI":"10.1145\/3110286","type":"journal-article","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T18:19:41Z","timestamp":1504030781000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Constrained type families"],"prefix":"10.1145","volume":"1","author":[{"given":"J. Garrett","family":"Morris","sequence":"first","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard A.","family":"Eisenberg","sequence":"additional","affiliation":[{"name":"Bryn Mawr College, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633628.2633635"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_26"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000150"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086397"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190229"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535856"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_10"},{"volume-title":"Cambridge University Press","author":"Girard Jean-Yves","key":"e_1_2_2_9_1"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227700"},{"key":"e_1_2_2_11_1","unstructured":"Thomas Hallgren. 2000. Fun with functional dependencies or (draft) types as values in static computations in Haskell. http:\/\/www.cse.chalmers.se\/~hallgren\/Papers\/wm01.html . (2000).  Thomas Hallgren. 2000. Fun with functional dependencies or (draft) types as values in static computations in Haskell. http:\/\/www.cse.chalmers.se\/~hallgren\/Papers\/wm01.html . (2000)."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663086"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224198"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46425-5_15"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017488"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976002.2976018"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_25"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804320"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863596"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633362"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869489"},{"volume-title":"Proceedings of the 1997 workshop on Haskell (Haskell \u201997)","year":"1997","author":"Jones Simon Peyton","key":"e_1_2_2_23_1"},{"volume-title":"Proceedings of the 1st ACM SIGPLAN Symposium on Haskell, Haskell 2008","year":"2008","author":"Pucella Riccardo","key":"e_1_2_2_24_1"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411215"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061839"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_19"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804314"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_2_32_1","unstructured":"Mat\u00fa\u0161 Teji\u0161\u010d\u00e1k and Edwin Brady. 2015. Practical Erasure in Dependently Typed Languages. (2015). http:\/\/eb.host.cs. st- andrews.ac.uk\/drafts\/dtp- erasure- draft.pdf Draft.  Mat\u00fa\u0161 Teji\u0161\u010d\u00e1k and Edwin Brady. 2015. Practical Erasure in Dependently Typed Languages. (2015). http:\/\/eb.host.cs. st- andrews.ac.uk\/drafts\/dtp- erasure- draft.pdf Draft."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_2_2_34_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\/3110286","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3110286","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:38:44Z","timestamp":1750221524000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110286"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,29]]},"references-count":33,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2017,8,29]]}},"alternative-id":["10.1145\/3110286"],"URL":"https:\/\/doi.org\/10.1145\/3110286","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2017,8,29]]},"assertion":[{"value":"2017-08-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}