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.2 Let Bindings Let-bindings are important since we can use them to eliminate duplication and make code more readable. In this section we introduce let-bindings to Fun for an additional reason: they allow us to introduce the second construct which gives the 𝜆𝜇𝜇˜-calculus its name: 𝜇˜-abstractions. The let-bindings in Fun are standard and are evaluated by substituting the value 𝔱 for the variable 𝑥 in the body which is a term. The analogue of a let-binding in Fun is a 𝜇˜-binding in Core which also binds a variable, with the difference that the body of a 𝜇˜-binding is a statement. It can easily be seen that 𝜇˜-bindings are the precise dual of 𝜇-bindings that we have already introduced. With both 𝜇- and 𝜇˜-bindings in Core we have to face a potential problem, namely statements of the form ⟨𝜇𝛼.𝑠1 | 𝜇𝑥.𝑠 ˜ 2⟩. Such a statement is called a critical pair since it can potentially be reduced to both 𝑠1 [𝜇𝑥.𝑠 ˜ 2/𝛼] and 𝑠2 [𝜇𝛼.𝑠1/𝑥] which can be a source of non-confluence. A closer inspection of the rules shows that we avoid this pitfall and always evaluate the statement to 𝑠1 [𝜇𝑥.𝑠 ˜ 2/𝛼]. We do not allow to reduce the statement to 𝑠2 [𝜇𝛼.𝑠1/𝑥] since only values 𝔭 can be substituted for variables, and 𝜇𝛼.𝑠1 is not a value. This restriction precisely mirrors the restriction on the evaluation of let-bindings in Fun. In other words, we use call-by-value evaluation order. We will address the critical pair and how it relates to different evaluation orders again in Section 5.6. We can observe that the arithmetic expression 2 ∗ 2 has been evaluated only once, which is precisely what we expect from call-by-value. 2.3 Top-level Definitions We introduce recursive top-level definitions to Fun and Core for two reasons. They allow us to write more interesting examples and they illustrate a difference in how recursive calls are handled. The extension is specified in Definition 2.4. Top-level definitions should not be confused with first-class functions which will be introduced later, since they cannot be passed as an argument or returned as a result. They are a part of a program that consists of a list of such top-level definitions. The top-level definitions in Fun curiously also take covariables as arguments even though the language does not contain consumers; you can ignore that for now. If you remember the example from the introduction, then you might recall that we use them for passing labels, but we will only formally introduce that construct in Section 2.6. We evaluate the call of a top-level definition by looking up the body in the program and substituting the arguments of the call for the parameters in the body of the definition. The body of a top-level definition is a term in Fun and a statement in Core. This difference explains why we have to add an additional parameter 𝛼 to every top-level definition when we translate it; this parameter 𝛼 also corresponds to the additional continuation argument when we ordinarily translate a function into continuation-passing style. We could also have specified that the body of a top-level definition in Core should be a producer. We don’t do that because when we eventually translate Core to machine code we want every top-level definition to become the target of a jump with arguments without building up a function call stack. The following example shows how this works: Example 2.3. Using a top-level definition, we can represent the factorial function in Core. Example 2.3 For the argument ⌜1⌝ this evaluates in the following way: At the point (∗) of the evaluation we can now see how the recursive call is evaluated. In Fun this recursive call would have the form 1 ∗ fac(0) and require a function stack, but in Core we can jump to the definition of fac with the consumer 𝜇𝑟 . ˜ ∗ (⌜1⌝, 𝑟; ⋆) as an additional argument which contains the information that the result of the recursive call should be bound to the variable 𝑟 and then multiplied with ⌜1⌝. Note again that this consumer argument corresponds to a continuation in continuation-passing style (in that sense it might be viewed as a reified stack) and so the basic techniques used in CPS-based intermediate representations and compilers can be applied for its implementation. 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 Lead image by ThisIsEngineering on Pexels. Lead image by ThisIsEngineering on Pexels.

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

Understanding Algebraic Data and Codata Types in Functional Programming

Why Arithmetic in Functional Languages Needs Sequent Calculus

Read My Stories

Too Long; Didn't Read

Make resilience your competitive advantage

How Let Bindings Improve Code Readability in Functional Programming

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