This content originally appeared on HackerNoon and was authored by Abstraction: Computer Science Discourse
Table of Links
Translating To Sequent Calculus
Evaluation Within a Context
Insights
5.1 Evaluation Contexts are First Class
5.3 Let-Bindings are Dual to Control Operators
5.4 The Case-of-Case Transformation
5.5 Direct and Indirect Consumers
Conclusion, Data Availability Statement, and Acknowledgments
A. The Relationship to the Sequent Calculus
C. Operational Semantics of label/goto
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.
\ def mult(𝑙) ≔ label 𝛼 {mult’(𝑙; 𝛼)}
\ def mult’(𝑙; 𝛼) ≔ case 𝑙 of {Nil ⇒ 1, Cons(𝑥, 𝑥𝑠) ⇒ ifz(𝑥, goto(0; 𝛼), 𝑥 ∗ mult’(𝑥𝑠; 𝛼))}
\ When we translate to Core and simplify the resulting term, we get the result:
\ 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.
\
:::info 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.
:::
:::info This paper is available on arxiv under CC BY 4.0 license.
:::
\
This content originally appeared on HackerNoon and was authored by Abstraction: Computer Science Discourse
Abstraction: Computer Science Discourse | Sciencx (2025-07-06T23:58:15+00:00) How Functional Languages Simulate Goto with Labels and μ-Bindings. Retrieved from https://www.scien.cx/2025/07/06/how-functional-languages-simulate-goto-with-labels-and-%ce%bc-bindings/
Please log in to upload a file.
There are no updates yet.
Click the Upload button above to add an update.