File Download
Supplementary
-
Citations:
- Appears in Collections:
postgraduate thesis: Taming intersection types and the merge operator
Title | Taming intersection types and the merge operator |
---|---|
Authors | |
Issue Date | 2023 |
Publisher | The University of Hong Kong (Pokfulam, Hong Kong) |
Citation | Huang, X. [黃雪晶]. (2023). Taming intersection types and the merge operator. (Thesis). University of Hong Kong, Pokfulam, Hong Kong SAR. |
Abstract | For modern programming languages, a systematic approach for establishing usability and
reliability is to first have a formalized and verified core language guarded by a type system.
This dissertation proposes a type-directed operational semantics (TDOS) approach to model
disjoint intersection types, and studies three calculi 𝜆𝑖, 𝜆𝑖+, and F𝑖+, serving as a new foundation
for Compositional Programming.
Compositional Programming is a recently proposed programming style. Its prototype
language CP supports multiple inheritance in a type-safe way and provides simple solutions
to modularity problems that are hard for conventional object-oriented programming and
functional programming languages. At the core of CP is F𝑖+ , a polymorphic calculus that
supports a symmetric merge operator with subtyping. The merge operator generalizes record
concatenation to any type, enabling expressive forms of object composition.
Due to its flexibility and ambiguity, the merge operator lacks a satisfying direct operational
semantics. Prior systems usually define the runtime semantics indirectly by elaborating the
source expressions into a target language. In contrast, the TDOS approach gives a semantics to
F𝑖+ directly. Besides being deterministic and type sound, the new calculus supports additional
features such as recursion and impredicative polymorphism.
As an essential part of the TDOS design, we show a novel algorithm for the subtyping of
intersection types with distributive laws. In this formulation, types that decompose into two
smaller parts are characterized by splittable types. This allows a simple proof of transitivity and
the modular addition of distributivity rules without pre-processing on types. We then extend
this idea to union types and present an algorithmic formulation of subtyping based on the
minimal relevant logic B+. |
Degree | Doctor of Philosophy |
Subject | Programming languages (Electronic computers) |
Dept/Program | Computer Science |
Persistent Identifier | http://hdl.handle.net/10722/325782 |
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Huang, Xuejing | - |
dc.contributor.author | 黃雪晶 | - |
dc.date.accessioned | 2023-03-02T16:32:47Z | - |
dc.date.available | 2023-03-02T16:32:47Z | - |
dc.date.issued | 2023 | - |
dc.identifier.citation | Huang, X. [黃雪晶]. (2023). Taming intersection types and the merge operator. (Thesis). University of Hong Kong, Pokfulam, Hong Kong SAR. | - |
dc.identifier.uri | http://hdl.handle.net/10722/325782 | - |
dc.description.abstract | For modern programming languages, a systematic approach for establishing usability and reliability is to first have a formalized and verified core language guarded by a type system. This dissertation proposes a type-directed operational semantics (TDOS) approach to model disjoint intersection types, and studies three calculi 𝜆𝑖, 𝜆𝑖+, and F𝑖+, serving as a new foundation for Compositional Programming. Compositional Programming is a recently proposed programming style. Its prototype language CP supports multiple inheritance in a type-safe way and provides simple solutions to modularity problems that are hard for conventional object-oriented programming and functional programming languages. At the core of CP is F𝑖+ , a polymorphic calculus that supports a symmetric merge operator with subtyping. The merge operator generalizes record concatenation to any type, enabling expressive forms of object composition. Due to its flexibility and ambiguity, the merge operator lacks a satisfying direct operational semantics. Prior systems usually define the runtime semantics indirectly by elaborating the source expressions into a target language. In contrast, the TDOS approach gives a semantics to F𝑖+ directly. Besides being deterministic and type sound, the new calculus supports additional features such as recursion and impredicative polymorphism. As an essential part of the TDOS design, we show a novel algorithm for the subtyping of intersection types with distributive laws. In this formulation, types that decompose into two smaller parts are characterized by splittable types. This allows a simple proof of transitivity and the modular addition of distributivity rules without pre-processing on types. We then extend this idea to union types and present an algorithmic formulation of subtyping based on the minimal relevant logic B+. | - |
dc.language | eng | - |
dc.publisher | The University of Hong Kong (Pokfulam, Hong Kong) | - |
dc.relation.ispartof | HKU Theses Online (HKUTO) | - |
dc.rights | The author retains all proprietary rights, (such as patent rights) and the right to use in future works. | - |
dc.rights | This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License. | - |
dc.subject.lcsh | Programming languages (Electronic computers) | - |
dc.title | Taming intersection types and the merge operator | - |
dc.type | PG_Thesis | - |
dc.description.thesisname | Doctor of Philosophy | - |
dc.description.thesislevel | Doctoral | - |
dc.description.thesisdiscipline | Computer Science | - |
dc.description.nature | published_or_final_version | - |
dc.date.hkucongregation | 2023 | - |
dc.identifier.mmsid | 991044649901903414 | - |