This content originally appeared on HackerNoon and was authored by Abstraction: Computer Science Discourse
Table of Links
Translating To Sequent Calculus
Evaluation Within a Context
Insights
5.1 Evaluation Contexts are First Class
5.3 Let-Bindings are Dual to Control Operators
5.4 The Case-of-Case Transformation
5.5 Direct and Indirect Consumers
Conclusion, Data Availability Statement, and Acknowledgments
A. The Relationship to the Sequent Calculus
C. Operational Semantics of label/goto
2.4 Algebraic Data and Codata Types
We now extend Fun and Core with two new features: algebraic data and codata types. Algebraic data types are familiar from most typed functional programming languages. Algebraic codata types [Hagino 1989] are a little more unusual; they are defined by a set of observations or methods called destructors and are quite similar to interfaces in object-oriented programming [Cook 2009]. We introduce them both in the same section because they help to illustrate some of the deep theoretical dualities and symmetries of the sequent calculus and the 𝜆𝜇𝜇˜-calculus.
\ To get acquainted with our syntax, let us first briefly look at two short examples in Fun. The following definition calculates the sum over a List it receives as input.
\ def sum(𝑥) ≔ case 𝑥 of {Nil ⇒ ⌜0⌝, Cons(𝑦, 𝑦𝑠) ⇒ 𝑦 + sum(𝑦𝑠)}
\ It does so by pattern matching using the case … of {…} construct which is entirely standard. As an example of codata types, consider this definition:
\ def repeat(𝑥) ≔ cocase {hd ⇒ 𝑥, tl ⇒ repeat(𝑥)}
\ It constructs an infinite Stream whose elements are all the same as the input 𝑥 of the function. A Stream is defined by two destructors, hd yields the head of the stream and tl yields the remaining stream without the head. The stream is constructed by copattern matching [Abel et al. 2013] using the cocase {…} construct.
\
\
2.4.1 Data Types. Let us consider another example to better understand the general syntax:
\ def swap(𝑥) ≔ case 𝑥 of {Tup(𝑦, 𝑧) ⇒ Tup(𝑧, 𝑦)}
\
\ In Core, algebraic data types are mostly handled in the same way as in Fun. The main difference is that the scrutinee is no longer a part of a case expression. Instead, the case expression is a consumer and the scrutinee is a producer, which are then combined in a statement. This is exactly what is done in the translation. When a case and a constructor meet, there is an opportunity for computation, consuming the constructed term and continuing with the corresponding righthand side of the case expression. This also explains our terminology of producers and consumers. Constructors create, or in other words, produce data structures while cases destroy, or consume them.
\ There is another difference, however. Constructors in Core can now also take consumers as arguments which is not the case in Fun. An example of this is the negation type of a type 𝜏 which can be formulated as a data type with one constructor taking a consumer of type 𝜏 as an argument. A program making use of this type can be found in section 7.2 of Ostermann et al. [2022].
\ Fun is a call-by-value language which manifests itself in that a value of an algebraic data type consists of a constructor applied to other values. A case expression case 𝑡 of {. . .} can only be evaluated if the scrutinee 𝑡 is a value, so this means that it must be a constructor whose arguments are all values in the evaluation rule.
\ Evaluation in Core is done the same way, only with the scrutinee term changed to be the producer of a cut. Note that all consumers in Core are covalues (which is why the arguments of destructors in the definition of covalues are not in Fraktur font), so in order for a constructor term to be a value, only its producer arguments need to be values. This also means that the requirement for the consumer arguments of the constructor to be covalues is vacuously satisfied in the evaluation rule in Core.
\ Example 2.4. The translation of swap (including a simplification) is given by
\ def swap(𝑥; 𝛼) ≔ ⟨𝑥 | case {Tup(𝑦, 𝑧) ⇒ ⟨Tup(𝑧, 𝑦) | 𝛼⟩}⟩
\ Evaluating with an argument Tup(⌜2⌝, ⌜3⌝) and ⋆ then proceeds as we would expect
\ ⟨Tup(⌜2⌝, ⌜3⌝) | case {Tup(𝑦, 𝑧) ⇒ ⟨Tup(𝑧, 𝑦) | ⋆⟩}⟩ ⊲ ⟨Tup(⌜3⌝, ⌜2⌝) | ⋆⟩
\ 2.4.2 Codata Types. To illustrate the syntax for codata types further, consider the definition
\ def swap_lazy(𝑥) ≔ cocase {fst ⇒ 𝑥.snd, snd ⇒ 𝑥.fst}
\
\ For codata in Fun, the scrutinee is located in the destructor term instead of the cocase, inverse to data types. So now destructors are the consumers and cocases are the producers. This is mirrored in the translation which again separates the scrutinee, since in Core codata types and copattern matching are perfectly dual to data types and pattern matching.
\ All the destructors we have used here do not have producer parameters, but this is just due to the selection of examples. In the next section, we will see an example of a destructor with a producer parameter. Moreover, during the translation each destructor is endowed with an additional consumer parameter which again determines how execution continues after the destructor was invoked (and is thus bound by a surrounding 𝜇). For constructors this is not necessary, as we can use the same consumer variable directly in each branch of a case (similar to ifz[2]) because the scrutinee and the case are in the same expression. Destructors (and also constructors) in Core can even have more than one consumer parameter. An example of this is given in Section 5.7.
\ Evaluation is done analogous to data types, with the roles of cases and constructors reversed for cocases and destructors. Note, however, that for evaluation in Core the producer arguments of the destructor also have to be values, so it is not sufficient for the destructor to be a covalue (which it always is). We will come back to this subtlety in Section 3.
\ Example 2.5. Translating swap_lazy is done analogously to swap.
\ def swap_lazy(𝑥; 𝛼) ≔ ⟨cocase {fst(𝛽) ⇒ ⟨𝑥 | snd(𝛽)⟩, snd(𝛽) ⇒ ⟨𝑥 | fst(𝛽)⟩} | 𝛼⟩
\ Now take 𝑝 = cocase {fst(𝛼) ⇒ ⟨⌜1⌝ | 𝛼⟩, snd(𝛼) ⇒ ∗(⌜2⌝, ⌜3⌝; 𝛼)} and evaluate swap_lazy with snd to retrieve its first element:
\ swap_lazy(𝑝; snd(⋆)) ⊲ ⟨cocase {fst(𝛽) ⇒ ⟨𝑝 | snd(𝛽)⟩, snd(𝛽) ⇒ ⟨𝑝 | fst(𝛽)⟩} | snd(⋆)⟩
\ ⊲ ⟨𝑝 | fst(⋆)⟩ ⊲ ⟨⌜1⌝ | ⋆⟩
\ Because cocases are values regardless of their right-hand sides (in contrast to constructors), we can apply the destructor snd without first evaluating the product ∗(⌜2⌝, ⌜3⌝; 𝛼). For pairs, we could not do this, as Tup(⌜1⌝, ∗(⌜2⌝, ⌜3⌝; 𝛼)) is not a value, so its arguments have to be evaluated first. This is why this codata type is called lazy pair, as it allows to not evaluate its contents in contrast to regular pairs.
\ This section showed an important property of Core which does not hold for Fun. The data and codata types of Core are completely symmetric: the syntax for cases is the same as the syntax for cocases and the same is true for constructors and destructors. The reason for this deep symmetry is the same reason that makes the sequent calculus more symmetric than natural deduction, but in Definition 2.5 we can observe it in a programming language.
\
:::info Authors:
(1) David Binder, University of Tübingen, Germany;
(2) Marco Tzschentke, University of Tübingen, Germany;
(3) Marius Muller, University of Tübingen, Germany;
(4) Klaus Ostermann, University of Tübingen, Germany.
:::
:::info This paper is available on arxiv under CC BY 4.0 license.
:::
[2] We could have modelled ifz as a case, too, by modeling numbers as a data type. But since ifz corresponds to a machine instruction quite directly, it is natural to make it a statement, as explained in Section 2.1.
This content originally appeared on HackerNoon and was authored by Abstraction: Computer Science Discourse
Abstraction: Computer Science Discourse | Sciencx (2025-07-06T23:58:13+00:00) Understanding Algebraic Data and Codata Types in Functional Programming. Retrieved from https://www.scien.cx/2025/07/06/understanding-algebraic-data-and-codata-types-in-functional-programming/
Please log in to upload a file.
There are no updates yet.
Click the Upload button above to add an update.