What Functional Programmers Can Learn from Sequent Calculus

Table of Links

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.