What Functional Programmers Can Learn from Sequent Calculus

This article highlights five key insights from the πœ†πœ‡πœ‡Λœ-calculus, particularly the treatment of evaluation contexts as first-class and the restored symmetry between data and codata in sequent calculus. These features simplify reasoning and implementation in functional languages by clarifying evaluation order and reducing conceptual asymmetries in type systems.


This content originally appeared on HackerNoon and was authored by Abstraction: Computer Science Discourse

  1. Introduction

  2. Translating To Sequent Calculus

    2.1 Arithmetic Expressions

    2.2 Let Bindings

    2.3 Top-level Definitions

    2.4 Algebraic Data and Codata Types

    2.5 First-Class Functions

    2.6 Control Operators

  3. Evaluation Within a Context

    3.1 Evaluation Contexts for Fun

    3.2 Focusing on Evaluation in Core

  4. Typing Rules

    4.1 Typing Rules for Fun

    4.2 Typing Rules for Core

    4.3 Type Soundness

  5. Insights

    5.1 Evaluation Contexts are First Class

    5.2 Data is Dual to Codata

    5.3 Let-Bindings are Dual to Control Operators

    5.4 The Case-of-Case Transformation

    5.5 Direct and Indirect Consumers

    5.6 Call-By-Value, Call-By-Name and Eta-Laws

    5.7 Linear Logic and the Duality of Exceptions

  6. Related Work

  7. Conclusion, Data Availability Statement, and Acknowledgments

A. The Relationship to the Sequent Calculus

B. Typing Rules for Fun

C. Operational Semantics of label/goto

References

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


Print Share Comment Cite Upload Translate Updates
APA

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/

MLA
" » What Functional Programmers Can Learn from Sequent Calculus." Abstraction: Computer Science Discourse | Sciencx - Tuesday July 8, 2025, https://www.scien.cx/2025/07/08/what-functional-programmers-can-learn-from-sequent-calculus/
HARVARD
Abstraction: Computer Science Discourse | Sciencx Tuesday July 8, 2025 » What Functional Programmers Can Learn from Sequent Calculus., viewed ,<https://www.scien.cx/2025/07/08/what-functional-programmers-can-learn-from-sequent-calculus/>
VANCOUVER
Abstraction: Computer Science Discourse | Sciencx - » What Functional Programmers Can Learn from Sequent Calculus. [Internet]. [Accessed ]. Available from: https://www.scien.cx/2025/07/08/what-functional-programmers-can-learn-from-sequent-calculus/
CHICAGO
" » What Functional Programmers Can Learn from Sequent Calculus." Abstraction: Computer Science Discourse | Sciencx - Accessed . https://www.scien.cx/2025/07/08/what-functional-programmers-can-learn-from-sequent-calculus/
IEEE
" » What Functional Programmers Can Learn from Sequent Calculus." Abstraction: Computer Science Discourse | Sciencx [Online]. Available: https://www.scien.cx/2025/07/08/what-functional-programmers-can-learn-from-sequent-calculus/. [Accessed: ]
rf:citation
» What Functional Programmers Can Learn from Sequent Calculus | Abstraction: Computer Science Discourse | Sciencx | 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.

You must be logged in to translate posts. Please log in or register.