File Download
Links for fulltext
(May Require Subscription)
- Publisher Website: 10.1145/3571211
- Scopus: eid_2-s2.0-85146575484
- WOS: WOS:000910847500018
Supplementary
- Citations:
- Appears in Collections:
Article: A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈
Title | A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈ |
---|---|
Authors | |
Keywords | extensibility polymorphism type systems |
Issue Date | 9-Jan-2023 |
Publisher | ACM |
Citation | Proceedings of the ACM on Programming Languages, 2023, v. 7, n. POPL, p. 515-543 How to Cite? |
Abstract | The typed merge operator offers the promise of a compositional style of statically-typed programming in which solutions to the expression problem arise naturally. This approach, dubbed compositional programming, has recently been demonstrated by Zhang et al. Unfortunately, the merge operator is an unwieldy beast. Merging values from overlapping types may be ambiguous, so disjointness relations have been introduced to rule out undesired nondeterminism and obtain a well-behaved semantics. Past type systems using a disjoint merge operator rely on intersection types, but extending such systems to include union types or overloaded functions is problematic: naively adding either reintroduces ambiguity. In a nutshell: the elimination forms of unions and overloaded functions require values to be distinguishable by case analysis, but the merge operator can create exotic values that violate that requirement. This paper presents F⋈, a core language that demonstrates how unions, intersections, and overloading can all coexist with a tame merge operator. The key is an underlying design principle that states that any two inhabited types can support either the deterministic merging of their values, or the ability to distinguish their values, but never both. To realize this invariant, we decompose previously studied notions of disjointness into two new, dual relations that permit the operation that best suits each pair of types. This duality respects the polarization of the type structure, yielding an expressive language that we prove to be both type safe and deterministic. |
Persistent Identifier | http://hdl.handle.net/10722/339349 |
ISI Accession Number ID |
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Rioux, Nick | - |
dc.contributor.author | Huang, Xuejing | - |
dc.contributor.author | Dos Santos Oliveira, Bruno C | - |
dc.contributor.author | Zdancewic, Steve | - |
dc.date.accessioned | 2024-03-11T10:35:54Z | - |
dc.date.available | 2024-03-11T10:35:54Z | - |
dc.date.issued | 2023-01-09 | - |
dc.identifier.citation | Proceedings of the ACM on Programming Languages, 2023, v. 7, n. POPL, p. 515-543 | - |
dc.identifier.uri | http://hdl.handle.net/10722/339349 | - |
dc.description.abstract | <p>The typed <em>merge operator</em> offers the promise of a compositional style of statically-typed programming in which solutions to the expression problem arise naturally. This approach, dubbed <em>compositional programming</em>, has recently been demonstrated by Zhang et al. </p><p>Unfortunately, the merge operator is an unwieldy beast. Merging values from overlapping types may be ambiguous, so <em>disjointness relations</em> have been introduced to rule out undesired nondeterminism and obtain a well-behaved semantics. Past type systems using a disjoint merge operator rely on intersection types, but extending such systems to include union types or overloaded functions is problematic: naively adding either reintroduces ambiguity. In a nutshell: the elimination forms of unions and overloaded functions require values to be distinguishable by case analysis, but the merge operator can create exotic values that violate that requirement. </p><p>This paper presents <em>F</em>⋈, a core language that demonstrates how unions, intersections, and overloading can all coexist with a tame merge operator. The key is an underlying design principle that states that any two inhabited types can support either the deterministic merging of their values, or the ability to distinguish their values, but never both. To realize this invariant, we decompose previously studied notions of disjointness into two new, dual relations that permit the operation that best suits each pair of types. This duality respects the polarization of the type structure, yielding an expressive language that we prove to be both type safe and deterministic.</p> | - |
dc.language | eng | - |
dc.publisher | ACM | - |
dc.relation.ispartof | Proceedings of the ACM on Programming Languages | - |
dc.rights | This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License. | - |
dc.subject | extensibility | - |
dc.subject | polymorphism | - |
dc.subject | type systems | - |
dc.title | A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈ | - |
dc.type | Article | - |
dc.description.nature | published_or_final_version | - |
dc.identifier.doi | 10.1145/3571211 | - |
dc.identifier.scopus | eid_2-s2.0-85146575484 | - |
dc.identifier.volume | 7 | - |
dc.identifier.issue | POPL | - |
dc.identifier.spage | 515 | - |
dc.identifier.epage | 543 | - |
dc.identifier.eissn | 2475-1421 | - |
dc.identifier.isi | WOS:000910847500018 | - |
dc.identifier.issnl | 2475-1421 | - |