-
Full Iso-recursive Types
Authors:
Litao Zhou,
Qianyong Wan,
Bruno C. d. S. Oliveira
Abstract:
There are two well-known formulations of recursive types: iso-recursive and equi-recursive types. Abadi and Fiore [1996] have shown that iso- and equi-recursive types have the same expressive power. However, their encoding of equi-recursive types in terms of iso-recursive types requires explicit coercions. These coercions come with significant additional computational overhead, and complicate reas…
▽ More
There are two well-known formulations of recursive types: iso-recursive and equi-recursive types. Abadi and Fiore [1996] have shown that iso- and equi-recursive types have the same expressive power. However, their encoding of equi-recursive types in terms of iso-recursive types requires explicit coercions. These coercions come with significant additional computational overhead, and complicate reasoning about the equivalence of the two formulations of recursive types.
This paper proposes a generalization of iso-recursive types called full iso-recursive types. Full iso-recursive types allow encoding all programs with equi-recursive types without computational overhead. Instead of explicit term coercions, all type transformations are captured by computationally irrelevant casts, which can be erased at runtime without affecting the semantics of the program. Consequently, reasoning about the equivalence between the two approaches can be greatly simplified. We present a calculus called $λ^μ_{Fi}$, which extends the simply typed lambda calculus (STLC) with full iso-recursive types. The $λ^μ_{Fi}$ calculus is proved to be type sound, and shown to have the same expressive power as a calculus with equi-recursive types. We also extend our results to subty**, and show that equi-recursive subty** can be expressed in terms of iso-recursive subty** with cast operators.
△ Less
Submitted 7 July, 2024; v1 submitted 30 June, 2024;
originally announced July 2024.
-
Direct Foundations for Compositional Programming
Authors:
Andong Fan,
Xue**g Huang,
Han Xu,
Yaozhu Sun,
Bruno C. d. S. Oliveira
Abstract:
The recently proposed CP language adopts Compositional Programming: a new modular programming style that solves challenging problems such as the Expression Problem. CP is implemented on top of a polymorphic core language with disjoint intersection types called Fi+. The semantics of Fi+ employs an elaboration to a target language and relies on a sophisticated proof technique to prove the coherence…
▽ More
The recently proposed CP language adopts Compositional Programming: a new modular programming style that solves challenging problems such as the Expression Problem. CP is implemented on top of a polymorphic core language with disjoint intersection types called Fi+. The semantics of Fi+ employs an elaboration to a target language and relies on a sophisticated proof technique to prove the coherence of the elaboration. Unfortunately, the proof technique is technically challenging and hard to scale to many common features, including recursion or impredicative polymorphism. Thus, the original formulation of Fi+ does not support the two later features, which creates a gap between theory and practice, since CP fundamentally relies on them.
This paper presents a new formulation of Fi+ based on a type-directed operational semantics (TDOS). The TDOS approach was recently proposed to model the semantics of languages with disjoint intersection types (but without polymorphism). Our work shows that the TDOS approach can be extended to languages with disjoint polymorphism and model the full Fi+ calculus. Unlike the elaboration semantics, which gives the semantics to Fi+ indirectly via a target language, the TDOS approach gives a semantics to Fi+ directly. With a TDOS, there is no need for a coherence proof. Instead, we can simply prove that the semantics is deterministic. The proof of determinism only uses simple reasoning techniques, such as straightforward induction, and is able to handle problematic features such as recursion and impredicative polymorphism. This removes the gap between theory and practice and validates the original proofs of correctness for CP. We formalized the TDOS variant of the Fi+ calculus and all its proofs in the Coq proof assistant.
△ Less
Submitted 12 May, 2022;
originally announced May 2022.
-
Resolution as Intersection Subty** via Modus Ponens
Authors:
Koar Marntirosian,
Tom Schrijvers,
Bruno C. d. S. Oliveira,
Georgios Karachalias
Abstract:
Resolution and subty** are two common mechanisms in programming languages. Resolution is used by features such as type classes or Scala-style implicits to synthesize values automatically from contextual type information. Subty** is commonly used to automatically convert the type of a value into another compatible type. So far the two mechanisms have been considered independently of each other.…
▽ More
Resolution and subty** are two common mechanisms in programming languages. Resolution is used by features such as type classes or Scala-style implicits to synthesize values automatically from contextual type information. Subty** is commonly used to automatically convert the type of a value into another compatible type. So far the two mechanisms have been considered independently of each other. This paper shows that, with a small extension, subty** with intersection types can subsume resolution. This has three main consequences. Firstly, resolution does not need to be implemented as a separate mechanism. Secondly, the interaction between resolution and subty** becomes apparent. Finally, the integration of resolution into subty** enables first-class (implicit) environments. The extension that recovers the power of resolution via subty** is the modus ponens rule of propositional logic. While it is easily added to declarative subty**, significant care needs to be taken to retain desirable properties, such as transitivity and decidability of algorithmic subty**, and coherence. To materialize these ideas we develop $λ_i^{\mathsf{MP}}$, a calculus that extends a iprevious calculus with disjoint intersection types, and develop its metatheory in the Coq theorem prover.
△ Less
Submitted 15 October, 2020; v1 submitted 13 October, 2020;
originally announced October 2020.
-
Kind Inference for Datatypes: Technical Supplement
Authors:
Ningning Xie,
Richard A. Eisenberg,
Bruno C. d. S. Oliveira
Abstract:
In recent years, languages like Haskell have seen a dramatic surge of new features that significantly extends the expressive power of their type systems. With these features, the challenge of kind inference for datatype declarations has presented itself and become a worthy research problem on its own.
This paper studies kind inference for datatypes. Inspired by previous research on type-inferenc…
▽ More
In recent years, languages like Haskell have seen a dramatic surge of new features that significantly extends the expressive power of their type systems. With these features, the challenge of kind inference for datatype declarations has presented itself and become a worthy research problem on its own.
This paper studies kind inference for datatypes. Inspired by previous research on type-inference, we offer declarative specifications for what datatype declarations should be accepted, both for Haskell98 and for a more advanced system we call PolyKinds, based on the extensions in modern Haskell, including a limited form of dependent types. We believe these formulations to be novel and without precedent, even for Haskell98. These specifications are complemented with implementable algorithmic versions. We study soundness, completeness and the existence of principal kinds in these systems, proving the properties where they hold. This work can serve as a guide both to language designers who wish to formalize their datatype declarations and also to implementors keen to have principled inference of principal types.
This technical supplement to Kind Inference for Datatypes serves to expand upon the text in the main paper. It contains detailed ty** rules, proofs, and connections to the Glasgow Haskell Compiler (GHC).
△ Less
Submitted 11 November, 2019;
originally announced November 2019.
-
Separating Use and Reuse to Improve Both
Authors:
Hrshikesh Arora,
Marco Servetto,
Bruno C. D. S. Oliveira
Abstract:
Context: Trait composition has inspired new research in the area of code reuse for object oriented (OO) languages. One of the main advantages of this kind of composition is that it makes possible to separate subty** from subclassing; which is good for code-reuse, design and reasoning. However, handling of state within traits is difficult, verbose or inelegant. Inquiry: We identify the this-leaki…
▽ More
Context: Trait composition has inspired new research in the area of code reuse for object oriented (OO) languages. One of the main advantages of this kind of composition is that it makes possible to separate subty** from subclassing; which is good for code-reuse, design and reasoning. However, handling of state within traits is difficult, verbose or inelegant. Inquiry: We identify the this-leaking problem as the fundamental limitation that prevents the separation of subty** from subclassing in conventional OO languages. We explain that the concept of trait composition addresses this problem, by distinguishing code designed for use (as a type) from code designed for reuse (i.e. inherited). We are aware of at least 3 concrete independently designed research languages following this methodology: TraitRecordJ, Package Templates and DeepFJig. Approach: In this paper, we design $42_μ$ a new language, where we improve use and reuse and support the This type and family polymorphism by distinguishing code designed for use from code designed for reuse. In this way $42_μ$ synthesise the 3 approaches above, and improves them with abstract state operations: a new elegant way to handle state composition in trait based languages. Knowledge and Grounding: Using case studies, we show that $42_μ$'s model of traits with abstract state operations is more usable and compact than prior work. We formalise our work and prove that type errors cannot arise from composing well typed code. Importance: This work is the logical core of the programming language 42. This shows that the ideas presented in this paper can be applicable to a full general purpose language. This form of composition is very flexible and could be used in many new languages.
△ Less
Submitted 1 February, 2019;
originally announced February 2019.
-
Extended Report: The Implicit Calculus
Authors:
Bruno C. d. S. Oliveira,
Tom Schrijvers,
Wontae Choi,
Wonchan Lee,
Kwangkeun Yi
Abstract:
Generic programming (GP) is an increasingly important trend in programming languages. Well-known GP mechanisms, such as type classes and the C++0x concepts proposal, usually combine two features: 1) a special type of interfaces; and 2) implicit instantiation of implementations of those interfaces.
Scala implicits are a GP language mechanism, inspired by type classes, that break with the traditio…
▽ More
Generic programming (GP) is an increasingly important trend in programming languages. Well-known GP mechanisms, such as type classes and the C++0x concepts proposal, usually combine two features: 1) a special type of interfaces; and 2) implicit instantiation of implementations of those interfaces.
Scala implicits are a GP language mechanism, inspired by type classes, that break with the tradition of coupling implicit instantiation with a special type of interface. Instead, implicits provide only implicit instantiation, which is generalized to work for any types. This turns out to be quite powerful and useful to address many limitations that show up in other GP mechanisms.
This paper synthesizes the key ideas of implicits formally in a minimal and general core calculus called the implicit calculus, and it shows how to build source languages supporting implicit instantiation on top of it. A novelty of the calculus is its support for partial resolution and higher-order rules (a feature that has been proposed before, but was never formalized or implemented). Ultimately, the implicit calculus provides a formal model of implicits, which can be used by language designers to study and inform implementations of similar mechanisms in their own languages.
△ Less
Submitted 20 March, 2012;
originally announced March 2012.
