{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,30]],"date-time":"2024-04-30T00:29:49Z","timestamp":1714436989701},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"\n The\n expression problem<\/jats:italic>\n describes how most types can easily be extended with new ways to\n produce<\/jats:italic>\n the type or new ways to\n consume<\/jats:italic>\n the type, but not both. When abstract syntax trees are defined as an algebraic data type, for example, they can easily be extended with new consumers, such as\n print<\/jats:italic>\n or\n eval<\/jats:italic>\n , but adding a new constructor requires the modification of all existing pattern matches. The expression problem is one way to elucidate the difference between functional or data-oriented programs (easily extendable by new consumers) and object-oriented programs (easily extendable by new producers). This difference between programs which are extensible by new producers or new consumers also exists for dependently typed programming, but with one core difference: Dependently-typed programming almost exclusively follows the functional programming model and not the object-oriented model, which leaves an interesting space in the programming language landscape unexplored. In this paper, we explore the field of dependently-typed object-oriented programming by\n deriving it from first principles<\/jats:italic>\n using the principle of duality. That is, we do not extend an existing object-oriented formalism with dependent types in an ad-hoc fashion, but instead start from a familiar data-oriented language and derive its dual fragment by the systematic use of defunctionalization and refunctionalization. Our central contribution is a dependently typed calculus which contains two dual language fragments. We provide type- and semantics-preserving transformations between these two language fragments: defunctionalization and refunctionalization. We have implemented this language and these transformations and use this implementation to explain the various ways in which constructions in dependently typed programming can be explained as special instances of the general phenomenon of duality.\n <\/jats:p>","DOI":"10.1145\/3649846","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"983-1009","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Deriving Dependently-Typed OOP from First Principles"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"http:\/\/orcid.org\/0000-0003-1272-0972","authenticated-orcid":false,"given":"David","family":"Binder","sequence":"first","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}]},{"ORCID":"http:\/\/orcid.org\/0000-0001-8320-8445","authenticated-orcid":false,"given":"Ingo","family":"Skupin","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}]},{"ORCID":"http:\/\/orcid.org\/0000-0001-8709-6321","authenticated-orcid":false,"given":"Tim","family":"S\u00fcberkr\u00fcb","sequence":"additional","affiliation":[{"name":"Aleph Alpha, Heidelberg, Germany"}]},{"ORCID":"http:\/\/orcid.org\/0000-0001-5294-5506","authenticated-orcid":false,"given":"Klaus","family":"Ostermann","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429075"},{"key":"e_1_2_2_2_1","unstructured":"Thorsten Altenkirch and Conor McBride. 2006. Towards Observational Type Theory. http:\/\/www.strictlypositive.org\/ott.pdf"},{"key":"e_1_2_2_3_1","volume-title":"Mixed Inductive-Coinductive Reasoning: Types, Programs and Logic. Ph. D. Dissertation","author":"Basold Henning","year":"2066","unstructured":"Henning Basold. 2018. Mixed Inductive-Coinductive Reasoning: Types, Programs and Logic. Ph. D. Dissertation. Radboud University. https:\/\/hdl.handle.net\/2066\/190323"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934514"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","unstructured":"Ulrich Berger and Anton Setzer. 2018. Undecidability of Equality for Codata Types. In Coalgebraic Methods in Computer Science Corina C\u00eerstea (Ed.). 34\u201355. https:\/\/doi.org\/10.1007\/978-3-030-00389-0_4 10.1007\/978-3-030-00389-0_4","DOI":"10.1007\/978-3-030-00389-0_4"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371098"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","unstructured":"David Binder Ingo Skupin Tim S\u00fcberkr\u00fcb and Klaus Ostermann. 2024. Deriving Dependently-Typed OOP from First Principles. https:\/\/doi.org\/10.5281\/zenodo.10779424 Archived version of the submitted artefact 10.5281\/zenodo.10779424","DOI":"10.5281\/zenodo.10779424"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","unstructured":"David Binder Ingo Skupin Tim S\u00fcberkr\u00fcb and Klaus Ostermann. 2024. Deriving Dependently-Typed OOP from First Principles \u2013 Extended Version with Additional Appendices. https:\/\/doi.org\/10.48550\/arXiv.2403.06707","DOI":"10.48550\/arXiv.2403.06707"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(3:7)2016"},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Jesper Cockx. 2017. Dependent Pattern Matching and Proof-Relevant Unification. Ph. D. Dissertation. KU Leuven.","DOI":"10.1145\/3018610.3018612"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628139"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0019443"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640133"},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of the 1992 Workshop on Types for Proofs and Programs, Bengt Nordstr\u00f6m, Kent Pettersson, and Gordon Plotkin (Eds.). 66\u201379","author":"Coquand Thierry","year":"1992","unstructured":"Thierry Coquand. 1992. Pattern Matching With Dependent Types. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, Bengt Nordstr\u00f6m, Kent Pettersson, and Gordon Plotkin (Eds.). 66\u201379."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.10.007"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/773184.773202"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429094"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500587"},{"key":"e_1_2_2_19_1","volume-title":"Feature Modularity in Mechanized Reasoning. Ph. D. Dissertation","author":"Delaware Benjamin James","unstructured":"Benjamin James Delaware. 2013. Feature Modularity in Mechanized Reasoning. Ph. D. Dissertation. The University of Texas at Austin."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_5"},{"key":"e_1_2_2_21_1","volume-title":"Dependent Types in Haskell: Theory and Practice. Ph. D. Dissertation","author":"Eisenberg Richard","unstructured":"Richard Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. Ph. D. Dissertation. University of Pennsylvania."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473569"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364522"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373817"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_16"},{"key":"e_1_2_2_27_1","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"Gamma Erich","year":"1995","unstructured":"Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. 1995. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Publishing Co., Boston."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.12.003"},{"key":"e_1_2_2_29_1","volume-title":"Induction Is Not Derivable in Second Order Dependent Type Theory","author":"Geuvers Herman","unstructured":"Herman Geuvers. 2001. Induction Is Not Derivable in Second Order Dependent Type Theory. In Typed Lambda Calculi and Applications, Samson Abramsky (Ed.). Springer, Berlin, Heidelberg. 166\u2013181. isbn:978-3-540-45413-7 https:\/\/doi.org\/3-540-45413-6_16"},{"key":"e_1_2_2_30_1","unstructured":"Herman Geuvers. 2014. The Church-Scott Representation of Inductive and Coinductive Data. https:\/\/www.cs.vu.nl\/~femke\/courses\/ep\/slides\/herman-data-types.pdf Presented at the TYPES 2014 meeting"},{"key":"e_1_2_2_31_1","unstructured":"Eduardo Gim\u00e9nez. 1996. Un Calcul de Constructions Infinies et son application a la v\u00e9rification de systemes communicants. Ph. D. Dissertation. Lyon \u00c9cole normale sup\u00e9rieure (sciences)."},{"key":"e_1_2_2_32_1","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Universit\u00e9 de Paris VII."},{"key":"e_1_2_2_33_1","unstructured":"Brian Goetz. 2014. JSR 335: Lambda Expressions for the Java Programming Language. https:\/\/jcp.org\/en\/jsr\/detail?id=335"},{"key":"e_1_2_2_34_1","volume-title":"Haskell and Dependent Types. Ph. D. Dissertation","author":"Gundry Adam","unstructured":"Adam Gundry. 2013. Type Inference, Haskell and Dependent Types. Ph. D. Dissertation. University of Strathclyde."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2010.05167"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80065-3"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0963-1_2"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316071"},{"key":"e_1_2_2_39_1","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Haskell Curry, Hindley B., Seldin J","author":"Howard William Alvin","unstructured":"William Alvin Howard. 1980. The Formulae-as-Types Notion of Construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Haskell Curry, Hindley B., Seldin J. Roger, and P. Jonathan (Eds.). Academic Press."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591241"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014058"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-1437-0_5"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2502488.2502491"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746330"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503786"},{"key":"e_1_2_2_46_1","volume-title":"Open Inductive Predicates. Master\u2019s thesis","author":"Molitor Richard","unstructured":"Richard Molitor. 2015. Open Inductive Predicates. Master\u2019s thesis. Karlsruher Institut f\u00fcr Technologie (KIT)."},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_3"},{"key":"e_1_2_2_49_1","unstructured":"Nicolas Oury. 2008. Coinductive Types and Type Preservation. Message on the coq-club mailing list https:\/\/sympa.inria.fr\/sympa\/arc\/coq-club\/2008-06\/msg00022.html"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8611-7"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784763"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2428116.2428120"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_16"},{"key":"e_1_2_2_55_1","first-page":"91","article-title":"Object-Oriented Programming in Dependent Type Theory","volume":"7","author":"Setzer Anton","year":"2006","unstructured":"Anton Setzer. 2006. Object-Oriented Programming in Dependent Type Theory. Trends in Functional Programming, 7 (2006), 91\u2013108.","journal-title":"Trends in Functional Programming"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","unstructured":"Anton Setzer. 2012. Coalgebras as Types Determined by Their Elimination Rules. In Epistemology versus Ontology. Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-L\u00f6f Peter Dybjer Sten Lindstr\u00f6m Erik Palmgren and G\u00f6ran Sundholm (Eds.) (Logic Epistemology and the Unity of Science Vol. 27). Springer Dordrecht. 351\u2013369. https:\/\/doi.org\/10.1007\/978-94-007-4435-6_16 10.1007\/978-94-007-4435-6_16","DOI":"10.1007\/978-94-007-4435-6_16"},{"key":"e_1_2_2_57_1","unstructured":"Thomas Streicher. 1993. Investigations into Intensional Type Theory. Habilitationsschrift Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1982.tb00820.x"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951929"},{"key":"e_1_2_2_61_1","unstructured":"Philip Wadler. 1998. The Expression Problem. 11 https:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/expression\/expression.txt Note to Java Genericity mailing list"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341705"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","unstructured":"Weixin Zhang Cristina David and Meng Wang. 2022. Decomposition Without Regret. arXiv preprint arXiv:2204.10411 https:\/\/doi.org\/10.48550\/ARXIV.2204.10411","DOI":"10.48550\/ARXIV.2204.10411"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649846","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:59:27Z","timestamp":1714413567000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649846"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":65,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649846"],"URL":"https:\/\/doi.org\/10.1145\/3649846","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}