Table of Links Introduction


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


Evaluation Within a Context
3.1 Evaluation Contexts for Fun
3.2 Focusing on Evaluation in Core


Typing Rules
4.1 Typing Rules for Fun
4.2 Typing Rules for Core
4.3 Type Soundness


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


Related Work


Conclusion, Data Availability Statement, and Acknowledgments Introduction Introduction Introduction Introduction 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 Translating To Sequent Calculus Translating To Sequent Calculus 2.1 Arithmetic Expressions 2.1 Arithmetic Expressions 2.2 Let Bindings 2.2 Let Bindings 2.3 Top-level Definitions 2.3 Top-level Definitions 2.4 Algebraic Data and Codata Types 2.4 Algebraic Data and Codata Types 2.5 First-Class Functions 2.5 First-Class Functions 2.6 Control Operators 2.6 Control Operators Evaluation Within a Context
3.1 Evaluation Contexts for Fun
3.2 Focusing on Evaluation in Core Evaluation Within a Context Evaluation Within a Context 3.1 Evaluation Contexts for Fun 3.1 Evaluation Contexts for Fun 3.2 Focusing on Evaluation in Core 3.2 Focusing on Evaluation in Core Typing Rules
4.1 Typing Rules for Fun
4.2 Typing Rules for Core
4.3 Type Soundness Typing Rules Typing Rules Typing Rules 4.1 Typing Rules for Fun 4.1 Typing Rules for Fun 4.2 Typing Rules for Core 4.2 Typing Rules for Core 4.3 Type Soundness 4.3 Type Soundness 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 Insights Insights 5.1 Evaluation Contexts are First Class 5.1 Evaluation Contexts are First Class 5.2 Data is Dual to Codata 5.2 Data is Dual to Codata 5.3 Let-Bindings are Dual to Control Operators 5.3 Let-Bindings are Dual to Control Operators 5.4 The Case-of-Case Transformation 5.4 The Case-of-Case Transformation 5.5 Direct and Indirect Consumers 5.5 Direct and Indirect Consumers 5.6 Call-By-Value, Call-By-Name and Eta-Laws 5.6 Call-By-Value, Call-By-Name and Eta-Laws 5.7 Linear Logic and the Duality of Exceptions 5.7 Linear Logic and the Duality of Exceptions Related Work Related Work Related Work Related Work Conclusion, Data Availability Statement, and Acknowledgments Conclusion, Data Availability Statement, and Acknowledgments Conclusion, Data Availability Statement, and Acknowledgments Conclusion, Data Availability Statement, and Acknowledgments A. The Relationship to the Sequent Calculus A. The Relationship to the Sequent Calculus B. Typing Rules for Fun B. Typing Rules for Fun C. Operational Semantics of label/goto C. Operational Semantics of label/goto References References 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(𝑦𝑠)} def case of 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(𝑥)} def cocase 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: 2.4.1 Data Types. def swap(𝑥) ≔ case 𝑥 of {Tup(𝑦, 𝑧) ⇒ Tup(𝑧, 𝑦)} def case of 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 Example 2.4. 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 2.4.2 Codata Types. 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. Example 2.5. 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. 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. Authors: 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. This paper is available on arxiv under CC BY 4.0 license. This paper is available on arxiv under CC BY 4.0 license. available on arxiv available on arxiv [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.

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

How Functional Languages Simulate Goto with Labels and μ-Bindings

How Let Bindings Improve Code Readability in Functional Programming

Read My Stories

Too Long; Didn't Read

Make resilience your competitive advantage

Understanding Algebraic Data and Codata Types in Functional Programming

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

Untitled Story

What Sequent Calculus Teaches Us About Computation

Rules of Thumb for Software Engineering

Building a cupboard

What is Code Review and Why We Need to Keep Doing It

How to Find the Stinky Parts of Your Code: 251 - Empty Collections

What Sequent Calculus Teaches Us About Computation

Rules of Thumb for Software Engineering

Building a cupboard

What is Code Review and Why We Need to Keep Doing It

How to Find the Stinky Parts of Your Code: 251 - Empty Collections

Light-Mode

Classic

Newspaper

Dark-Mode

Neon Noir

Minty

HN StartUps