{"id":1156515,"date":"2025-11-24T10:15:50","date_gmt":"2025-11-24T18:15:50","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-research-item&p=1156515"},"modified":"2026-02-23T11:06:05","modified_gmt":"2026-02-23T19:06:05","slug":"syntactic-implicit-parameters-with-static-overloading-extended-version","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/syntactic-implicit-parameters-with-static-overloading-extended-version\/","title":{"rendered":"Syntactic Implicit Parameters with Static Overloading (Extended Version)"},"content":{"rendered":"
Implicits provide a powerful mechanism for term-based inference, where
\n“obvious” arguments can be omitted and inferred by the type checker. This can
\ngreatly reduce the programmers burden and improve the clarity of expression. As
\nsuch, many languages support a form of implicits in practice, such as type
\nclasses in Haskell or Lean, or implicits in Scala. Unfortunately, many of these
\nsystems have become increasingly complex and often require significant
\nimplementation effort.<\/p>\n
In this paper we take a fresh look at the design space with an arguably simpler
\napproach based on two orthogonal features: _syntactic implicit parameters_ and
\n_static overloading_. Each of these features is limited in scope and has a
\nstraightforward implementation. Taken together though, they are surprisingly
\nexpresive and we believe they can cover many of the common usage scenarios of
\nimplicits in practice.<\/p>\n
We formalize our system and provide various examples, and prove our elaboration is
\ncoherent. We also give an inference algorithm and show it is sound and
\ncomplete. Our system is fully implemented in the Koka language, and we describe
\nour experience with these features at scale, and discuss further extensions.<\/p>\n","protected":false},"excerpt":{"rendered":"
Implicits provide a powerful mechanism for term-based inference, where “obvious” arguments can be omitted and inferred by the type checker. This can greatly reduce the programmers burden and improve the clarity of expression. As such, many languages support a form of implicits in practice, such as type classes in Haskell or Lean, or implicits in […]<\/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":"","msr_publisher_other":"","msr_booktitle":"","msr_chapter":"","msr_edition":"","msr_editors":"","msr_how_published":"","msr_isbn":"","msr_issue":"","msr_journal":"","msr_number":"MSR-TR-2025-56","msr_organization":"Microsoft","msr_pages_string":"","msr_page_range_start":"","msr_page_range_end":"","msr_series":"","msr_volume":"","msr_copyright":"","msr_conference_name":"","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-11-24","msr_highlight_text":"","msr_notes":"v5 (2026-02-23)","msr_longbiography":"","msr_publicationurl":"","msr_external_url":"","msr_secondary_video_url":"","msr_conference_url":"","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":[],"research-area":[13560],"msr-publication-type":[193718],"msr-publisher":[],"msr-focus-area":[],"msr-locale":[268875],"msr-post-option":[269148,269142],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-1156515","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-post-option-approved-for-river","msr-post-option-include-in-river"],"msr_publishername":"","msr_edition":"","msr_affiliation":"","msr_published_date":"2025-11-24","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-TR-2025-56","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"Microsoft","msr_how_published":"","msr_notes":"v5 (2026-02-23)","msr_highlight_text":"","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\/11\/implicits-tr-v5.pdf","id":"1162743","title":"implicits-tr-v5","label_id":"243109","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":1162743,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2025\/11\/implicits-tr-v5.pdf"},{"id":1159628,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2025\/11\/implicits-tr-v3.pdf"},{"id":1156981,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2025\/11\/implicits-tr-v2.pdf"},{"id":1156517,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2025\/11\/implicits-tr-v1.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":"Tim Whiting","user_id":0,"rest_url":false}],"msr_impact_theme":[],"msr_research_lab":[199565],"msr_event":[],"msr_group":[144812],"msr_project":[170943],"publication":[],"video":[],"msr-tool":[],"msr_publication_type":"techreport","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\/1156515","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":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/1156515\/revisions"}],"predecessor-version":[{"id":1156516,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/1156515\/revisions\/1156516"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=1156515"}],"wp:term":[{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=1156515"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=1156515"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=1156515"},{"taxonomy":"msr-publisher","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publisher?post=1156515"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=1156515"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=1156515"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=1156515"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=1156515"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=1156515"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=1156515"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=1156515"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=1156515"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}