Why Arithmetic in Functional Languages Needs 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

2 Translating To Sequent Calculus

In this section, we introduce Fun, an expression-oriented functional programming language, together with its translation into the sequent-calculus-based intermediate language Core. We present both languages and the translation function [−] in multiple steps, starting with arithmetic expressions and adding more features in later subsections. We postpone the typing rules for both languages until Section 4.

2.1 Arithmetic Expressions

We begin with arithmetic expressions which consist of variables, integer literals, binary operators and ifz, a conditional expression which checks whether its first argument is equal to zero. The syntax of arithmetic expressions for Fun and Core is given in Definition 2.1.

In Fun there is only one syntactic category: terms𝑡. These terms can either be variables 𝑥, literals ⌜𝑛⌝, binary operators 𝑡 + 𝑡, 𝑡 ∗ 𝑡 and 𝑡 − 𝑡, or a conditional ifz(𝑡, 𝑡0, 𝑡1). This conditional evaluates to 𝑡0 if 𝑡 evaluates to ⌜0⌝, or to 𝑡1 otherwise. In contrast to this single category, Core uses three different syntactic categories: producers 𝑝, consumers 𝑐 and statements 𝑠. These categories are directly inherited from the 𝜆𝜇𝜇˜-calculus, and it is important to understand their differences:

Producers All constructs in Core which construct or produce an element of some type belong to the syntactic category of producers. In other words, producers correspond to “introduction forms” or “proof terms”, and every term of the language Fun is translated to a producer in Core.

Consumers Consumers are probably less intuitive than producers since they do not correspond directly to any term of the language Fun. The basic idea is that if some consumer𝑐 has type 𝜏, then 𝑐 consumes or destructs a producer of type 𝜏. If you have encountered evaluation contexts or continuations before, then it is helpful to think of consumers of type 𝜏 as continuations or evaluation contexts for a producer of type 𝜏. And if you are familiar with the Curry-Howard correspondence, then you can think of consumers as refutations or direct evidence that a proposition is false.

Statements Statements are the ingredient which make computation happen; without statements, we would only have static objects without any dynamic behavior. Here is a non-exhaustive list of examples for statements: Every IO action which reads from or prints to the console or a file should be represented as a statement in Core. Computations on primitive types such as machine integers should be statements. Finally, everything which is a redex in an expression-based language should also correspond to a statement in Core. Since statements themselves only compute and do not return anything they do not have a type.

After these general remarks, let us now look at how arithmetic expressions are represented in the language Core. Variables 𝑥 and literals ⌜𝑛⌝ both belong to the category of producers, but binary operators are represented as statements ⊙(𝑝1, 𝑝2;𝑐). First, let us explain why they are represented as statements instead of producers. The idea is that a binary operator on primitive integers has to be evaluated directly by the arithmetic logic unit (ALU) of the underlying machine. And any operation which directly invokes the machine should belong to the same syntactic category as a print or other IO instruction: statements. The machine does not return a result; rather, it reads inputs from registers and makes the result available in a register for further computation. This is also reflected in the second surprising aspect: the operator has three instead of two arguments. The two producers 𝑝1 and 𝑝2 correspond to the usual arguments, but the third consumer argument 𝑐 says what should happen to the result once the binary operator has been evaluated. This is similar to the continuation argument of a function in continuation-passing style. Binary operators ⊙(𝑝1, 𝑝2;𝑐) also display a syntactic convention we use: whenever some construct has arguments of different syntactic categories, we use a semicolon instead of a comma to separate them.

We can immediately see that the result of J𝑝1 + 𝑝2K should contain the statement +([𝑝1] [𝑝2]; ?), but we still have to figure out which consumer to plug in at the third-argument place, and how to convert this statement into a producer. We can do this with a 𝜇-abstraction in Core, which turns a statement into a producer while binding a covariable 𝛼: 𝜇𝛼. + ([𝑝1], [𝑝2]; 𝛼).

