By using this site, you agree to the Privacy Policy and Terms of Use.
Accept
World of SoftwareWorld of SoftwareWorld of Software
  • News
  • Software
  • Mobile
  • Computing
  • Gaming
  • Videos
  • More
    • Gadget
    • Web Stories
    • Trending
    • Press Release
Search
  • Privacy
  • Terms
  • Advertise
  • Contact
Copyright © All Rights Reserved. World of Software.
Reading: Sequent Calculus vs CPS: A Compiler’s Perspective on Consumers and Evaluation Strategies | HackerNoon
Share
Sign In
Notification Show More
Font ResizerAa
World of SoftwareWorld of Software
Font ResizerAa
  • Software
  • Mobile
  • Computing
  • Gadget
  • Gaming
  • Videos
Search
  • News
  • Software
  • Mobile
  • Computing
  • Gaming
  • Videos
  • More
    • Gadget
    • Web Stories
    • Trending
    • Press Release
Have an existing account? Sign In
Follow US
  • Privacy
  • Terms
  • Advertise
  • Contact
Copyright © All Rights Reserved. World of Software.
World of Software > Computing > Sequent Calculus vs CPS: A Compiler’s Perspective on Consumers and Evaluation Strategies | HackerNoon
Computing

Sequent Calculus vs CPS: A Compiler’s Perspective on Consumers and Evaluation Strategies | HackerNoon

News Room
Last updated: 2025/07/09 at 5:56 PM
News Room Published 9 July 2025
Share
SHARE

Table of Links

  1. Introduction

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

  3. Evaluation Within a Context

    3.1 Evaluation Contexts for Fun

    3.2 Focusing on Evaluation in Core

  4. Typing Rules

    4.1 Typing Rules for Fun

    4.2 Typing Rules for Core

    4.3 Type Soundness

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

  6. Related Work

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

5.5 Direct and Indirect Consumers

As mentioned in the introduction, a natural competitor of sequent calculus as an intermediate representation is continuation-passing style (CPS). In CPS, reified evaluation contexts are represented by functions. This makes the resulting types of programs in CPS arguably harder to understand. There is, however, another advantage of sequent calculus over CPS as described by Downen et al. [2016]. The first-class representation of consumers in sequent calculus allows us to distinguish between two different kinds of consumers: direct consumers, i.e., destructors, and indirect consumers. In particular, this allows to chain direct consumers in Core in a similar way as in Fun.

Suppose we have a codata type with destructors get and set for getting and setting the value of a reference. Now consider the following chain of destructor calls on a reference 𝑟 in Fun

𝑟 .set(3).set(4).get()

A compiler could use a user-defined custom rewrite rule for rewriting two subsequent calls to set into only the second call. In Core the above example looks as follows:

