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 6 Related Work The central ideas of the calculi that we have presented in this pearl are not novel: the 𝜆𝜇𝜇˜-calculus is by now over 20 years old. We chose a variant of this calculus that can be used as a starting point to explore all the variants that have been described in the literature. This related work section is therefore intended to provide suggestions for further reading and the chance to dive deeper into specific topics that we have only touched upon. 6.1 The Sequent Calculus 6.1 The Sequent Calculus The basis of our language Core is a term assignment system for the sequent calculus, an alternative logical system to natural deduction. The sequent calculus was originally introduced by Gentzen in the articles Gentzen [1935a,b, 1969]. For a more thorough introduction to the sequent calculus as a logical system, we can recommend the books by Negri and Von Plato [2001] and Troelstra and Schwichtenberg [2000] which introduce the sequent calculus and show how it differs from the natural deduction systems that are more commonly taught. 6.2 Term Assignment for the Sequent Calculus 6.2 Term Assignment for the Sequent Calculus The original article which introduced the 𝜆𝜇𝜇˜-calculus as a term assignment system for the sequent calculus was by Curien and Herbelin [2000]. Before we list some of the other articles, we should preface them with the following remark on notation: The reasons for this divergence are easily explained. The notation of Curien and Herbelin [2000] with its two contexts Γ and Δ perfectly illustrates the correspondence to the sequent calculus which operates with sequents Γ ⊢ Δ which contain multiple formulas on the left- and right-hand side of the turnstile. This close correspondence to the sequent calculus is less important for us. We found that splitting the context in this way often makes it more difficult to write down rules in their full generality when we extend the language with other features. Features which introduce a dependency of later bindings on earlier bindings within a typing context, for example when we add parametric polymorphism, don’t fit easily into the format of Curien and Herbelin [2000]. With these remarks out of the way, we can recommend the articles by Zeilberger [2008], Downen and Ariola [2014, 2018b, 2020], Munch-Maccagnoni [2009] and Spiwack [2014] which were very helpful to us when we learned about the 𝜆𝜇𝜇˜-calculus. 6.3 Codata Types 6.3 Codata Types Codata types were originally invented by Hagino [1989]. They had the most success in proof assistants such as Agda where they help circumvent certain technical problems that arise when we try to model coinductive types. Copattern matching as a way to create producers of codata types was popularized by Abel et al. [2013], although the basic idea of the concept had been around before that, see, e.g., [Zeilberger 2008]. But probably the best starting point to learn more about codata types is an article written by Downen et al. [2019]. 6.4 Control Operators and Classical Logic 6.4 Control Operators and Classical Logic The label/goto construct that we are using in Fun is an example of a control operator, of which Landin’s operator J [Felleisen 1987; Landin 1965; Thielecke 1998] likely is the oldest. Their translation into Core uses 𝜇-abstractions, which are also a form of control operator that was originally introduced by Parigot [1992] before it became a part of the 𝜆𝜇𝜇˜-calculus of Curien and Herbelin [2000]. Control operators have an important relationship to classical logic via the Curry-Howard isomorphism. This relationship was discovered by Griffin [1989]; a more thorough introduction can be found in Sørensen and Urzyczyn [2006]. 6.5 Different Evaluation Orders 6.5 Different Evaluation Orders We have already talked about the evaluation strategies call-by-value and call-by-name, and how their difference can be explained by different choices of how a critical pair should be evaluated. This duality between call-by-value and call-by-name has already been observed by Filinski [1989] and has been explored in more detail by Wadler [2003, 2005]. We have also seen in Section 5.6 how 𝜂-reduction only works with data types in call-by-value and with codata types in call-by-name. A lot of people therefore conclude that the choice of an evaluation order should maybe not be a global decision, but should instead depend on the type. This approach requires tracking the polarity of types and providing additional shift connectives which help mediate between the different evaluation orders; the article by Downen and Ariola [2018a] is a good entry point for pursuing these kinds of questions which are discussed in detail in [Zeilberger 2009] and [Munch-Maccagnoni 2013]. A well-known example of mixing evaluation orders is the call-by-push-value paradigm [Levy 1999] which distinguishes value types and computation types and subsumes both call-by-value and call-by-name. 7 Conclusion In this functional pearl, we have presented the 𝜆𝜇𝜇˜-calculus in the way we introduce it to our colleagues and students on the whiteboard; by compiling small examples of functional programs. We think this is a better way to introduce programming-language enthusiasts and compiler writers to the 𝜆𝜇𝜇˜-calculus, since it doesn’t require prior knowledge of the sequent calculus. We have also shown why we are excited about this calculus, by giving examples of how it allows us to express aspects like strict vs. lazy evaluation or compiler optimizations like case-of-case in an extremely clear way. We want to share our enthusiasm for the sequent calculus and languages built on it with more people, and with this pearl, we hope that others will start to write their own little compilers to the sequent calculus and explore the exciting possibilities it offers. Data Availability Statement Data Availability Statement This paper is accompanied by an implementation in Haskell. Upon acceptance and publication of this article, the implementation will be made available permanently using Zenodo. Acknowledgments Acknowledgments We would like to thank the anonymous reviewers and Paul Downen for their feedback which helped us greatly in improving the final presentation of the paper. 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.

What Sequent Calculus Teaches Us About Computation

Sequent Calculus vs CPS: A Compiler’s Perspective on Consumers and Evaluation Strategies

Read My Stories

Too Long; Didn't Read

Make resilience your competitive advantage

What Codata, Control Flow, and Logic Teach Us About Programming

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