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 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. 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.

How Typing Rules and Type Soundness Work in Core and Fun Programming Languages

How Focusing Resolves Stuck Terms in Core Evaluation

Read My Stories

Too Long; Didn't Read

Make resilience your competitive advantage

Why Type Soundness Matters in Functional Programming Languages

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

Untitled Story

Account Abstraction, Analysed: Abstract & Introduction

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

Account Abstraction, Analysed: Abstract & Introduction

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