{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T06:18:20Z","timestamp":1784182700750,"version":"3.55.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"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":["1704041"],"award-info":[{"award-number":["1704041"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Hong Kong Research Grant Council","award":["17210617, 17209519"],"award-info":[{"award-number":["17210617, 17209519"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>In recent years, languages like Haskell have seen a dramatic surge of new features that significantly extends the expressive power of their type systems. With these features, the challenge of kind inference for datatype declarations has presented itself and become a worthy research problem on its own. This paper studies kind inference for datatypes. Inspired by previous research on type-inference, we offer declarative specifications for what datatype declarations should be accepted, both for Haskell98 and for a more advanced system we call PolyKinds, based on the extensions in modern Haskell, including a limited form of dependent types. We believe these formulations to be novel and without precedent, even for Haskell98. These specifications are complemented with implementable algorithmic versions. We study soundness, completeness and the existence of principal kinds in these systems, proving the properties where they hold. This work can serve as a guide both to language designers who wish to formalize their datatype declarations and also to implementors keen to have principled inference of principal types.<\/jats:p>","DOI":"10.1145\/3371121","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Kind inference for datatypes"],"prefix":"10.1145","volume":"4","author":[{"given":"Ningning","family":"Xie","sequence":"first","affiliation":[{"name":"University of Hong Kong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Richard A.","family":"Eisenberg","sequence":"additional","affiliation":[{"name":"Bryn Mawr College, USA \/ Tweag I\/O, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bruno C. d. S.","family":"Oliveira","sequence":"additional","affiliation":[{"name":"University of Hong Kong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2021953.2021960"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.2307\/2269949"},{"key":"e_1_2_2_3_1","volume-title":"Bird and Lambert Meertens","author":"Richard","year":"1998"},{"key":"e_1_2_2_4_1","volume-title":"Simon Peyton Jones, and Stephanie Weirich","author":"Breitner Joachim","year":"2016"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086397"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951917"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_10"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/778559.778560"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535856"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_10"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676992"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90040-2"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47813-2_16"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36384-X_13"},{"key":"e_1_2_2_20_1","volume-title":"A tutorial implementation of dynamic pattern unification. Unpublished draft","author":"Gundry Adam","year":"2013"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863597.1863608"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/169701.169692"},{"key":"e_1_2_2_24_1","first-page":"29","article-title":"The principal type-scheme of an object in combinatory logic","volume":"146","author":"Hindley J. Roger","year":"1969","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237728"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001210"},{"key":"e_1_2_2_28_1","first-page":"22","volume-title":"Proceedings of the 1999 Haskell Workshop (Haskell \u201999)","author":"Jones Mark P.","year":"1999"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341706"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944709"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480891"},{"key":"e_1_2_2_32_1","unstructured":"Dale Miller. 1991. Unification of simply typed lambda-terms as logic programming. (1991).  Dale Miller. 1991. Unification of simply typed lambda-terms as logic programming. (1991)."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12925-1_41"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237729"},{"key":"e_1_2_2_35_1","volume-title":"Haskell 98 language and libraries: the revised report","author":"Jones Simon Peyton"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_2_2_38_1","volume-title":"The essence of ML type inference. Advanced Topics in Types and Programming Languages","author":"Pottier Fran\u00e7ois","year":"2005"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1577824.1577832"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411216"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596599"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192389"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180475.1180476"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411246"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341705"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500599"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"key":"e_1_2_2_50_1","volume-title":"Coercion Quantification. In Haskell Implementors\u2019 Workshop.","author":"Xie Ningnign","year":"2018"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103795"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784751"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371121","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371121","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371121","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371121"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":48,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371121"],"URL":"https:\/\/doi.org\/10.1145\/3371121","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}