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 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. 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

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

Why Compiler Writers Care About Case-of-Case

How Typing Rules and Type Soundness Work in Core and Fun Programming Languages

Read My Stories

Too Long; Didn't Read

Make resilience your competitive advantage

What Functional Programmers Can Learn from Sequent Calculus

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

Untitled Story

Account Abstraction, Analysed: Abstract & Introduction

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

Account Abstraction, Analysed: Abstract & Introduction

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