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
5 Insights
In the previous section, we have explained what the πππΛ-calculus is, and how it works. Now that we know the what and how we can explain why this calculus is so interesting. This section is therefore a small collection of independent insights. To be clear, these insights are obvious to those who are deeply familiar with the πππΛ-calculus, but we can still recall how surprising they were for us when we first learned about them.
5.1 Evaluation Contexts are First Class
A central feature of the πππΛ-calculus is the treatment of evaluation contexts as first-class objects, as we have mentioned before. For example, consider the term (β2β β β3β) β β4β in Fun. When we want to evaluate this, we have to use the evaluation context β‘ β β4β to evaluate the subterm (β2β β β3β) and get β6β β β4β which we can then evaluate to β24β. Translating this term into Core gives ππΌ. β (ππ½. β (β2β, β3β; π½), β4β; πΌ). To evaluate this term, we first need to focus it giving
\ ππΌ.β¨ππ½. β (β2β, β3β; π½) | ππ₯. Λ β (π₯, β4β; πΌ)β©
\ When we now start evaluating with β, the steps are the same as in Fun. Using call-by-value, the π-abstraction is evaluated first, giving β(β2β, β3β; β(ππ₯. Λ β (π₯, β4β; β)). This now has the form where the product can be evaluated to β¨β6β | ππ₯. Λ β (π₯, β4β; β)β©, after which β6β is substituted for π₯. The term β(β6β, β4β; β) can then be directly evaluated to β24β.
\ After focusing, we can see how π½ is a variable that stands for the evaluation context in Fun. The term ππ₯. Λ β (π₯, β4β; πΌ) is the first-class representation of the evaluation context β‘ β β4β. We first evaluate the subexpression β(β2β, β3β; π½) and then insert the result into β(π₯, β4β; β) to finish the evaluation, as we did in Fun. In other words, the β‘ of an evaluation context in Fun, corresponds to a continuation π½ in Core, and similarly determines in which order subexpressions are evaluated.
5.2 Data is Dual to Codata
The sequent calculus clarifies the relation between data and codata as being exactly dual to each other. When looking at the typing rules in Figure 2, we can see that data and codata types are completely symmetric. The two are not symmetric in languages based on natural deduction: A pattern match on data types includes the scrutinee but there is no corresponding object in the construction of codata. Similarly, invoking a destructor π· of a codata type always includes the codata object π₯ to be destructed, e.g., π₯.π·(. . .), whereas the invocation of the constructor of a data type has no corresponding object.
\ This asymmetry is fixed in the sequent calculus. Destructors (such as fst) are first-class and donβt require a scrutinee, which repairs the symmetry to constructors. Similarly, pattern matches (case {. . .}) do not require an object to destruct, which makes them completely symmetrical to copattern matches. This duality reduces the conceptual complexity and opens the door towards shared design and implementation of features of data and codata types.
\
:::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.
:::
\
This content originally appeared on HackerNoon and was authored by Abstraction: Computer Science Discourse
Abstraction: Computer Science Discourse | Sciencx (2025-07-08T09:00:03+00:00) What Functional Programmers Can Learn from Sequent Calculus. Retrieved from https://www.scien.cx/2025/07/08/what-functional-programmers-can-learn-from-sequent-calculus/
Please log in to upload a file.
There are no updates yet.
Click the Upload button above to add an update.