Table Of Links
2 DEPENDENTLY-TYPED OBJECT-ORIENTED PROGRAMMING
4 DESIGN CONSTRAINTS AND SOLUTIONS
RELATED WORK
Codata types. Codata types were first introduced by Hagino [Hagino 1987, 1989]. The original interpretation of codata types stems from coalgebras in category theory. An overview of the history of codata types as coalgebras is given by Setzer [Setzer 2012]. We have discussed the relation between codata types and OOP in Section 1.1. The expression problem. The expression problem poses the challenge for statically typed languages to create a type which can be extended by both new producers and new consumers. Based on earlier observations, Wadler [1998] formulated the problem and gave it its current name.
The expression problem for proofs is recognized as an important challenge in the verification community, but there are fewer proposed and implemented solutions than in the programming world. One popular solution in the programming world is Swierstra [2008]’s “Data Types à la carte” approach. In that approach, a type is defined as the fixpoint of a coproduct of functors which can be extended by new functors in a modular way. Most proposed solutions for dependent types are based on Swierstra [2008]’s approach and extend them to dependent types. Delaware et al. [2013a,b]; Delaware [2013] as well as Keuchel and Schrijvers [2013] implemented this approach for the Coq proof assistant and Schwaab and Siek [2013] implemented it for Agda.
A system for writing modular proofs in the Isabelle proof assistant has been described by Molitor [2015]. The most recent adaptation of the idea is by Forster and Stark [2020], who give an excellent presentation of this line of work in their related work section. In this article, our focus was not to propose a solution to the expression problem for proofs, since the defunctionalization and refunctionalization algorithms are whole-program transformations. Instead, our approach distills the essence of the expression problem for dependent types: Neither the functional nor the object-oriented decomposition solves the expression problem, since data types cannot be easily extended by new constructors, and codata types cannot be easily extended by new destructors.
Dependently-typed object-oriented programming. In Section 2 we presented our perspective on dependently-typed object-oriented programming. But we are not the first to think about this design space. Jacobs [1995] proposes using coalgebras to express object-oriented classes with coalgebraic specifications. His concept is based on three main components: objects, class implementations, and class specifications. The latter are used to specify a set of methods on an abstract state space as well as a set of assertions that define the behavior of these methods. Such a specification can then be implemented by a class.
A class gives a carrier set as a concrete interpretation for the state space and a coalgebra that implements the specified methods. An object is then just an element of the carrier set. In our system, we can express specifications similar to Jacobs’ proposal using self-parameters on destructors (see Section 2.2). Rather than having separate notions of specifications, classes, and objects, our system has a singular notion of codata types. Jacobs separates these notions to construct a model in which objects are indistinguishable if they are bisimilar according to their specification.
In contrast, in our system, we have a full syntactic duality between data and codata types through de- and refunctionalization. Hence, we need to decouple codata types from the semantics that are usually associated with them, including behavioral equality such as bisimilarity. Setzer [2006] conceived of dependently-typed object-oriented programming by specifying interfaces and having interactive programs as objects implementing these interfaces. The interfaces contain a command type, which represents the method signatures of an interface. Interactive programs are programs that react to incoming method calls by producing a return value and a new object.
Dependent type theories with definable Π-type and Σ-type. In Section 2.3 we demonstrated that the programmer can define both the Π-type and the Σ-type in our system, whereas in most proof assistants only the Σ-type can be defined. This is a generalization of the observation that programmers can’t define the function type in most functional programming languages, but that the function type can be defined in object-oriented languages [Setzer 2003]. Apart from this paper, the only other dependent type theory that doesn’t presuppose a built-in Π-type is by Basold [2018]; Basold and Geuvers [2016]. Like us, they give an explicit definition of the Π-type in their system.
Their definition, however, is slightly different from ours, since they have a more expressive core system. In their system, parameterized type constructors and type variables don’t have to be fully applied. Partially applied type constructors have a special type Γ _ ∗, and they specify a sort of simply-typed lambda calculus which governs the rules for abstracting over, and partially applying type constructors to arguments. As a result, their definition of the Π and Σ-type is a bit simpler: We have to use a previously-defined non-dependent function type 𝐴 → Type to represent the type family that the Σ and Π-types are indexed over, while they use a partially applied type variable 𝑋 : 𝐴 _ ∗. Our system is also not consistent; theirs is, and they prove both subject reduction and strong normalization.
Dependent pattern matching. The traditional primitive elimination forms in dependent type theories are eliminators. The eliminator for natural numbers, for example, has the type ∀(P : N → Type), P 0 → (∀n : N, P n → P (S n)) → ∀n : N, P n. They are suitable for studying the metatheory of dependent types, but programming with them isn’t very ergonomic. A more convenient alternative to eliminators is dependent pattern matching, a generalization of ordinary pattern matching to dependent types, which was first proposed by Coquand [1992].
While ordinary pattern matching can be compiled to eliminators and is therefore nothing more than syntactic sugar, the compilation of dependent pattern matches additionally requires Streicher [1993]’s axiom K. Hofmann and Streicher [1994] proved that this axiom does not follow from the standard elimination rules for the identity type. Since the K axiom is sometimes undesirable—it is incompatible with other principles such as univalence—a variant of dependent pattern matching which does not rely on axiom K was developed by Cockx et al. [2014]. We use a variant of dependent pattern and copattern matching which requires axiom K if we want to compile it to eliminators, but we could get rid of this dependency by applying the three restrictions presented in Cockx’ thesis [Cockx 2017, p.55].
Copattern matching. Copattern matching as a dual concept to pattern matching was first proposed by Abel et al. [2013]. Their work was motivated by the deficiencies of previous approaches which used constructors to represent infinite objects. For instance, the coinductive types originally introduced in Coq broke subject reduction, as noted by Giménez [1996] and Oury [2008]. Even simple infinite objects such as streams cannot be represented using constructors and pattern matching in a sensible way. This follows from the observation of Berger and Setzer [2018] that there exists no decidable equality for streams which admits a one-step expansion of a stream 𝑠 to a stream (cons 𝑛 𝑠′ ).
Inconsistent dependent type theories. The type theory presented in this paper is inconsistent, i.e. every type is inhabited by some term, a property it shares with most programming languages but not with proof assistants. However, the inconsistency of the theory does not imply that the properties expressed by the dependent types are meaningless. We can compare the situation to the programming language Haskell, where it is already possible to write dependent programs by using several language extensions and programming tricks [Eisenberg and Weirich 2012; Lindley and McBride 2013].
Instead of relying on these tricks, a more ergonomic and complete design of dependent types in Haskell has been the subject of various articles [Weirich et al. 2019, 2017] and PhD theses [Eisenberg 2016; Gundry 2013]. Their main insight also applies to our system: the central property of an inconsistent dependent type theory is type soundness [Wright and Felleisen 1994]. For example, every term of type Vec(5) can only evaluate to a vector containing five elements or diverge; it cannot evaluate to a vector of six elements. But they also show that inconsistency has downsides, especially for optimization: In a consistent theory every term of type Eq(𝑠, 𝑡) must evaluate to the term refl, and can therefore be erased during compilation. In an inconsistent theory, we cannot erase the equality witness, since we could otherwise write a terminating unsafe coercion between arbitrary types, which would violate type soundness.
Defunctionalization and refunctionalization. The related work on defunctionalization and refunctionalization can be partitioned into two groups: The first group only considers defunctionalization and refunctionalization for the function type, while the second group generalizes them to transformations between arbitrary data and codata types. De/Refunctionalization of the function type has a long history, which starts with the seminal paper by Reynolds [1972] and the later work of Danvy and Millikin [2009]; Danvy and Nielsen [2001]. That the defunctionalization of polymorphic functions requires GADTs was first observed by Pottier and Gauthier [2006].
In a recent paper, Huang and Yallop [2023] describe the defunctionalization of dependent functions, and especially how to correctly deal with type universes and positivity restrictions, but don’t consider the general case of indexed data and codata types. On the contrary, they do not use data types at all and instead introduce the construct of first-class function labels which enables them to avoid problems arising from the expressivity of data type definitions like recursive types. The generalization of defunctionalization from functions to arbitrary codata types was first described by Rendel et al. [2015] for a simply typed system without local lambda abstractions or local pattern matches.
That the generalization to polymorphic data and codata types then also requires GAcoDTs has been described by Ostermann and Jabs [2018]. How to treat local pattern and copattern matches in such a way as to preserve the invertibility of defunctionalization and refunctionalization has been described by Binder et al. [2019]. Recently, Zhang et al. [2022] implemented defunctionalization and refunctionalization for the programming language Scala, and used these transformations for some larger case studies. In this article, we describe the generalization to indexed data and codata types, but in distinction to Huang and Yallop [2023] we circumvent the problems of type universes and positivity restrictions by working in an inconsistent type theory.
CONCLUSION AND REFERENCES
Most dependently typed programming languages don’t support programming with codata as well as programming with data. The main reason some proof assistants support codata types at all was that some support was necessary for the convenient formalization of theorems about infinite and coalgebraic objects. But codata types are useful for more than just representing infinite objects like streams; they represent an orthogonal way to structure programs and proofs, with different extensibility properties and reasoning principles.
In this paper we have presented a vision of how programming can look in a dependently typed language in which the data and codata sides are completely symmetric and treated with equal care. By implementing this language and testing it on a case study we have demonstrated that this style of purely functional, dependently typed object-oriented programming does work. We think that this way of systematic language design, in place of ad-hoc extensions, provides a good case study on how the design of dependently typed languages and proof assistants should be approached.
DATA-AVAILABILITY STATEMENT
This article is accompanied by an online IDE available at polarity-lang.github.io/oopsla24 where the examples discussed in this paper can be selected and loaded. This online IDE consists of a static website hosted on GitHub pages, with all the code running in the browser on the client side. Should the hosted website despite our best efforts no longer be available, then it is possible to recreate it locally using the archived version available at Zenodo [Binder et al. 2024].
REFERENCES
Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. Copatterns: Programming Infinite Structures by Observations. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Rome, Italy) (POPL ’13). Association for Computing Machinery, New York, NY, USA, 27–38. https://doi.org/ 10.1145/2480359.2429075
Thorsten Altenkirch and Conor McBride. 2006. Towards Observational Type Theory. http://www.strictlypositive.org/ott. pdf Henning Basold. 2018. Mixed Inductive-Coinductive Reasoning: Types, Programs and Logic. Ph. D. Dissertation. Radboud University. https://hdl.handle.net/2066/190323
Henning Basold and Herman Geuvers. 2016. Type Theory Based on Dependent Inductive and Coinductive Types. In Proceedings of the Symposium on Logic in Computer Science (New York). Association for Computing Machinery, New York, NY, USA, 327–336. https://doi.org/10.1145/2933575.2934514 Ulrich Berger and Anton Setzer. 2018. Undecidability of Equality for Codata Types. In Coalgebraic Methods in Computer Science, Corina Cîrstea (Ed.). Springer, 34–55. https://doi.org/10.1007/978-3-030-00389-0_4
David Binder, Julian Jabs, Ingo Skupin, and Klaus Ostermann. 2019. Decomposition Diversity with Symmetric Data and Codata. Proc. ACM Program. Lang. 4, POPL, Article 30 (2019), 28 pages. https://doi.org/10.1145/3371098
David Binder, Ingo Skupin, Tim Süberkrüb, and Klaus Ostermann. 2024. Deriving Dependently-Typed OOP from First Principles. https://doi.org/10.5281/zenodo.10779424 Archived version of the submitted artefact.
Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. 2017. The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science 12 (April 2017). Issue 3. https://doi.org/10.2168/LMCS-12(3:7)2016
Jesper Cockx. 2017. Dependent Pattern Matching and Proof-Relevant Unification. Ph. D. Dissertation. KU Leuven.
Jesper Cockx, Dominique Devriese, and Frank Piessens. 2014. Pattern Matching without K. In International Conference on Functional Programming. Association for Computing Machinery, New York, NY, USA, 257–268. https://doi.org/10.1145/ 2628136.2628139
William R. Cook. 1990. Object-Oriented Programming versus Abstract Data Types. In Proceedings of the REX Workshop / School on the Foundations of Object-Oriented Languages. Springer, 151–178. https://doi.org/10.1007/BFb0019443
William R. Cook. 2009. On Understanding Data Abstraction, Revisited. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications: Onward! Essays (Orlando). Association for Computing Machinery, New York, NY, USA, 557–572. https://doi.org/10.1145/1640089.1640133
Thierry Coquand. 1992. Pattern Matching With Dependent Types. In Proceedings of the 1992 Workshop on Types for Proofs and Programs (Bastad, Sweden), Bengt Nordström, Kent Pettersson, and Gordon Plotkin (Eds.). 66–79.
Olivier Danvy and Kevin Millikin. 2009. Refunctionalization at Work. Science of Computer Programming 74, 8 (2009), 534–549. https://doi.org/10.1016/j.scico.2007.10.007
Olivier Danvy and Lasse R. Nielsen. 2001. Defunctionalization at Work. In Proceedings of the Conference on Principles and Practice of Declarative Programming (Florence). 162–174. https://doi.org/10.1145/773184.773202
Benjamin Delaware, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2013a. Meta-Theory à La Carte. In Symposium on Principles of Programming Languages (Rome) (POPL ’13). Association for Computing Machinery, New York, NY, USA, 207–218. https://doi.org/10.1145/2429069.2429094
Benjamin Delaware, Steven Keuchel, Tom Schrijvers, and Bruno C.d.S. Oliveira. 2013b. Modular Monadic Meta-Theory. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (Boston, Massachusetts, USA) (ICFP ’13). Association for Computing Machinery, New York, NY, USA, 319–330. https://doi.org/10.1145/2500365. 2500587
Benjamin James Delaware. 2013. Feature Modularity in Mechanized Reasoning. Ph. D. Dissertation. The University of Texas at Austin. Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. 2019. Codata in Action. In European Symposium on Programming (ESOP ’19). Springer, 119–146. https://doi.org/10.1007/978-3-030-17184-1_5
Richard Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. Ph. D. Dissertation. University of Pennsylvania.
Richard A. Eisenberg, Guillaume Duboc, Stephanie Weirich, and Daniel Lee. 2021. An Existential Crisis Resolved: Type Inference for First-Class Existential Types. Proc. ACM Program. Lang. 5, ICFP, Article 64 (aug 2021), 29 pages. https: //doi.org/10.1145/3473569
Richard A. Eisenberg and Stephanie Weirich. 2012. Dependently Typed Programming with Singletons. In Proceedings of the Haskell Symposium (Copenhagen, Denmark) (Haskell ’12). Association for Computing Machinery, New York, NY, USA, 117–130. https://doi.org/10.1145/2364506.2364522
Matthias Felleisen and Robert Hieb. 1992. The Revised Report on the Syntactic Theories of Sequential Control and State. Theoretical Computer Science 103, 2 (1992), 235–271. https://doi.org/10.1016/0304-3975(92)90014-7
Yannick Forster and Kathrin Stark. 2020. Coq à La Carte: A Practical Approach to Modular Syntax with Binders. In Proceedings of the Conference on Certified Programs and Proofs (New Orleans) (CPP 2020). Association for Computing Machinery, New York, NY, USA, 186–200. https://doi.org/10.1145/3372885.3373817
Peng Fu and Aaron Stump. 2014. Self Types for Dependently Typed Lambda Encodings. In International Conference on Rewriting Techniques and Applications, Gilles Dowek (Ed.). Springer, 224–239. https://doi.org/10.1007/978-3-319-08918- 8_16
Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. 1995. Design Patterns: Elements of Reusable Object-Oriented Software.
Addison-Wesley Publishing Co., Boston.
Richard Garner. 2009. On the Strength of Dependent Products in the Type Theory of Martin-Löf. Annals of Pure and Applied Logic 160, 1 (2009), 1–12. https://doi.org/10.1016/j.apal.2008.12.003
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–181. https://doi.org/3-540-45413-6_16
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.
Eduardo Giménez. 1996. Un Calcul de Constructions Infinies et son application a la vérification de systemes communicants. Ph. D. Dissertation. Lyon, École normale supérieure (sciences).
Jean-Yves Girard. 1972. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. Thése de Doctorat d’Etat. Université de Paris VII.
Brian Goetz et al. 2014. JSR 335: Lambda Expressions for the Java Programming Language. https://jcp.org/en/jsr/detail?id= 335
Adam Gundry. 2013. Type Inference, Haskell and Dependent Types. Ph. D. Dissertation. University of Strathclyde.
Tatsuya Hagino. 1987. A Categorical Programming Language. Ph. D. Dissertation. University of Edinburgh. https://doi. org/10.48550/arXiv.2010.05167
Tatsuya Hagino. 1989. Codatatypes in ML. Journal of Symbolic Computation 8, 6 (1989), 629–650. https://doi.org/10.1016/ S0747-7171(89)80065-3
Martin Hofmann. 1997. Syntax and Semantics of Dependent Types. In Extensional Constructs in Intensional Type Theory. Springer, London, 13–54. https://doi.org/10.1007/978-1-4471-0963-1_2
Martin Hofmann and Thomas Streicher. 1994. The Groupoid Model Refutes Uniqueness of Identity Proofs. In Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science. IEEE, 208–212. https://doi.org/10.1109/LICS.1994.316071
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.
Yulong Huang and Jeremy Yallop. 2023. Defunctionalization with Dependent Types. Proc. ACM Program. Lang. 7, PLDI, Article 127 (jun 2023), 23 pages. https://doi.org/10.1145/3591241
Antonius J. C. Hurkens. 1995. A Simplification of Girard’s Paradox. In Proceedings of the Conference on Typed Lambda Calculi and Applications. Springer, London, 266–278. http://dx.doi.org/10.1007/BFb0014058
Bart Jacobs. 1995. Objects and Classes, Coalgebraically. In Object Orientation with Parallelism and Persistence, Burkhard Freitag, Cliff B. Jones, Christian Lengauer, and Hans-Jörg Schek (Eds.). Springer, 83–103. https://doi.org/10.1007/978- 1-4613-1437-0_5
Steven Keuchel and Tom Schrijvers. 2013. Generic Datatypes à La Carte. In Workshop on Generic Programming (Boston) (WGP ’13). Association for Computing Machinery, New York, NY, USA, 13–24. https://doi.org/10.1145/2502488.2502491
Pieter Koopman, Rinus Plasmeijer, and Jan Martin Jansen. 2014. Church Encoding of Data Types Considered Harmful for Implementations: Functional Pearl. In Proceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages (IFL ’14). Association for Computing Machinery, New York, NY, USA, Article 4, 12 pages. https://doi.org/10.1145/2746325.2746330
Sam Lindley and Conor McBride. 2013. Hasochism: The Pleasure and Pain of Dependently Typed Haskell Programming. In Proceedings of the Haskell Symposium (Boston) (Haskell ’13). Association for Computing Machinery, New York, NY, USA, 81–92. https://doi.org/10.1145/2503778.2503786 Richard Molitor. 2015. Open Inductive Predicates. Master’s thesis. Karlsruher Institut für Technologie (KIT).
Hiroshi Nakano. 2000. A Modality for Recursion. In Proceedings of the Symposium on Logic in Computer Science. 255–266. https://doi.org/10.1109/LICS.2000.855774
Klaus Ostermann and Julian Jabs. 2018. Dualizing Generalized Algebraic Data Types by Matrix Transposition. In European Symposium on Programming. Springer, 60–85. https://doi.org/10.1007/978-3-319-89884-1_3
Nicolas Oury. 2008. Coinductive Types and Type Preservation. Message on the coq-club mailing list (2008). https://sympa. inria.fr/sympa/arc/coq-club/2008-06/msg00022.html
François Pottier and Nadji Gauthier. 2006. Polymorphic Typed Defunctionalization and Concretization. Higher-Order and Symbolic Computation 19, 1 (3 2006), 125–162. https://doi.org/10.1007/s10990-006-8611-7
Tillmann Rendel, Julia Trieflinger, and Klaus Ostermann. 2015. Automatic Refunctionalization to a Language with Copattern Matching: With Applications to the Expression Problem. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Vancouver, BC, Canada) (ICFP 2015). Association for Computing Machinery, New York, NY, USA, 269–279. https://doi.org/10.1145/2784731.2784763
John Charles Reynolds. 1972. Definitional Interpreters for Higher-Order Programming Languages. In ACMConf (Boston). Association for Computing Machinery, New York, NY, USA, 717–740. https://doi.org/10.1145/800194.805852
Christopher Schwaab and Jeremy G. Siek. 2013. Modular Type-Safety Proofs in Agda. In Proceedings of the 7th Workshop on Programming Languages Meets Program Verification (Rome, Italy) (PLPV ’13). Association for Computing Machinery, New York, NY, USA, 3–12. https://doi.org/10.1145/2428116.2428120
Anton Setzer. 2003. Java as a Functional Programming Language. In Types for Proofs and Programs, Herman Geuvers and Freek Wiedijk (Eds.). Springer, Berlin, Heidelberg, 279–298. https://doi.org/10.1007/3-540-39185-1_16
Anton Setzer. 2006. Object-Oriented Programming in Dependent Type Theory. Trends in Functional Programming 7 (2006), 91–108.
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öf, Peter Dybjer, Sten Lindström, Erik Palmgren, and Göran Sundholm (Eds.). Logic, Epistemology, and the Unity of Science, Vol. 27. Springer, Dordrecht, 351–369. https: //doi.org/10.1007/978-94-007-4435-6_16
Thomas Streicher. 1993. Investigations into Intensional Type Theory. Habilitationsschrift, Ludwig-Maximilians-Universität München. Wouter Swierstra. 2008. Data Types à la Carte. Journal of Functional Programming 18, 4 (2008), 423–436. https://doi.org/ 10.1017/S0956796808006758
Neil Tennant. 1982. Proof and Paradox. Dialectica 36, 2-3 (1982), 265–296. https://doi.org/10.1111/j.1746-8361.1982.tb00820.
x David Thibodeau, Andrew Cave, and Brigitte Pientka. 2016. Indexed Codata Types. In Proceedings of the International Conference on Functional Programming (Nara, Japan) (ICFP 2016). Association for Computing Machinery, New York, NY, USA, 351–363. https://doi.org/10.1145/2951913.2951929
Philip Wadler. 1998. The Expression Problem. (11 1998). https://homepages.inf.ed.ac.uk/wadler/papers/expression/ expression.txt Note to Java Genericity mailing list. S
tephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard A. Eisenberg. 2019. A Role for Dependent Types in Haskell. Proc. ACM Program. Lang. 3, ICFP, Article 101 (jul 2019), 29 pages. https://doi.org/10.1145/3341705
Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A. Eisenberg. 2017. A Specification for Dependent Types in Haskell. Proceedings of the ACM on Programming Languages 1, ICFP (8 2017). https://doi.org/ 10.1145/3110275
Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation 115, 1 (11 1994), 38–94. https://doi.org/10.1006/inco.1994.1093
Weixin Zhang, Cristina David, and Meng Wang. 2022. Decomposition Without Regret. arXiv preprint arXiv:2204.10411 (2022). https://doi.org/10.48550/ARXIV.2204.10411
This paper is