{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:52:08Z","timestamp":1790927528036,"version":"4.1.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"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,10,31]]},"abstract":"<jats:p>Intersection and union types are becoming more popular by the day, entering the mainstream in programming languages like TypeScript and Scala 3. Yet, no language so far has managed to combine these powerful types with principal polymorphic type inference. We present a solution to this problem in MLstruct, a language with subtyped records, equirecursive types, first-class unions and intersections, class-based instance matching, and ML-style principal type inference. While MLstruct is mostly structurally typed, it contains a healthy sprinkle of nominality for classes, which gives it desirable semantics, enabling the expression of a powerful form of extensible variants that does not need row variables. Technically, we define the constructs of our language using conjunction, disjunction, and negation connectives, making sure they form a Boolean algebra, and we show that the addition of a few nonstandard but sound subtyping rules gives us enough structure to derive a sound and complete type inference algorithm. With this work, we hope to foster the development of better type inference for present and future programming languages with expressive subtyping systems.<\/jats:p>","DOI":"10.1145\/3563304","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T16:23:35Z","timestamp":1667233415000},"page":"449-478","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["MLstruct: principal type inference in a Boolean algebra of structural types"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8805-0728","authenticated-orcid":false,"given":"Lionel","family":"Parreaux","sequence":"first","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0323-6644","authenticated-orcid":false,"given":"Chun Yin","family":"Chau","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. 242\u2013252","author":"Abadi Martin","unstructured":"Martin Abadi and Marcelo P. Fiore . 1996. Syntactic considerations on recursive types . In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. 242\u2013252 . Martin Abadi and Marcelo P. Fiore. 1996. Syntactic considerations on recursive types. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. 242\u2013252."},{"key":"e_1_2_1_2_1","volume-title":"In CP96 Workshop on Set Constraints.","author":"Aiken Alexander","year":"1996","unstructured":"Alexander Aiken . 1996 . Making set-constraint program analyses scale . In In CP96 Workshop on Set Constraints. Alexander Aiken. 1996. Making set-constraint program analyses scale. In In CP96 Workshop on Set Constraints."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165188"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177847"},{"key":"e_1_2_1_5_1","volume-title":"d. S. Oliveira, and Zhiyuan Shi","author":"Alpuim Jo\u00e3o","year":"2017","unstructured":"Jo\u00e3o Alpuim , Bruno C. d. S. Oliveira, and Zhiyuan Shi . 2017 . Disjoint Polymorphism. In Programming Languages and Systems, Hongseok Yang (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg. 1\u201328. isbn:978-3-662-54434-1 Jo\u00e3o Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. 2017. Disjoint Polymorphism. In Programming Languages and Systems, Hongseok Yang (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1\u201328. isbn:978-3-662-54434-1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1086"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3546196.3550163"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2379036.2379037"},{"key":"e_1_2_1_12_1","volume-title":"Object-Oriented Programming A Unified Foundation","author":"Castagna Giuseppe","unstructured":"Giuseppe Castagna . 2012. Object-Oriented Programming A Unified Foundation . Springer Science & Business Media . Giuseppe Castagna. 2012. Object-Oriented Programming A Unified Foundation. Springer Science & Business Media."},{"key":"e_1_2_1_13_1","unstructured":"Giuseppe Castagna Victor Lanvin Micka\u00ebl Laurent and Kim Nguyen. 2021. Revisiting Occurrence Typing. arxiv:1907.05590. \t\t\t\t  Giuseppe Castagna Victor Lanvin Micka\u00ebl Laurent and Kim Nguyen. 2021. Revisiting Occurrence Typing. arxiv:1907.05590."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498674"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951928"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.29"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351259"},{"key":"e_1_2_1_21_1","unstructured":"Van Bakel Dezani-Ciancaglini S. Van Bakel M. Dezani-ciancaglini and Y. Motohama. 1998. The Minimal Relevant Logic and the Call-by-Value Lambda Calculus. \t\t\t\t  Van Bakel Dezani-Ciancaglini S. Van Bakel M. Dezani-ciancaglini and Y. Motohama. 1998. The Minimal Relevant Logic and the Call-by-Value Lambda Calculus."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009882"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364534"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/217838.217858"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029823"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391289.1391293"},{"key":"e_1_2_1_29_1","volume-title":"TAPSOFT \u201989","author":"Fuh You-Chin","unstructured":"You-Chin Fuh and Prateek Mishra . 1989. Polymorphic subtype inference: Closing the theory-practice gap . In TAPSOFT \u201989 , J. D\u00edaz and F. Orejas (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 167\u2013183. isbn:978-3-540-46118-0 You-Chin Fuh and Prateek Mishra. 1989. Polymorphic subtype inference: Closing the theory-practice gap. In TAPSOFT \u201989, J. D\u00edaz and F. Orejas (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 167\u2013183. isbn:978-3-540-46118-0"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90144-7"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004318"},{"key":"e_1_2_1_32_1","volume-title":"ML Workshop. 13","author":"Garrigue Jacques","year":"1998","unstructured":"Jacques Garrigue . 1998 . Programming with polymorphic variants . In ML Workshop. 13 , 7. Jacques Garrigue. 1998. Programming with polymorphic variants. In ML Workshop. 13, 7."},{"key":"e_1_2_1_33_1","unstructured":"Jacques Garrigue. 2001. Simple Type Inference for Structural Polymorphism.. In APLAS. 329\u2013343. \t\t\t\t  Jacques Garrigue. 2001. Simple Type Inference for Structural Polymorphism.. In APLAS. 329\u2013343."},{"key":"e_1_2_1_34_1","volume-title":"Jones","author":"Gaster Benedict R.","year":"1996","unstructured":"Benedict R. Gaster and Mark P . Jones . 1996 . A Polymorphic Type System for Extensible Records and Variants . Benedict R. Gaster and Mark P. Jones. 1996. A Polymorphic Type System for Extensible Records and Variants."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1040067315"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.2307\/1995158"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1053468.1053470"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473594"},{"key":"e_1_2_1_39_1","unstructured":"Trevor Jim and Jens Palsberg. 1999. Type Inference in Systems of Recursive Types With Subtyping. \t\t\t\t  Trevor Jim and Jens Palsberg. 1999. Type Inference in Systems of Recursive Types With Subtyping."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(05)80051-0"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80019-5"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/800017.800529"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276482"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-9942(199901\/03)5:1<35::AID-TAPO4>3.0.CO;2-4"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/218570.218572"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01212524"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409006"},{"key":"e_1_2_1_50_1","volume-title":"MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types (Extended Version)","author":"Parreaux Lionel","unstructured":"Lionel Parreaux and Chun Yin Chau . 2022. MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types (Extended Version) . The Hong Kong University of Science and Technology . https:\/\/lptk.github.io\/mlscript-paper Lionel Parreaux and Chun Yin Chau. 2022. MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types (Extended Version). The Hong Kong University of Science and Technology. https:\/\/lptk.github.io\/mlscript-paper"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7121838"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_21"},{"key":"e_1_2_1_55_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and programming languages . MIT press . Benjamin C. Pierce. 2002. Types and programming languages. MIT press."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/232627.232642"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289448"},{"key":"e_1_2_1_58_1","unstructured":"Fran\u00e7ois Pottier. 1998. Type Inference in the Presence of Subtyping: from Theory to Practice. INRIA. https:\/\/hal.inria.fr\/inria-00073205 \t\t\t\t  Fran\u00e7ois Pottier. 1998. Type Inference in the Presence of Subtyping: from Theory to Practice. INRIA. https:\/\/hal.inria.fr\/inria-00073205"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2963"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2003.1210073"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2022.25"},{"key":"e_1_2_1_62_1","volume-title":"Type Inference for Records in Natural Extension of ML","author":"R\u00e9my Didier","year":"2071","unstructured":"Didier R\u00e9my . 1994. Type Inference for Records in Natural Extension of ML . MIT Press , Cambridge, MA, USA . 67\u201395. isbn:026 2071 55X Didier R\u00e9my. 1994. Type Inference for Records in Natural Extension of ML. MIT Press, Cambridge, MA, USA. 67\u201395. isbn:026207155X"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4118-8_9"},{"key":"e_1_2_1_64_1","volume-title":"Type Inference with Structural Subtyping: A Faithful Formalization of an Efficient Constraint Solver","author":"Simonet Vincent","unstructured":"Vincent Simonet . 2003. Type Inference with Structural Subtyping: A Faithful Formalization of an Efficient Constraint Solver . In Programming Languages and Systems, Atsushi Ohori (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 283\u2013302. isbn:978-3-540-40018-9 Vincent Simonet. 2003. Type Inference with Structural Subtyping: A Faithful Formalization of an Efficient Constraint Solver. In Programming Languages and Systems, Atsushi Ohori (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 283\u2013302. isbn:978-3-540-40018-9"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73568"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328486"},{"key":"e_1_2_1_68_1","volume-title":"Subtyping constrained types","author":"Trifonov Valery","unstructured":"Valery Trifonov and Scott Smith . 1996. Subtyping constrained types . In Static Analysis, Radhia Cousot and David A. Schmidt (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 349\u2013365. isbn:978-3-540-70674-8 Valery Trifonov and Scott Smith. 1996. Subtyping constrained types. In Static Analysis, Radhia Cousot and David A. Schmidt (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 349\u2013365. isbn:978-3-540-70674-8"},{"key":"e_1_2_1_69_1","unstructured":"Leo White. 2015. Row polymorphism. https:\/\/www.cl.cam.ac.uk\/teaching\/1415\/L28\/rows.pdf \t\t\t\t  Leo White. 2015. Row polymorphism. https:\/\/www.cl.cam.ac.uk\/teaching\/1415\/L28\/rows.pdf"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563304","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563304","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T12:38:10Z","timestamp":1750163890000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563304"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":63,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563304"],"URL":"https:\/\/doi.org\/10.1145\/3563304","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}