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: Why Compiler Writers Care About Case-of-Case | 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 > Why Compiler Writers Care About Case-of-Case | HackerNoon
Computing

Why Compiler Writers Care About Case-of-Case | HackerNoon

News Room
Last updated: 2025/07/09 at 6:59 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.3 Let-Bindings are Dual to Control Operators

The label construct in Fun is translated to a πœ‡-binding in Core. Also, when considering the typing rule for label 𝛼 {𝑑 } in Section 4.1, we can see that it directly corresponds to typing a πœ‡-binding with the label 𝛼 being the bound covariable. Similarly, a let-binding is translated to a πœ‡Λœ-binding and typing a let-binding in Fun closely corresponds to typing a πœ‡Λœ-term in Core. This way, labels and let-bindings are dual to each other, the same way πœ‡ and πœ‡Λœ are. The duality can be extended to other control operators such as call/cc.

As it turns out, the label construct is very closely related to call/cc. There are in fact only two differences. First, label 𝛼 {𝑑 } has the binder 𝛼 for the continuation built into the construct, just as the variation of call/cc named let/cc (which Reynolds [1972] called escape). The second, and more important difference is that the invocation of the continuation captured by label 𝛼 {𝑑 } happens through an explicit language construct goto(𝑑; 𝛼). This makes it easy to give a translation to Core as we can simply insert another πœ‡-binding to discard the remaining continuation at exactly the place where the captured continuation is invoked. In contrast, with call/cc and let/cc the continuation is applied in the same way as a normal function, making it necessary to redefine the variable the captured continuation is bound to when translating to Core. This obscures the duality to let-bindings which is so evident for label and goto.

To see this, here is a translation of let/cc π‘˜ 𝑑 to Core

[let/cc π‘˜ 𝑑] ≔ πœ‡π›Ό.⟨cocase {ap(π‘₯, 𝛽) β‡’ ⟨π‘₯ | π›ΌβŸ©} | πœ‡π‘˜. ˜ ⟨[𝑑] | π›ΌβŸ©βŸ©

The essence of the translation still is that the current continuation is captured by the outer πœ‡ and bound to 𝛼. But now we also have to transform this 𝛼 into a function (the cocase here) which discards its context (here bound to 𝛽) and bind this function to π‘˜, which is done using πœ‡Λœ. For call/cc, the duality is even more obscured, as there the binder for the continuation is hidden in the function which call/cc is applied to. For the translation, this function must then be applied to the above cocase and the captured continuation 𝛼, resulting in the following term (cf. also [Miquey 2019]).

[call/cc 𝑓] ≔ πœ‡π›Ό.⟨[𝑓 ] | ap(cocase {ap(π‘₯, 𝛽) β‡’ ⟨π‘₯ | π›ΌβŸ©}, 𝛼)⟩

Other control operators for undelimited continuations can be translated in a similar way. For example, consider Felleisen’s C [Felleisen et al. 1987]. The difference to call/cc is that C discards the current continuation if it is not invoked somewhere in the term C is applied to, whereas call/cc leaves it in place and thus behaves as a no-op if the captured continuation is never invoked. The only change that needs to be made in the translation to Core is that the top-level continuation ⋆ has to be used for the outer cut instead of using the captured continuation. This is most easily seen for a variation of C which has the binder for the continuation built into the operator and where the invocation of the continuation is explicit, similar to label/goto. Calling this variation labelC, we obtain the following translation

[labelC 𝛼 {𝑑 }] ≔ πœ‡π›Ό.⟨[𝑑] | β‹†βŸ©

Here the duality to let-bindings is evident again. The translation for C itself is then obtained in the same way as for call/cc

[C 𝑓 ] ≔ πœ‡π›Ό.⟨[𝑓 ] | ap(cocase {ap(π‘₯, 𝛽) β‡’ ⟨π‘₯ | π›ΌβŸ©}, ⋆)⟩

5.4 The Case-of-Case Transformation

One important transformation in functional compilers is the case-of-case transformation. Maurer et al. [2017] give the following example of this transformation. The term

ifΒ (if 𝑒1Β then 𝑒2Β else 𝑒3)Β then 𝑒4Β else 𝑒5

can be replaced by the term

if 𝑒1Β thenΒ (if 𝑒2Β then 𝑒4Β else 𝑒5)Β elseΒ (if 𝑒3Β then 𝑒4Β else 𝑒5).

Logicians call these kinds of transformations commutative conversions, and they play an important role in the study of the sequent calculus. But as Maurer et al. [2017] show, they are also important for compiler writers who want to generate efficient code.

In the πœ†πœ‡πœ‡Λœ-calculus, commuting conversions don’t have to be implemented as a special compiler pass. They fall out for free as a special instance of πœ‡-reductions! Let us illustrate this point by translating Maurer et al.’s example into the πœ†πœ‡πœ‡Λœ-calculus. First, let us translate the two examples using pattern-matching syntax:

![](data:image/svg+xml,%3csvg%20xmlns=%27http://www.w3.org/2000/svg%27%20version=%271.1%27%20width=%27800%27%20height=%2761.38513513513513%27/%3e) imageimage

Let us now translate these two terms into the πœ†πœ‡πœ‡Λœ-calculus:

![](data:image/svg+xml,%3csvg%20xmlns=%27http://www.w3.org/2000/svg%27%20version=%271.1%27%20width=%27800%27%20height=%27128.48765432098767%27/%3e) imageimage

We can see that just by reducing all of the underlined redexes we reduce both of these examples to the same term.

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 Apple’s second-generation Vision Pro might launch this year
Next Article Pick up the Amazon Fire TV Soundbar at an all-time low price with Prime savings
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

Why Cluely’s Roy Lee isn’t sweating cheating detectors | News
News
Popular Tex Mex chain confirms it will close down all locations after 36 years
News
Sky overtakes Virgin Media with blisteringly fast new broadband for millions
News
Today's NYT Mini Crossword Answers for July 10 – CNET
News

You Might also Like

Computing

Manus trims China team, relocates core staff to Singapore headquarters Β· TechNode

3 Min Read
Computing

The HackerNoon Newsletter: Pixels, Paperbacks, and Power (7/9/2025) | HackerNoon

2 Min Read
Computing

AI’s Fingerprints Were Found in 13.5% of Scientific Papers | HackerNoon

5 Min Read
Computing

Wayback Is Now Hosted On FreeDesktop.org

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?