English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Data types and codata types are, as the names suggest, often seen as duals ofeach other. However, most programming languages do not support both of them intheir full generality, or if they do, they are still seen as distinctconstructs with separately defined type-checking, compilation, etc. Rendel etal. were the first to propose variants of two standard program transformations,de- and refunctionalization, as a test to gauge and improve the symmetrybetween data and codata types. However, in previous works, codata and data werestill seen as separately defined language constructs, with de- andrefunctionalization being defined as similar but separate algorithms. Theseworks also glossed over interactions between the aforementioned transformationsand evaluation order, which leads to a loss of desirable $\eta$ expansionequalities. We argue that the failure of complete symmetry is due to theinherent asymmetry of natural deduction as the logical foundation of thelanguage design. Natural deduction is asymmetric in that its focus is onproducers (proofs) of types, whereas consumers (contexts, continuations,refutations) have a second-class status. Inspired by existingsequent-calculus-based language designs, we present the first language designthat is fully symmetric in that the issues of polarity (data type vs codatatypes) and evaluation order (call-by-value vs call-by-name) are untangled andbecome independent attributes of a single form of type declaration. Bothattributes, polarity and evaluation order, can be changed independently by onealgorithm each. In particular, defunctionalization and refunctionalization arenow one algorithm. Evaluation order can be defined and changed individually foreach type, independently from polarity. By allowing only certain combinationsof evaluation order and polarity, the aforementioned $\eta$ laws can berestored.

Data-Codata Symmetry and its Interaction with Evaluation Order