𝜇𝛼.⟨𝑟 | set(3; set(4; get(𝛼)⟩

We still can immediately see the direct chaining of destructors and thus apply essentially the same rewrite rule. In CPS, however, the example would rather become

𝜆𝑘. 𝑟 .set(3; 𝜆𝑠. 𝑠.set(4; 𝜆𝑡 . 𝑡 .get(𝑘)))

The chaining of the destructors becomes obfuscated by the indirections introduced by representing the continuations for each destructor as a function. To apply the custom rewrite rule mentioned above, it is necessary to see through the lambdas, i.e. the custom rewrite rule has to be transformed to be applicable.

5.6 Call-By-Value, Call-By-Name and Eta-Laws

In Section 2.2 we already pointed out the existence of statements ⟨𝜇𝛼.𝑠1 | 𝜇𝑥.𝑠 ˜ 2⟩ which are called critical pairs because they can a priori be reduced to either𝑠1 [𝜇𝑥.𝑠 ˜ 2/𝛼] or𝑠2 [𝜇𝛼.𝑠1/𝑥]. These critical pairs were already discussed by Curien and Herbelin [2000] when they introduced the 𝜆𝜇𝜇˜-calculus. One solution is to pick an evaluation order, either call-by-value (cbv) or call-by-name (cbn), that determines to which of the two statements we should evaluate, and in this paper we chose to always use the call-by-value evaluation order. The difference between these two choices has also been discussed by Wadler [2003]. Note that this freedom for the evaluation strategy is another advantage of sequent calculus over continuation-passing style, as the latter always fixes an evaluation strategy.

Which evaluation order we choose has an important consequence for the optimizations we are allowed to perform in the compiler. If we choose call-by-value, then we are not allowed to use all 𝜂-equalities for codata types, and if we use call-by-name, then we are not allowed to use all 𝜂-equalities for data types. Let us illustrate the problem in the case of codata types with the following example:

⟨cocase {ap(𝑥; 𝛼) ⇒ ⟨𝜇𝛽.𝑠1 | ap(𝑥; 𝛼)⟩} | 𝜇𝑥.𝑠 ˜ 2⟩ ≡𝜂 ⟨𝜇𝛽.𝑠1 | 𝜇𝑥.𝑠 ˜ 2⟩

We assume that 𝑥 and 𝛼 do not appear free in 𝑠1. The 𝜂-transformation is just the ordinary 𝜂-law for functions but applied to the representation of functions as codata types. The statement on the left-hand side reduces the 𝜇˜ first under both call-by-value and call-by-name evaluation order, i.e.

The right-hand side of the 𝜂-equality, however, reduces the 𝜇 first under call-by-value evaluation order, i.e.

Therefore, the 𝜂-equality is only valid under call-by-name evaluation order. This example shows that the validity of applying this 𝜂-rule as an optimization depends on whether the language uses call-by-value or call-by-name. If we instead used a data type such as Pair, a similar 𝜂-reduction would only give the same result as the original statement when using call-by-value.

5.7 Linear Logic and the Duality of Exceptions

We have introduced the data type Pair(𝜎, 𝜏) and the codata type LPair(𝜎, 𝜏) as two different ways to formalize tuples. The data type Pair(𝜎, 𝜏) is defined by the constructor Tup whose arguments are evaluated eagerly, so this type corresponds to strict tuples in languages like ML or OCaml. The codata type LPair(𝜎, 𝜏) is a lazy pair which is defined by its two projections fst and snd, and only when we invoke the first or second projection do we start to compute its contents. This is closer to how tuples behave in a lazy language like Haskell.

Linear logic [Girard 1987; Wadler 1990] adds another difference to these types. In linear logic we consider arguments as resources which cannot be arbitrarily duplicated or discarded; every argument to a function has to be used exactly once. If we follow this stricter discipline, then we have to distinguish between two different types of pairs: In order to use a pair 𝜎 ⊗ 𝜏 (pronounced “times” or “tensor”), we have to use both the 𝜎 and the 𝜏, but if we want to use a pair 𝜎 & 𝜏 (pronounced “with”), we must choose to either use the 𝜎 or the 𝜏. It is now easy to see that the type 𝜎 ⊗ 𝜏 from linear logic corresponds to the data type Pair(𝜎, 𝜏), since when we pattern match on this type we get two variables in the context, one for 𝜎 and one for 𝜏. The type 𝜎 & 𝜏 similarly corresponds to the type LPair(𝜎, 𝜏) which we use by invoking either the first or the second projection, consuming the whole pair.

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.


Sign Up For Daily Newsletter

Be keep up! Get the latest breaking news delivered straight to your inbox.
By signing up, you agree to our Terms of Use and acknowledge the data practices in our Privacy Policy. You may unsubscribe at any time.
Share This Article
Facebook Twitter Email Print
Share
What do you think?
Love0
Sad0
Happy0
Sleepy0
Angry0
Dead0
Wink0
Previous Article The 35 best Prime Day deals you can get for under $25
Next Article Dude, You’re Getting Prime Day Deals on Dell Desktops, Laptops, Monitors, and More
Leave a comment

Leave a Reply Cancel reply

Your email address will not be published. Required fields are marked *

Stay Connected

248.1k Like
69.1k Follow
134k Pin
54.3k Follow

Latest News

Germany Leapfrogs UK To Lead European VC Investment In Q2 As Region’s Funding Settles
News
Sky is giving away free pizzas with almost 2 million treats and Sky Sports perk
News
Shark’s powerful cordless vacuum is reduced by £170 for Prime Day
Gadget
AMD Warns of New Transient Scheduler Attacks Impacting a Wide Range of CPUs
Computing

You Might also Like

Computing

AMD Warns of New Transient Scheduler Attacks Impacting a Wide Range of CPUs

7 Min Read
Computing

Four Arrested in £440M Cyber Attack on Marks & Spencer, Co-op, and Harrods

4 Min Read
Computing

LibreOffice 25.8 RC1 Released With Various File Performance Improvements

2 Min Read
Computing

Agibot denies backdoor listing via Swancor Advanced Materials acquisition · TechNode

1 Min Read
//

World of Software is your one-stop website for the latest tech news and updates, follow us now to get the news that matters to you.

Quick Link

  • Privacy Policy
  • Terms of use
  • Advertise
  • Contact

Topics

  • Computing
  • Software
  • Press Release
  • Trending

Sign Up for Our Newsletter

Subscribe to our newsletter to get our newest articles instantly!

World of SoftwareWorld of Software
Follow US
Copyright © All Rights Reserved. World of Software.
Welcome Back!

Sign in to your account

Lost your password?