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 3.2 Focusing on Evaluation in Core Let us now come back to the problem in Core and find a solution for the stuck term 𝜇𝛼. + (𝜇𝛽. ∗ (⌜2⌝, ⌜4⌝; 𝛽), ⌜5⌝; 𝛼). We know that we have to evaluate 𝜇𝛽. ∗ (⌜2⌝, ⌜4⌝; 𝛽) next and then somehow plug the intermediate result into the hole [·] in the producer 𝜇𝛼. + ( [·], ⌜5⌝; 𝛼). If we give the intermediate result the name 𝑥 and play around with cuts, 𝜇-bindings and 𝜇˜ bindings, we might discover that we can recombine all these parts in the following way: 𝜇𝛼.⟨𝜇𝛽. ∗ (⌜2⌝, ⌜4⌝; 𝛽) | 𝜇𝑥. ˜ + (𝑥, ⌜5⌝; 𝛼)⟩ his term looks a bit mysterious, but the transformation corresponds roughly to what happens when we translate the term let 𝑥 = 2 ∗ 4 in 𝑥 + 5 instead of (2 ∗ 4) + 5 into Core. That is, we have lifted a subcomputation to the outside of the term we are evaluating. This kind of transformation is called focusing [Andreoli 1992; Curien and Munch-Maccagnoni 2010] and we use it to solve the problem with stuck terms in Core. We can see that it worked in our example because the term now fully evaluates to its normal form. Example 3.1. The producer 𝜇𝛼.⟨𝜇𝛽. ∗ (⌜2⌝, ⌜4⌝; 𝛽) | 𝜇𝑥. ˜ + (𝑥, ⌜5⌝; 𝛼)⟩ reduces as follows: Example ⟨𝜇𝛽. ∗ (⌜2⌝, ⌜4⌝; 𝛽) | 𝜇𝑥. ˜ + (𝑥, ⌜5⌝; ⋆)⟩ ⊲ ∗(⌜2⌝, ⌜4⌝; 𝜇𝑥. ˜ + (𝑥, ⌜5⌝; ⋆)) ⊲ ⟨⌜8⌝ | 𝜇𝑥. ˜ + (𝑥, ⌜5⌝; ⋆)⟩ ⊲ +(⌜8⌝, ⌜5⌝; ⋆) ⊲ ⟨⌜13⌝ | ⋆⟩ Once we have settled on focusing, we have another choice to make: Do we want to use this trick during the evaluation of a statement or as a preprocessing step before we start with the evaluation? These two alternatives are called dynamic and static focusing. Dynamic Focusing With dynamic focusing [Wadler 2003] we add additional evaluation rules, usually called 𝜍-rules, to lift sub-computations to the outside of the statement we are evaluating. Dynamic Focusing Static Focusing For static focusing [Curien and Herbelin 2000] we perform a transformation on the code before we start evaluating it. This results in a focused normal form which is a subset of the syntax of Core that we have described so far. Static Focusing Core Dynamic focusing is great for reasoning about the meaning of programs, but static focusing is more efficient if we are interested in compiling and running programs. For this reason, we only consider static focusing in what follows. The complete rules for static focusing are presented in Definition 3.2. Most of these rules are only concerned with performing the focusing transformation on all subexpressions, but some of the clauses where something interesting happens are the clauses for binary operators: The first two clauses look for the arguments of the binary operator ⊙ which are not values and use the trick described above to lift them to the outside. Focusing is invoked recursively until the binary operator is only applied to values and the third clause comes into play. This third clause then applies the focusing transformation to all arguments of the binary operator. The clauses for constructors, destructors, ifz and calls to top-level definitions work in precisely the same way as those for binary operators. It is noteworthy that by focusing the producer arguments of destructors we guarantee that the evaluation rule for codata types can fire. If we had not required the producer arguments to be values in that rule (but only that the destructor is a covalue), we could easily introduce an unfocused term again by substituting a non-value for a variable. The focusing transformation described in Definition 3.2 is not ideal since it creates a lot of administrative redexes. As an example, consider how the statement defining mult’ from Example 2.7 is focused: F (⟨𝑙 | case {Nil ⇒ ⟨1 | 𝛽⟩, Cons(𝑥, 𝑥𝑠) ⇒ ifz(𝑥, ⟨0 | 𝛼⟩, ∗(𝑥, 𝜇𝛾 .mult’(𝑥𝑠; 𝛼,𝛾); 𝛽))}⟩) = ⟨𝑙 | case {Nil ⇒ ⟨1 | 𝛽⟩, Cons(𝑥, 𝑥𝑠) ⇒ ifz(𝑥, ⟨0 | 𝛼⟩, ⟨𝜇𝛾 .mult’(𝑥𝑠; 𝛼,𝛾) | 𝜇𝑧. ˜ ∗ (𝑥, 𝑧; 𝛽)⟩)}⟩ Focusing has introduced the administrative redex ⟨𝜇𝛾 .mult’(𝑥𝑠; 𝛼,𝛾) | 𝜇𝑧. ˜ ∗ (𝑥, 𝑧; 𝛽)⟩ in the second statement of the ifz. After reducing this redex to mult’(𝑥𝑠; 𝛼, 𝜇𝑧. ˜ ∗ (𝑥, 𝑧; 𝛽)), we finally arrive at the result from the introduction. In the implementation, we solve this problem by statically reducing administrative redexes in a simplification step, but it is also possible to come up with a more elaborate definition of focusing which does not create them in the first place. Such an optimized focusing transformation is, however, much less transparent than the one we have described. 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 Type Soundness Matters in Functional Programming Languages

An Introduction to Evaluation Contexts in Programming Semantics

Read My Stories

Too Long; Didn't Read

Make resilience your competitive advantage

How Focusing Resolves Stuck Terms in Core Evaluation

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