The statement ifz works similarly to binary operators: It is a computation which checks if the producer 𝑝 is zero and then continues with one of its two branches. These branches are also statements, indicating which computation to run after the condition has been evaluated. In the language Fun the two branches were terms, so we now have to find a way to transform two producers into two statements. We can do this by using a cut ⟨𝑝 | 𝑐⟩ which combines a producer and a consumer of the same type to obtain a statement in each branch: ifz([𝑡1], ⟨[𝑡2] | ? ⟩, ⟨[𝑡3] | ? ⟩). We can then use the same covariable 𝛼 in both statements to represent the fact that the we want the result in either branch to return to the same point in the program; we use a surrounding 𝜇-binding again to bind this covariable: 𝜇𝛼.ifz([𝑡1], ⟨[𝑡2] | 𝛼⟩, ⟨[𝑡3] | 𝛼⟩).

Let us now see how arithmetic expressions are evaluated. Definition 2.2 introduces the syntax of values and covalues, and shows how to reduce immediate redexes. We use a simple syntactic convention here: The metavariable for a value of terms𝑡 is 𝔱, the values of producers 𝑝 are written 𝔭 and the covalues which correspond to consumers𝑐 are written 𝔠. We use the symbol ⊲ for reduction in both Fun and Core (and write ⊲ ∗ when multiple steps are performed at once).

Values and the evaluation of redexes in Fun is straightforward, the only noteworthy aspect is that the two rules for ifz(·, 𝑡1, 𝑡2) do not require 𝑡1 and 𝑡2 to be values. Thus, let us proceed with the discussion of the language Core.

The first interesting aspect of the language Core is that there are both values and covalues. This can be explained by the role that values play in operational semantics: they specify the subset of terms that we are allowed to substitute for a variable. And since we have both variables which stand for producers and covariables which stand for consumers, we need both values and covalues as the respective subsets which we are allowed to substitute for a variable or covariable.

The second interesting aspect of the language Core is that only statements are reduced, not producers or consumers. This substantiates our remark from above that it is statements that introduce dynamism into the language by driving computation. It also contributes to the feeling that reduction in the language is close to the evaluation of an abstract machine and that the statements of Core correspond to the states of such an abstract machine.

We are still faced with a small problem when we want to show that a term of Fun evaluates to the same result as its translation into Core: We have only specified the reduction for statements but not for producers. We can easily solve this problem by introducing a special covariable ⋆ which acts as the “top-level” consumer of an evaluation. Using ⋆ we can then evaluate the statement ⟨[𝑡] | ⋆⟩ instead of the producer [𝑡].

Example 2.1. Consider the two terms ⌜2⌝ ∗ ⌜3⌝ and ifz(⌜2⌝, ⌜5⌝, ⌜10⌝) of Fun. Their respective translations into Core are 𝜇𝛼. ∗ (⌜2⌝, ⌜3⌝; 𝛼) and 𝜇𝛼.ifz(⌜2⌝, ⟨⌜5⌝ | 𝛼⟩, ⟨⌜10⌝ | 𝛼⟩). When we wrap them into a statement using the top-level continuation ⋆, we observe the following evaluation:

We have successfully evaluated the first term to the result ⌜6⌝ and the second term to the result ⌜10⌝.

In the following, we will often leave out the first reduction step in examples, thus silently replacing the covariable bound by the outermost 𝜇-binding with the top-level consumer ⋆.

Here is a bigger problem that we haven’t addressed yet. The evaluation rules in the present section do not allow to evaluate nested expressions like (⌜2⌝ ∗ ⌜4⌝) + ⌜5⌝ in Fun or its translation 𝜇𝛼. + (𝜇𝛽. ∗ (⌜2⌝, ⌜4⌝; 𝛽), ⌜5⌝; 𝛼) in Core. We will discuss this problem and its solution in more detail in Section 3.