At the heart of the Damas-Hindley-Milner (HM) type system lies
\nthe abstraction rule which derives a function type for a lambda expression.
\nIn this rule, the type of the parameter can be “guessed”, and can be any
\ntype that fits the derivation. The beauty of the HM system is that there always exists a most general type that
\nencompasses all possible derivations — Algorithm W is used to infer these most
\ngeneral types in practice.<\/p>\n
Unfortunately, this property is also the bane of the HM type rules. Many languages
\nextend HM typing with additional features which often require complex side
\nconditions to the type rules to maintain principal types. For example, various type systems for
\nimpredicative type inference, like HMF, FreezeML, or Boxy types, require
\nlet-bindings to always assign most general types. Such a restriction is difficult
\nto specify as a logical deduction rule though, as it ranges over all possible
\nderivations. Despite these complications, the actual implementations of various
\ntype inference algorithms are usually straightforward extensions of algorithm\\ W,
\nand from an implementation perspective, much of the complexity of various type
\nsystem extensions, like boxes or polymorphic weights, is in some sense
\nartificial.<\/p>\n
In this article we rephrase the HM type rules as _type inference under a
\nprefix_, called HMQ. HMQ is sound and complete with respect to the HM type
\nrules, but always derives principal types that correspond to the types inferred
\nby algorithm W. The HMQ type rules are close to the clarity of the declarative HM
\ntype rules, but also specific enough to “read off” an inference algorithm, and
\ncan form an excellent basis to describe type system extensions in practice.
\nWe show in particular how to describe the FreezeML and HMF systems in terms
\nof inference under a prefix, and how we no longer require complex side conditions.
\nWe also show a novel formalization of static overloading in HMQ as implemented
\nin Koka language.<\/p>\n","protected":false},"excerpt":{"rendered":"
At the heart of the Damas-Hindley-Milner (HM) type system lies the abstraction rule which derives a function type for a lambda expression. In this rule, the type of the parameter can be “guessed”, and can be any type that fits the derivation. The beauty of the HM system is that there always exists a most […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":null,"msr_publishername":"ACM","msr_publisher_other":"","msr_booktitle":"","msr_chapter":"","msr_edition":"","msr_editors":"","msr_how_published":"","msr_isbn":"","msr_issue":"","msr_journal":"","msr_number":"","msr_organization":"ACM SIGPLAN","msr_pages_string":"","msr_page_range_start":"1","msr_page_range_end":"24","msr_series":"","msr_volume":"","msr_copyright":"","msr_conference_name":"PLDI'25","msr_doi":"","msr_arxiv_id":"","msr_s2_paper_id":"","msr_mag_id":"","msr_pubmed_id":"","msr_other_authors":"","msr_other_contributors":"","msr_speaker":"","msr_award":"","msr_affiliation":"","msr_institution":"","msr_host":"","msr_version":"","msr_duration":"","msr_original_fields_of_study":"","msr_release_tracker_id":"","msr_s2_match_type":"","msr_citation_count_updated":"","msr_published_date":"2025-6-16","msr_highlight_text":"Distinguished Paper","msr_notes":"\"A Fresh Look at Static Overloading\". See also the accompanying technical report.","msr_longbiography":"","msr_publicationurl":"","msr_external_url":"","msr_secondary_video_url":"","msr_conference_url":"https:\/\/pldi25.sigplan.org\/","msr_journal_url":"","msr_s2_pdf_url":"","msr_year":0,"msr_citation_count":0,"msr_influential_citations":0,"msr_reference_count":0,"msr_s2_match_confidence":0,"msr_microsoftintellectualproperty":true,"msr_s2_open_access":false,"msr_s2_author_ids":[],"msr_pub_ids":[],"msr_hide_image_in_river":null,"footnotes":""},"msr-research-highlight":[246574],"research-area":[13560],"msr-publication-type":[193716],"msr-publisher":[],"msr-focus-area":[],"msr-locale":[268875],"msr-post-option":[269148,269142],"msr-field-of-study":[249202],"msr-conference":[260122],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-1139401","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-highlight-award","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-post-option-approved-for-river","msr-post-option-include-in-river","msr-field-of-study-programming-language"],"msr_publishername":"ACM","msr_edition":"","msr_affiliation":"","msr_published_date":"2025-6-16","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"","msr_chapter":"","msr_isbn":"","msr_journal":"","msr_volume":"","msr_number":"","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"ACM SIGPLAN","msr_how_published":"","msr_notes":"\"A Fresh Look at Static Overloading\". See also the accompanying technical report.","msr_highlight_text":"Distinguished Paper","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"file","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2025\/05\/principal.pdf","id":"1139402","title":"principal","label_id":"243109","label":0},{"type":"doi","viewUrl":"false","id":"false","title":"10.1145\/3729308","label_id":"243106","label":0}],"msr_related_uploader":"","msr_citation_count":0,"msr_citation_count_updated":"","msr_s2_paper_id":"","msr_influential_citations":0,"msr_reference_count":0,"msr_arxiv_id":"","msr_s2_author_ids":[],"msr_s2_open_access":false,"msr_s2_pdf_url":null,"msr_attachments":[{"id":1139664,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2025\/05\/principal-1.pdf"},{"id":1139402,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2025\/05\/principal.pdf"}],"msr-author-ordering":[{"type":"user_nicename","value":"Daan Leijen","user_id":31497,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=Daan Leijen"},{"type":"text","value":"Wenjia Ye","user_id":0,"rest_url":false}],"msr_impact_theme":[],"msr_research_lab":[199565],"msr_event":[1139118],"msr_group":[144812],"msr_project":[170943],"publication":[],"video":[],"msr-tool":[],"msr_publication_type":"inproceedings","related_content":{"projects":[{"ID":170943,"post_title":"Koka","post_name":"koka","post_type":"msr-project","post_date":"2012-04-13 08:38:42","post_modified":"2021-06-18 11:46:37","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/koka\/","post_excerpt":"Koka is a strongly typed functional-style language with effect types and handlers.","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170943"}]}}]},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/1139401","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":2,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/1139401\/revisions"}],"predecessor-version":[{"id":1139405,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/1139401\/revisions\/1139405"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=1139401"}],"wp:term":[{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=1139401"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=1139401"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=1139401"},{"taxonomy":"msr-publisher","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publisher?post=1139401"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=1139401"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=1139401"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=1139401"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=1139401"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=1139401"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=1139401"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=1139401"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=1139401"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}