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
A. The Relationship to the Sequent Calculus
B. Typing Rules for Fun
C. Operational Semantics of label/goto
References
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
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
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
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
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
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
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
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.
