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
4 Typing Rules
In this section, we introduce the typing rules for Fun in Section 4.1 and for Core in Section 4.2. In Section 4.3 we state type soundness for both languages and prove that the translation from Fun to Core preserves the typeability of programs. We use the same constructors, destructors, types and typing contexts for both Fun and Core, which are summarized in Definition 4.1. Note that we distinguish between producer and consumer variables in the typing contexts, which we indicate with the prd and cns annotations.
We specialize the rules for data types to the concrete types Pair and List, and the rules for codata types to LPair, Stream and functions 𝜎 → 𝜏. A realistic programming language would use type declarations introduced by the programmer to typecheck data and codata types instead of using these special cases. But the formalization of such a general mechanism for specifying data and codata types makes the typing rules less readable. This kind of mechanism for specifying algebraic data and codata types in sequent-calculus-based languages can be found in [Downen et al. 2015] or [Downen and Ariola 2020, section 8]. In all of the typing rules below we assume that we have a program environment which contains type declarations for all the definitions contained in the program, but don’t explicitly thread this program environment through each of the typing rules.
4.1 Typing Rules for Fun
We don’t discuss the typing rules for Fun in detail since they are mostly standard. Instead, we provide the full rules in Appendix B. The language Fun only has one syntactic category, terms, so we only need one typing judgment Γ ⊢ 𝑡 : 𝜏. This typing judgment says that in the context Γ (which contains type assignments for both variables and covariables) the term 𝑡 has type 𝜏. The only two interesting rules concern the control operators label and goto:
In the rule Goto we require that the covariable 𝛼 is in the context with type 𝜏, and that the term 𝑡 can be typechecked with the same type. The term goto(𝑡; 𝛼) itself can be used at any type 𝜏 ′ because it does not return to its immediately surrounding context.
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.
