{"id":189350,"date":"2013-04-02T00:00:00","date_gmt":"2013-05-15T21:18:15","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/msr-research-item\/towards-algebra-oriented-programming\/"},"modified":"2016-08-10T07:18:05","modified_gmt":"2016-08-10T14:18:05","slug":"towards-algebra-oriented-programming","status":"publish","type":"msr-video","link":"https:\/\/www.microsoft.com\/en-us\/research\/video\/towards-algebra-oriented-programming\/","title":{"rendered":"Towards Algebra-Oriented Programming"},"content":{"rendered":"<div class=\"asset-content\">\n<p>Programs can be modularly decomposed in several dimensions. However, it has long been noted that existing programming languages typically suffer from \u201cthe tyranny of the dominant decomposition\u201d, only supporting decomposition of programs well in one dimension. Bad support for other dimensions leads to crosscutting concerns: code that logically represents some separate, modular functionality of the program, but which is not easily modularized. The main problem lies in existing programming language structuring abstractions, such as algebraic\/inductive datatypes in functional languages or object interfaces  in object-oriented languages, which dictate the particular flavor of modularity supported by the language.<\/p>\n<p>This talk suggests a form of algebraic signatures, which we generally refer to as algebras, as an alternative programming language structuring abstraction. Algebras do not dictate a particular modularity dimension on the programmer. Instead they support various composition operators which allow them to cater for several dimensions of modularity at once. Algebras have desirable properties of a programming abstraction: they support modular type-checking, separate-compilation and modular reasoning\/proofs. I will show how algebras can already be encoded in existing programming languages and theorem provers, and how they can help dealing with several practical problems: from modularizing DSL components, to modularizing inductive proofs and meta-theory of programming languages.  I&#8217;ll finish the talk by discussing some of the remaining challenges on creating truly algebra-oriented programming languages.<\/p>\n<\/div>\n<p><!-- .asset-content --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Programs can be modularly decomposed in several dimensions. However, it has long been noted that existing programming languages typically suffer from \u201cthe tyranny of the dominant decomposition\u201d, only supporting decomposition of programs well in one dimension. Bad support for other dimensions leads to crosscutting concerns: code that logically represents some separate, modular functionality of the [&hellip;]<\/p>\n","protected":false},"featured_media":197612,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr_hide_image_in_river":0,"footnotes":""},"research-area":[],"msr-video-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-session-type":[],"msr-impact-theme":[],"msr-pillar":[],"msr-episode":[],"msr-research-theme":[],"class_list":["post-189350","msr-video","type-msr-video","status-publish","has-post-thumbnail","hentry","msr-locale-en_us"],"msr_download_urls":"","msr_external_url":"https:\/\/youtu.be\/bdxQ-b03r8k","msr_secondary_video_url":"","msr_video_file":"","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/189350","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-video"}],"version-history":[{"count":0,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/189350\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/197612"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=189350"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=189350"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=189350"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=189350"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=189350"},{"taxonomy":"msr-session-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-session-type?post=189350"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=189350"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=189350"},{"taxonomy":"msr-episode","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-episode?post=189350"},{"taxonomy":"msr-research-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-theme?post=189350"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}