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 2.5 First-Class Functions A core feature that we have omitted until now are first-class functions which are characterized by lambda abstractions 𝜆𝑥.𝑡 and function applications 𝑡1 𝑡2. But first-class functions do not add any expressive power to a language with codata types, since codata types are a more general concept which subsumes functions as a special case. We could therefore implement lambda abstractions and function applications as syntactic sugar in both Fun and Core. This is incidentally also what the developers of Java did when they introduced lambdas to the language [Goetz et al. 2014]. We introduce lambda abstractions and function application to the syntax of Fun and desugar them to cocases and destructors of a codata type with an ap destructor during the translation to Core. Example 2.6. Consider the term (𝜆𝑥.𝑥 ∗ 𝑥) ⌜2⌝ in Fun. We can translate this term and evaluate it in Core as follows: ⟨cocase {ap(𝑥, 𝛽) ⇒ ⟨𝜇𝛾 . ∗ (𝑥, 𝑥;𝛾) | 𝛽⟩} | ap(⌜2⌝; ⋆)⟩ ⊲ ⟨𝜇𝛾 . ∗ (⌜2⌝, ⌜2⌝;𝛾) | ⋆⟩ ⊲ ∗ ⟨⌜4⌝ | ⋆⟩ 2.6 Control Operators Finally, we add the feature that we used in the motivating example in the introduction: labels and jumps. We have to extend Fun with label and goto constructs but since we can translate them locally to 𝜇-bindings we don’t have to add anything to Core. A term label 𝛼 {𝑡 } binds a covariable 𝛼 in the term 𝑡 and thereby provides a location to which a goto used within 𝑡 can jump. Such a goto(𝑡; 𝛼) takes the location 𝛼 as an argument, as well as the term 𝑡 that should be used to continue the computation at the location where 𝛼 was bound. It is a bit tricky to write down precisely how the evaluation of label and goto works, but the following two rules are a good approximation, where we assume that 𝛼 does not occur free in 𝔱: label 𝛼 {𝔱} ⊲ 𝔱 label 𝛼 {. . . goto(𝔱; 𝛼) . . .} ⊲ 𝔱 The left rule says that when the labeled term 𝑡 can be evaluated to a value 𝔱 without ever using a goto, then we can discard the surrounding label. The rule on the right says that if we do have a goto which jumps to the label 𝛼 with a value 𝔱, then we discard everything between the label and the goto and continue the computation with this value 𝔱. In order to make this second rule precise, we have to make explicit what we only indicate with the ellipses separating the label from the jump; we will do so in Section 3. Example 2.7. In the introduction, we used the example of a fast multiplication function which multiplies all the elements of a list and short-circuits the computation if it encounters a zero. As we have allowed top-level definitions to pass covariables as arguments, we can now write the example of the introduction. Example 2.7. def mult(𝑙) ≔ label 𝛼 {mult’(𝑙; 𝛼)} def label def mult’(𝑙; 𝛼) ≔ case 𝑙 of {Nil ⇒ 1, Cons(𝑥, 𝑥𝑠) ⇒ ifz(𝑥, goto(0; 𝛼), 𝑥 ∗ mult’(𝑥𝑠; 𝛼))} def case of ifz goto When we translate to Core and simplify the resulting term, we get the result: Core def mult(𝑙; 𝛼) ≔ mult’(𝑙; 𝛼, 𝛼) def mult’(𝑙; 𝛼, 𝛽) ≔ ⟨𝑙 | case {Nil ⇒ ⟨1 | 𝛽⟩, Cons(𝑥, 𝑥𝑠) ⇒ ifz(𝑥, ⟨0 | 𝛼⟩, ∗(𝑥, 𝜇𝛾 .mult’(𝑥𝑠; 𝛼,𝛾); 𝛽))}⟩ This is almost the result we have seen in the introduction. The only difference is that the recursive call to mult’ is nested inside the multiplication. This is the same problem we have seen with nested arithmetic operations at the end of Section 2.1 and we will address it in the next section. The label/goto control operator we have introduced in this subsection is of course named after the goto instructions and labels which can be found in many imperative programming languages. Our adaption to the context of functional programming languages is similar to classical control operators (see Section 5.3 for a more precise discussion) such as J [Landin 1965] or let/cc (also known as escape) [Reynolds 1972]; the programming language Scala also provides the closely related boundary/break[3] where a boundary marks a block of code to which the programmer can jump with a break instruction. One central property of this control effect is that it is lexically scoped, since the label names 𝛼 are passed around lexically and can be shadowed. This distinguishes them from dynamically scoped control operators like the exception mechanisms found in many programming languages like Java or C++. (A dynamically scoped variant of our control operator would omit the label names, and the jump in label {. . . goto(𝑡) . . .} would return to the nearest enclosing label at runtime.) We follow the more recent reappraisal of lexically scoped control effects, for example by Zhang et al. [2016] in the case of exceptions or by Brachthäuser et al. [2020] in the case of effect handlers and delimited continuations. 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.

An Introduction to Evaluation Contexts in Programming Semantics

Understanding Algebraic Data and Codata Types in Functional Programming

Read My Stories

Too Long; Didn't Read

Make resilience your competitive advantage

How Functional Languages Simulate Goto with Labels and μ-Bindings

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