Dieses Kapitel untersucht die Konzeption und Implementierung von benannten und optionalen Argumenten in Programmiersprachen und hebt deren Vorteile und Herausforderungen hervor. Es beginnt mit der Diskussion des -Kalküls und des Konzepts der Strömung, die zwar nützlich ist, aber die Flexibilität der Funktionsanwendung einschränken kann. Das Kapitel untersucht dann anhand von Beispielen aus Sprachen wie Python, Ruby und OCaml, wie benannte und optionale Argumente die Lesbarkeit und Flexibilität verbessern. Es identifiziert fünf zentrale Designentscheidungen in Sprachen, die die genannten Argumente unterstützen: Kommutativität, Wahlfreiheit, Strömung, Unterscheidbarkeit und erstklassige Werte. Das Kapitel vertieft sich in die Fragen der Typensicherheit, die sich aus erstklassigen benannten Argumenten und Subtypen ergeben, und präsentiert einen neuartigen Ansatz, der eine Kernrechnung mit Schnitt- und Verbundtypen verwendet. Dieser Ansatz gewährleistet die Typensicherheit durch Umschreiben der Anrufseite und Ausarbeitungssemantik, die formell mit dem Coq-Proof-Assistenten nachgewiesen werden. Das Kapitel behandelt auch die Umsetzung dieses Ansatzes in der CP-Sprache und seine möglichen Anwendungen in anderen Sprachen. Darüber hinaus werden benannte Argumente in bestehenden Sprachen wie OCaml, Scala, Racket und Haskell untersucht und ihre Stärken und Grenzen diskutiert. Das Kapitel schließt mit der Betonung der Wichtigkeit einer soliden Grundlage für benannte und optionale Argumente und der Notwendigkeit sorgfältiger Berücksichtigung von Fragen der Typensicherheit im Sprachdesign.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Named and optional arguments are prevalent features in many mainstream programming languages, enhancing code readability and flexibility. Despite widespread use, their formalization has not been extensively studied. This paper bridges this gap by presenting a type-safe foundation for named and optional arguments using intersection and union types. We begin by identifying a critical type-safety issue in popular static type checkers for Python and Ruby, particularly in handling first-class named arguments in the presence of subtyping. Our solution involves rewriting call sites to ensure type safety, which we formalize through a translation into a core calculus called \(\lambda _\textsf{iu}\). The type safety of the translation is proven using the Coq proof assistant. The practical implementation of our approach in the CP language validates our theoretical contributions. Furthermore, we informally discuss how our approach could be adapted to encode named and optional arguments in other existing languages.
1 Introduction
The \(\lambda \)-calculus, introduced by Alonzo Church [5], shows how to model computation solely with function abstraction and application. For example, natural numbers, boolean values, pairs, and lists, as well as various operations on them, can be represented by higher-order functions via Church encoding. In the \(\lambda \)-calculus, a function only has one parameter and can only be applied to one argument. Many programming languages in the ML family inherit this feature. If more than one argument is desired in those languages, we need to create a sequence of functions, each with a single argument, and perform an iteration of applications. This idea is called currying. Currying brings brevity to functional programming and naturally allows partial application, but it usually limits the flexibility of function application. For example, we cannot pass arguments in a different order nor omit some of them by providing default values. Both demands are not rare in practical programming and can be met in a language that supports named and optional arguments. Named arguments also largely improve the readability of function calls. For example, it is unclear which is the source and which is the destination in copy(x, y), while copy(to: x, from: y) is self-explanatory.
Named arguments are widely supported in mainstream programming languages, such as Python, Ruby, OCaml, C#, and Scala, just to name a few. The earliest instance, to the best of our knowledge, is Smalltalk, where every method argument must be associated with a keyword (i.e. an external name). In other words, there are no positional arguments (i.e. arguments with no keywords) in Smalltalk. The syntax of modern languages is usually less rigid, so programmers can choose whether to attach keywords to arguments or not. There are two ways to reconcile positional and named arguments. One way, employed by Python and shown in Fig. 1a, is to make parameter names in a function definition as non-mandatory keywords. Thus, every argument can be passed with or without keywords by default. As shown in the Python code, exp(10, 2) is equivalent to exp(x=10, base=2). To reconcile the two forms in the same call, a restriction is imposed that all named arguments must follow positional ones. The other way, shown in Fig. 1b and used in Ruby, is to strictly distinguish named arguments from positional ones. When defining a Ruby function, a keyword parameter should always end with a colon even if it does not have a default value. By this means, they are syntactically distinct from positional parameters, and their keywords cannot be omitted in a function call. There is also a restriction in Ruby that all named arguments must follow positional ones in both function definitions and call sites. The two kinds of arguments are usually used in different scenarios: positional arguments are used when the number of arguments is small and the order is clear, while named arguments are used in more complex cases especially when settings or configurations are involved.
Anzeige
More interestingly, named arguments are first-class values in Python and Ruby: they can be assigned to a variable. As shown at the bottom of Fig. 1, the variable args stores the two arguments named base and x, and we can later pass it to exp by unpacking it with ** (sometimes called the splat operator). In fact, args is a dictionary in Python and similarly a hash in Ruby. Thus, first-class named arguments can be manipulated and passed around like standard data structures. This feature is widely used in Python and Ruby.
Fig. 1:
Named arguments in Python and Ruby.
Including the distinctness and first-class values illustrated above, we have identified five important design choices found in existing languages that support named arguments:
1.
Commutativity: whether the order of (actual) arguments can be different from that of (formal) parameters originally declared.
2.
Optionality: whether some arguments can be omitted in a function call if their default values are predefined.
3.
Currying: whether a function that takes more than one argument is always converted into a chain of functions that each take a single argument.
4.
Distinctness: whether named arguments are distinct from positional ones in how they are defined and passed.
5.
First-class value: whether named arguments are first-class values.
As shown in Table 1, the first two properties hold for most mainstream programming languages, with Smalltalk and Swift being two exceptions. Commutativity and optionality are so useful that we believe they should not be compromised. Concerning the third point, OCaml is the only language that manages to reconcile currying with commutativity, though at the cost of introducing a very complicated core calculus. We agree that currying is very useful when we use normal positional arguments, but we argue here that currying can be temporarily dropped when we use named arguments because the most common use case for named arguments is to represent a whole chunk of parameters like settings or configurations. The fourth design, distinctness, is endorsed by Ruby, Racket, OCaml, Dart, and Swift. It improves the readability of call sites to enforce keywords whenever arguments are defined to be named. We advocate distinctness in this paper also because it simplifies the language design and allows us to focus on more important topics, especially type safety with first-class named arguments.
Table 1:
Named arguments with different design choices in different languages.
Dummy
Although named arguments are ubiquitous, they have not attracted enough attention in the research of programming languages. Among the few related papers, the work by Garrigue et al. [1, 9, 12] formalizes a label-selective \(\lambda \)-calculus and eventually applies it to OCaml [11]. Another work by Rytz and Odersky [26] discusses the design of named and optional arguments in Scala, but it mainly focuses on practical aspects. The core features of Scala are formalized in a family of DOT calculi, but named arguments are never included. The support for named arguments is implemented as macros in Racket [7]. So their extension is more like userland syntactic sugar and requires no changes to the core compiler. Haskell does not support named arguments natively, but the paradigm of named arguments as records is folklore. We will discuss OCaml, Scala, Racket, and Haskell in detail in Section 5. In short, named arguments are implemented in an ad-hoc manner and are not well founded from a type-theoretic perspective in most languages, especially object-oriented ones. Only OCaml and this paper provide soundness proofs for the feature of named arguments.
Anzeige
An important issue that has not been explored in the literature is the interaction between subtyping and first-class named arguments. A naive design can easily lead to a type-safety issue. We will show in Section 2.2 that the most widely used optional type checker for Python, mypy [13], fails to detect a type-unsafe use of first-class named arguments. The same issue also exists in Ruby with Steep [16] or Sorbet [28]. It arises from subtyping hiding some arguments from their static type and bypassing the type checking for optional arguments. As a result, an optional argument may have an unexpected type at run time, which leads to a runtime error.
In this paper, we present a type-safe foundation for named and optional arguments. At the heart of our approach is the translation into a core calculus called \(\lambda _\textsf{iu}\), which features intersection and union types [2, 6, 8]. Our approach supports first-class named arguments like Python and Ruby, but the type-safety issue is addressed by us. The \(\lambda _\textsf{iu}\) calculus has been shown to be type-sound [23], and we show that our translation from our source language into \(\lambda _\textsf{iu}\) is type-safe. Thus, we establish the type safety of our approach. In addition, our design has recently been incorporated into the CP language [33].
In summary, the contributions of this paper are:
We identify a type-safety issue with first-class named arguments in the presence of subtyping and propose a solution based on call site rewriting.
We demonstrate how a minimal language with named and optional arguments can be translated to a core calculus with intersection and union types.
We formalize the translation as an elaboration semantics and prove its type safety using the Coq proof assistant.
We validate our theoretical contributions by implementing our approach in the CP language and showcasing a practical example.
We conduct a survey of named arguments in existing programming languages and discuss the best practice for named arguments as records in Haskell.
2 Named and Optional Arguments: The Bad Parts
Since named and optional arguments are not well studied in most languages, the ad-hoc mechanisms employed in those languages may sometimes surprise programmers or even cause safety issues.
2.1 Gotcha! Mutable Default Arguments in Python
Let us consider a simple Python function that appends an element to a list. We provide a default value for the list, which is an empty list:
After calling append(1), we get the expected result [1]. However, continuing to call append(2) gives us [1, 2] instead of [2]. This is because Python only evaluates the default value once when the function is defined, so the same list initialized for xs is shared across different calls to append. When calling append(2), the default value for xs is no longer an empty list but the list that has been modified by the previous call append(1).
This issue, while seemingly minor, highlights the importance of understanding the semantics of default arguments. Our design strives to avoid such surprises, following the principle of least astonishment, yet this is not our main focus. We will discuss the more critical issue about type safety next.
2.2 Caution! Type Safety with First-Class Named Arguments
As we have shown in Fig. 1, quite a few languages, especially dynamically typed ones like Python and Ruby, treat named arguments as first-class values. This feature is particularly helpful for passing settings because they are usually stored in a separate configuration file. We can read the settings from the file and pass them as named arguments using the ** operator. For example, we can find such code in Python to run a web server:
Although Python is dynamically typed, there is continuous effort in the Python community to improve the detection of type errors earlier in the development process, primarily through static analysis. There is an optional static type checker for Python called mypy [13]. In the example above, we make use of type hints, introduced in Python 3.5, to specify the types of the parameters and the return value of the run method. The type hints have no effect at run time but can be used by external tools like mypy to statically check if the code is well-typed. Perhaps surprisingly, the code above cannot pass mypy’s type checking, because the type inferred for args (i.e. dict[str,object]) is not precise enough. The type checker needs to know what keys args exactly has and what types the values associated with those keys have, in order to make sure that **args is compatible with the parameters of app.run.
Fortunately, TypedDict is added in Python 3.8 to represent a specific set of keys and their associated types. By default, every specified key is required, except when it is marked as NotRequired, which is a type qualifier added in Python 3.11. With TypedDict and NotRequired, we can now define a precise dictionary type for args that passes mypy’s type checking:
The mypy type checker will raise an error if we provide an argument with an incompatible type, such as a string for the debug key:
However, mypy’s type system is not completely type-safe. We can create a function f that takes a dictionary with three keys specified in type In and returns a dictionary with only two keys specified in type Out. The function type-checks in mypy because type In is compatible whenever type Out is expected. Roughly speaking, it means that In is a subtype of Out. Then we can use f to forget the debug key in the static type:
Here args3 has type Out without the debug key specified. From a static viewpoint, args3 only has two keys host and port, which are compatible with the parameters of app.run since debug is optional and has a default value. That is why app.run(**args3) type-checks in mypy. However, at run time, the debug key is still present in args3, so the string "Oops!" is passed as a named argument to app.run, which originally expects a boolean value. This results in a runtime error since there is an assertion in app.run to ensure that debug is boolean.
This issue is not unique to Python and mypy. We have reproduced nearly the same issue in Ruby with two popular type checkers, namely Steep [16] and Sorbet [28], which is illustrated in Appendices A&B.
In conclusion, subtyping can lead to a fundamental type-safety issue when dealing with first-class named and optional arguments. In essence, the following subsumption chain is questionable:
Following this chain bypasses mypy’s type compatibility checking for the debug key. Next we will show how to break the chain and address the type-safety issue.
3 Our Type-Safe Approach
In this section, we informally present how we translate named and optional arguments into a core language with intersection and union types, while retaining type safety. We start by introducing the core language constructs that we need. Then we illustrate our translation scheme by example and demonstrate how it recovers type safety. After that, we showcase a practical example in the CP language, which has incorporated our approach to support named and optional arguments. Finally, we discuss how our translation scheme can be applied to other languages.
3.1 Core Language
The core language features intersection and union types, which establish an elegant duality in the type system. A value of the intersection type \( A \wedge B \) can be assigned both \( A \) and \( B \), whereas a value of the union type \( A \vee B \) can be assigned either \( A \) or \( B \). Intersection and union types correspond to the logical conjunction and disjunction respectively. Similar calculi are widely studied [2, 6, 8] and provide a well-understood foundation for named and optional arguments.
Named Arguments as Intersections. Named arguments are translated to multi-field records. However, the core language does not support multi-field records directly. There are only single-field records in the core language, and multiple fields are represented as intersections of single-field record types. For example, \(\{ x : \mathbb {Z} \} \wedge \{ y : \mathbb {Z} \}\) represents a record type with two integer fields x and y. With intersection types, width subtyping for record types comes for free, and permutations of record fields are naturally allowed [24].
At the term level, a merge operator [6, 23] (denoted by
in this paper) is used to concatenate multiple single-field records to form multi-field records, reminiscent of Forsythe [24]. For example,
forms a two-field record from two single-field records.
Optional Arguments as Unions. Optional arguments are translated to nullable types. A nullable type is not implicit in the core language but is represented as a union with the null type [18]. For example, an optional integer argument named z is translated to \(\{ z : \mathbb {Z} \vee \textbf{Null} \}\).
At the term level, a type-based switch expression [8, 23] is used to scrutinize a term of a union type, reminiscent of ALGOL 68 [32]. For example, \(\textbf{switch} \, z \, \textbf{case} \, \mathbb {Z} \Rightarrow e_{{\textrm{1}}} \, \textbf{case} \, \textbf{Null} \Rightarrow e_{{\textrm{2}}} \) returns \( e_{{\textrm{1}}} \) if z is an integer or \( e_{{\textrm{2}}} \) if \(\textbf{null}\).
3.2 Translation by Example
Let us review the previous Python function in Section 2.1 that appends an element to a list, which defaults to an empty list:
The function will be translated to a core function as follows:
Here we can see that the default value (i.e. the empty list) is not shared across different calls to append because the default value is evaluated within the function body. Therefore, calling append(x=1) will consistently return [1] instead of surprisingly modifying the default value. This design leads to less astonishment and more predictable behavior.
Since we translate named parameter types to record types, we correspondingly translate named arguments to records. For example, the function call append(x=1, xs=[0]) will be translated to
.
Rewriting Call Sites. More importantly, we also rewrite call sites to add null values for absent optional arguments. For example, the function call append(x=1) will be rewritten and translated to
.
Dependent Default Values. Another advantage of our translation scheme is that it naturally allows default values to depend on earlier arguments. Python and Ruby do not support dependent default values, but this feature can be useful in some practical scenarios. For example, when setting up I/O, we may want to output error messages to the same stream as out by default:
The variable out can be used in the default value of err because it has been brought into scope by the previous let-in binding:
The type safety of our translation scheme is essentially guaranteed by call site rewriting. Besides adding null values for absent optional arguments, we also sanitize arguments to ensure that they are expected from the parameter list. Since named arguments are first-class and can be passed as a variable, we may not have literals like append(x=1, xs=[0]) but splats like append(**args). So the matching between (formal) parameters and (actual) arguments is performed based on their static types:
If args has type \(\{ x : \mathbb {Z} \} \wedge \{ xs : [ \mathbb {Z} ] \}\), the call site will be rewritten to something equivalent to append(x=args.x, xs=args.xs).
If args only has type \(\{ x : \mathbb {Z} \}\), the call site will be rewritten to something equivalent to
.
For the append function, no other cases can pass the sanitization process.
Let us review the previous type-unsafe Python example in Section 2.2:
Recall that args has type Out, which is similar to
. The debug key is forgotten in the static type but is still present at run time. It passes mypy’s type checking but raises a runtime error. In our translation scheme, the call site will be rewritten to the following form based on the type of args (i.e. Out):
Therefore, type safety is recovered in our translation scheme.
Takeaways. There are two important observations from our translation scheme:
1.
is not equivalent to
because the former contains more information that prevents optional from being associated with other types than B. In other words, the optional argument can be absent, but if it is present, it must have type B.
2.
Corresponding to the above observation at the type level, we explicitly pass a null value as an optional argument if it is statically missing. The null value fills the position of a potentially forgotten argument that may have a wrong type. In other words, we implement the splat operator as per the static type of named arguments.
3.4 Implementation in the CP Language
Our approach to named and optional arguments has been implemented in the CP language, a statically typed language for compositional programming [33]. CP supports not only intersection and union types but also the merge operator and type-based switch expression. The implementation of named and optional arguments in CP is a direct application of our translation scheme.
More interestingly, the sanitization process during call site rewriting comes for free because CP employs a coercive semantics for subtyping [14]. For example, a subtyping relation between
and
implies a coercion function from subtype to supertype. In CP, such coercions are implicitly inserted to remove the forgotten fields (e.g. debug in this case). Therefore, the only remaining work is to add null values for absent optional arguments.
Fig. 2:
Sierpiński carpets implemented in the CP language.
To demonstrate the use of named and optional arguments in CP, we show a fractal example in Fig. 2, which is adapted from previous work on CP’s application to embedded DSLs [29]. The code makes use of named and optional arguments a lot, including both the SVG/Rect constructors from the library and the fractal function defined by the client. For example, fractal has five named arguments (level, x, y, width, and height), among which level is optional with a default value of 4.
It is worth noting that named arguments are used as first-class values in the CP code. On the first line of the fractal body, we store three fields level, width, and height in a variable args, which are shared arguments for later calls. When constructing the center rectangle, we merge args with three more fields x, y, and color to form a full set of named arguments we need for the Rect constructor. When recursively calling fractal, we pass args merged with different x and y values to draw the eight sub-copies. In the main function, we also use a variable init to avoid repeating the same set of arguments for SVG, Rect, and fractal calls. The ** operator is not needed in CP when passing first-class named arguments. Note that the parameter lists of these three constructors/functions are not completely the same, but we can still use a larger set of named arguments to cover all the cases. This is possible because CP allows subtyping for named arguments while retaining type safety.
3.5 Applications to Other Languages
Although we base our translation scheme on a core language with intersection and union types for type-theoretic solidness and elegance, it can work for a wider range of languages. We discuss the alternatives to intersections and unions below.
Alternative to Intersections. Record types have existed long before intersection types were invented. In practice, multi-field records are rarely represented as intersections of single-field records. For example, Software Foundations [22] demonstrates how to directly model multi-field records and define depth, width, and permutation subtyping without intersections, though their formalization is more complex than ours.
There is a merge operator in our translation scheme, but we only use it to construct multi-field records statically. Although the merge operator can be powerful if we want to construct first-class named arguments at run time like in CP, its absence does not disable our translation scheme. In other words, we only assume a simplified version that does not merge terms dynamically.
Alternative to Unions. Nullable types are rarely represented as unions with the null type too. For example, C#, Kotlin, and Dart support nullable types as a primitive data structure. Putting a question mark behind any type makes it nullable in these languages (e.g. int?).
No matter how a nullable type is represented, there is usually some expression that can check whether a nullable value is null or not. For example, C# provides the
operator to examine the runtime type, which is generally known as type introspection and is similar to the type-based switch. C# also provides the null coalescing operator ?? and simplifies the common pattern \(\textbf{switch} \, e \, \textbf{as} \, x \, \textbf{case} \, A \Rightarrow x \, \textbf{case} \, \textbf{Null} \Rightarrow d \) as e??d for nullable values.
Dynamically Typed Languages. It may be surprising at first sight that dynamically typed languages can benefit from our work with static typing, but recall that the type-safety issue in Section 2.2 was found in Python. Nowadays, popular dynamically typed languages have been retrofitted with gradual typing. For example, Python has type hints and mypy [13], Ruby has RBS and Steep [16], JavaScript gets typed by TypeScript [17], and Lua gets typed by Luau [25]. All of these typed versions support record-like and union types, and all except Python also support intersection types. Our translation scheme can almost directly apply to these languages. For a concrete example, we show how the aforementioned exp function can be encoded in TypeScript:
The code is almost the same as in Section 3.2. Note that the
operator is the standard way to perform type introspection in TypeScript, and the type of args.base is refined from the
to
in the true-branch. We assume the call sites have been rewritten in the code above. In this manner, named and optional arguments can be added to TypeScript as syntactic sugar.
Although we have discussed several alternatives to intersection and union types, we believe that if a language is designed from scratch, our approach is a good choice. Intersection and union types not only subsume multi-field record and nullable types but also provide a solid and elegant foundation for other advanced features, such as function overloading and heterogeneous data structures. Castagna’s essay [3] is an excellent further reading on the beauty of programming with intersection and union types.
4 Formalization
In this section, we formalize the translation of named and optional arguments as an elaboration semantics. The target of elaboration is called \(\lambda _\textsf{iu}\), and the source is called Uaena. We prove that the source language with named and optional arguments is type-safe via (1) the type soundness of the target calculus and (2) the type soundness of elaboration. All the theorems are mechanically proven using the Coq proof assistant.
4.1 The Target Calculus: \(\lambda _\textsf{iu}\)
\(\lambda _\textsf{iu}\) is an extension to the calculus in Chapter 5 of Rehman’s dissertation [23] with \(\textbf{null}\), single-field records, and let-in bindings. The addition of let-in bindings is not essential because they can be desugared into lambda abstractions and applications:
However, we still have let-in bindings for the sake of readability, and this form of let-in bindings simplifies the rules of parameter elaboration (introduced later in Fig. 5). Another difference is that the original calculus uses the locally nameless representation [4] while ours directly uses names for bound variables.
Our changes to Rehman’s calculus are relatively trivial, and we do not touch the rules for intersection and union types. We will not discuss his design choices in this paper, because our focus is on the type soundness with the addition of \(\textbf{Null}\) and record types. We have proven in Coq that these extensions preserve type soundness.
Syntax of\(\boldsymbol{\lambda }_\textsf{iu}\)
The types include the top type \( \top \), the bottom type \( \bot \), the null type \(\textbf{Null}\), the integer type \( \mathbb {Z} \), function types \( A \rightarrow B \), record types \(\{ \ell : A \}\), intersection types \( A \wedge B \), and union types \( A \vee B \). \(\textbf{Null}\) is a unit type that has only one value \(\textbf{null}\).
The expressions include the empty record \(\{\}\), the null value \(\textbf{null}\), integer literals n, variables \( x \), lambda abstractions \( \lambda x \!:\! A .\; e \!:\! B \), function applications \( e_{{\textrm{1}}} \, e_{{\textrm{2}}} \), record literals \(\{ \ell : A = e \}\), record projections \( e . \ell \), merges
, type-based switch expressions \(\textbf{switch} \, e_{{\textrm{0}}} \, \textbf{as} \, x \, \textbf{case} \, A \Rightarrow e_{{\textrm{1}}} \, \textbf{case} \, B \Rightarrow e_{{\textrm{2}}} \), and let-in bindings \( letin \, e \). The syntax of \( letin \) is as follows:
$$\begin{aligned} letin {:}{:}= \textbf{let} \, x = e \, \textbf{in} ~|~ letin_{{\textrm{1}}} \circ letin_{{\textrm{2}}} ~|~ \textbf{id} \end{aligned}$$
The composition of two let-in bindings is denoted by \( letin_{{\textrm{1}}} \circ letin_{{\textrm{2}}} \), and an empty binding is denoted by \(\textbf{id}\).
Fig. 3:
Subtyping of \(\lambda _\textsf{iu}\).
Subtyping. Fig. 3 shows the subtyping rules of \(\lambda _\textsf{iu}\). The rules are standard for a type system with intersection and union types. rule Sub-Top shows that the top type \( \top \) is a supertype of any type, and rule Sub-Bot shows that the bottom type \( \bot \) is a subtype of any type. Rules Sub-And, Sub-AndL, and Sub-AndR handle the subtyping for intersection types, while rules Sub-Or, Sub-OrL, and Sub-OrR are for union types. Rules Sub-Null and Sub-Rcd added by us are straightforward. We prove that the subtyping relation is reflexive and transitive.
Theorem 1 (Subtyping Reflexivity)
\(\forall A, A <: A \).
Theorem 2 (Subtyping Transitivity)
If \( A <: B \) and \( B <: C \), then \( A <: C \).
Fig. 4:
Typing of \(\lambda _\textsf{iu}\).
Typing. Fig. 4 shows the typing rules of \(\lambda _\textsf{iu}\). The empty record \(\{\}\) has the top type \( \top \), as shown in rule Typ-Top. Rule Typ-Merge is the introduction rule for intersection types. Merging two functions is used for function overloading, and merging two records is used for record concatenation. Rule Typ-Switch is the elimination rule for union types. The type-based switch expression scrutinizes an expression having a union of the two scrutinizing types (i.e. \( e_{{\textrm{0}}} : A \vee B \)). This premise ensures the exhaustiveness of the cases in the switch. The \(\textbf{as}\)-variable \( x \) is refined to type \( A \) in \( e_{{\textrm{1}}} \) and to type \( B \) in \( e_{{\textrm{2}}} \). Rules Typ-Null, Typ-Rcd, and Typ-Prj added by us are straightforward. Rule Typ-Let uses an auxiliary judgment \(\varGamma \,\vdash \, letin \,\dashv \, \varGamma '\) (defined in Appendix C) to obtain the typing context for the body of the let-in binding. For example, if \( e_{{\textrm{1}}} \) has type \( A \), then \(\textbf{let} \, x = e_{{\textrm{1}}} \, \textbf{in} \, e_{{\textrm{2}}} \) adds \( x : A \) to the typing context before type-checking \( e_{{\textrm{2}}} \).
Dynamic Semantics. We have a small-step operational semantics for \(\lambda _\textsf{iu}\). The judgment \( e \longrightarrow e' \) means that \( e \) reduces to \( e' \) in one step, and \( e \longrightarrow ^* e' \) is for multi-step reduction. We extend the original dynamic semantics by adding rules for records and projections. Similarly to the applicative dispatch for function applications in the original calculus, we add a relation called projective dispatch for record projections. For example,
reduces to \(\{ x = 1 \} . x \) via projective dispatch to select the needed field.
Since the dynamic semantics of \(\lambda _\textsf{iu}\) is independent of the elaboration from Uaena to \(\lambda _\textsf{iu}\), we omit the rules here but leave them in Appendix D. Note that the operational semantics is not commonplace in that it is type-directed and non-deterministic. Please refer to Rehman’s dissertation [23] for detailed explanations.
Theorem 3 (Progress)
If \( \cdot \,\vdash \, e : A \), then either \( e \) is a value or \(\exists e' , e \longrightarrow e' \).
Theorem 4 (Preservation)
If \( \cdot \,\vdash \, e : A \) and \( e \longrightarrow e' \), then \( \cdot \,\vdash \, e' : A \).
Putting progress and preservation together, we conclude that \(\lambda _\textsf{iu}\) is type-sound: a well-typed term can never reach a stuck state.
Corollary 1 (Type Soundness)
If \( \cdot \,\vdash \, e : A \) and \( e \longrightarrow ^* e' \), then either \( e' \) is a value or \(\exists e'' , e' \longrightarrow e'' \).
4.2 The Source Calculus: Uaena
Uaena (Unnamed Arguments Extended with Named Arguments) is a minimal calculus with named and optional arguments. Although the calculus is small, named arguments are supported as first-class values and can be passed to or returned by a function. Besides functions with named arguments, Uaena also supports normal functions with positional arguments. The two kinds of functions are distinguished in the syntax, as seen in Ruby, Racket, OCaml, etc.
The types include the integer type \( \mathbb {Z} \), normal function types \( ( \mathcal {A} ) \rightarrow \mathcal {B} \), function types with named parameters \(\{ \mathcal {P} \} \rightarrow \mathcal {B}\), and (first-class) named argument types \(\{ \mathcal {K} \}\). The expressions include integer literals n, variables \( x \), normal lambda abstractions \( \lambda ( x \!:\! \mathcal {A} ).\; \epsilon \), lambda abstractions with named parameters \( \lambda \{ \rho \}.\; \epsilon \), function applications \(\epsilon _{{\textrm{1}}} \, \epsilon _{{\textrm{2}}}\), and (first-class) named arguments \(\{ \kappa \}\).
A named parameter type \(\mathcal {P}\) can be required (\(\ell :\mathcal {A}\)) or optional (\(\ell ?:\mathcal {A}\)). If a named parameter is optional, its default value must be provided in the function definition. For example, \(\lambda \{ x : \mathbb {Z} ;\; y =0\}.\; x + y \) has type \(\{ x : \mathbb {Z} ;\; y ?: \mathbb {Z} \} \rightarrow \mathbb {Z} \). A function with named parameters can only be applied to named arguments, which are basically a list of key-value pairs. For example, the previous function can be applied to \(\{ x =1;\; y =2\}\) or \(\{ x =1\}\) or a variable having a compatible type. The variable case demonstrates the first-class nature of named arguments in Uaena.
Careful readers may notice that a named argument type can also serve as the parameter of a normal function. This also demonstrates the first-class nature of named arguments. But note that a normal function that takes named arguments is different from a function with named parameters. Consider the following two functions, the former of which is a function with named parameters and the latter is a normal function:
$$\begin{aligned} (\lambda \{ x : \mathbb {Z} ;\; y =0\}.\; x + y ) \quad &:\quad \{ x : \mathbb {Z} ;\; y ?: \mathbb {Z} \} \rightarrow \mathbb {Z} \\ (\lambda ( args :\{ x : \mathbb {Z} ;\; y : \mathbb {Z} \}).\; args ) \quad &:\quad (\{ x : \mathbb {Z} ;\; y : \mathbb {Z} \}) \rightarrow \{ x : \mathbb {Z} ;\; y : \mathbb {Z} \} \end{aligned}$$
Although both functions can be applied to \(\{ x =1;\; y =2\}\), there are two main differences between them. First, optional parameters cannot be defined in a normal function. So we cannot provide \( y =0\) as a default value in the second function. Second, \( x \) and \( y \) are not brought into the scope of the function body in a normal function. So the only accessible variable is \( args \) in the second function.
Fig. 5:
Type-directed elaboration from Uaena to \(\lambda _\textsf{iu}\).
Fig. 6:
Type-directed call site rewriting in Uaena.
Elaboration. The type-directed elaboration from Uaena to \(\lambda _\textsf{iu}\) is defined at the top of Fig. 5. \(\varDelta \,\vdash \, \epsilon : \mathcal {A} \,\rightsquigarrow \, e \) means that the source expression \(\epsilon \) has type \(\mathcal {A}\) and elaborates to the target expression \( e \) under the typing context \(\varDelta \). Rules Ela-Abs and Ela-App for normal functions are straightforward. In rule Ela-NAbs for functions with named parameters, besides inferring the type of the function body \(\epsilon \) and elaborating it to \( e \), we generate let-bindings for the named parameters, which is delegated to the auxiliary judgment \( \varDelta \,\vdash \, _{\!\!\!\! x }\,\, \rho : \mathcal {P} \,\rightsquigarrow \, letin \,\dashv \, \varDelta ' \). In rule Ela-NApp, there is also an auxiliary judgment \( \varDelta \,\vdash \, _{\!\!\!\! e }\,\, \mathcal {P} \,\diamond \, \mathcal {K} \,\rightsquigarrow \, e' \) that rewrites call sites according to the parameter and argument types. Rules Ela-NEmpty and Ela-NField are used to elaborate named arguments.
Named Parameter Elaboration. As shown at the bottom of Fig. 5, \( \varDelta \,\vdash \, _{\!\!\!\! x }\,\, \rho : \mathcal {P} \,\rightsquigarrow \, letin \,\dashv \, \varDelta ' \) means that the named parameter \(\rho \) is inferred to have type \(\mathcal {P}\) and elaborates to a series of let-in bindings \( letin \), given that the named parameters correspond to the target bound variable \( x \). In the meanwhile, the typing context \(\varDelta \) is extended with the types of the named parameters to form \(\varDelta '\). \(\varDelta '\) is used for typing the body of the function with named parameters. Rule PEla-Required simply generates \(\textbf{let} \, \ell = x . \ell \, \textbf{in}\), while rule PEla-Optional generates \(\textbf{let} \, \ell = \textbf{switch} \, x . \ell \, \textbf{as} \, y \, \textbf{case} \, | \mathcal {A} | \Rightarrow y \, \textbf{case} \, \textbf{Null} \Rightarrow e \, \textbf{in}\) to provide a default value \( e \) for the \(\textbf{Null}\) case.
Call Site Rewriting. As shown in Fig. 6, \( \varDelta \,\vdash \, _{\!\!\!\! e }\,\, \mathcal {P} \,\diamond \, \mathcal {K} \,\rightsquigarrow \, e' \) means that if the parameter type \(\mathcal {P}\) is compatible with the argument type \(\mathcal {K}\), the target expression \( e \), which corresponds to the named arguments, will be rewritten to \( e' \). The compatibility check is based on the parameter type \(\mathcal {P}\). Rule PMat-Required handles the case where the argument is required, while rules PMat-Present and PMat-Absent handle the cases where the optional argument with a specific type is present and where the optional argument is absent, respectively. The remaining case, where the optional argument is present but associated with a wrong type, is prohibited and cannot elaborate to any term. We have two more auxiliary judgments \( \mathcal {K}\,{:}{:}\,\ell \Rightarrow \mathcal {A} \) and \( \mathcal {K}\,{:}{:}\,\ell \nRightarrow \) to indicate that the argument type \(\mathcal {K}\) contains a field \(\ell \) with type \(\mathcal {A}\) or \(\mathcal {K}\) does not contain \(\ell \), whose definitions can be found in Appendix E.
Type Translation. As we have informally mentioned in Section 3.1, we translate named parameters to intersection types and optional parameters to union types. The rules for \(|\cdot |\) can be found in Appendix F. Having defined the translation, we can prove the soundness of call site rewriting and elaboration.
Theorem 5 (Soundness of Call Site Rewriting)
If \( \varDelta \,\vdash \, _{\!\!\!\! e }\,\, \mathcal {P} \,\diamond \, \mathcal {K} \,\rightsquigarrow \, e' \) and \(| \varDelta | \,\vdash \, e : | \mathcal {K} | \), then \(| \varDelta | \,\vdash \, e' : | \mathcal {P} |\).
Theorem 6 (Soundness of Elaboration)
If \(\varDelta \,\vdash \, \epsilon : \mathcal {A} \,\rightsquigarrow \, e \), then \(| \varDelta | \,\vdash \, e : | \mathcal {A} |\).
With the two theorems above and the type soundness of \(\lambda _\textsf{iu}\), we can conclude that Uaena is type-safe.
5 Discussion and Related Work
In this section, we first discuss OCaml, the only language we know of that has well-studied support for named and optional arguments, though its mechanism does not go well with higher-order functions. Then we briefly show how named arguments are handled very differently in Scala and Racket. After that, we illustrate how named arguments can be encoded as records in Haskell while not natively supported. Finally, we discuss two more approaches we find in record calculi [19, 20]. We will also explain why all these approaches have drawbacks.
5.1 OCaml
OCaml did not support named arguments originally. Nevertheless, Garrigue et al. [1, 9, 12] conducted research on the label-selective \(\lambda \)-calculus and implemented it in OLabl [10], which extends OCaml with labeled and optional arguments, among others. All features of OLabl were merged into OCaml 3, despite subtle differences [11].
Here is an example of the exponential function defined in a labeled style:
In the definition of exp, base is an optional labeled parameter while x is a positional parameter. Changing x into a second labeled parameter will trigger an unerasable-optional-argument warning because OCaml expects that there should be a positional parameter after all optional parameters. This expectation is at the heart of how OCaml resolves the ambiguity introduced by currying.
For example, consider the function application exp 10.0. Is it a partially applied function or a fully applied one using the default value of base? Both interpretations are possible, but OCaml considers it to be a full application because the trailing positional argument x is given. The presence of the positional argument is used to indicate that the optional arguments before it can be replaced by their default values. However, this design may confuse users since (exp 10.0)\(\sim \)base:2.0 will raise a type error but exp 10.0\(\sim \)base:2.0 will not. Partial application does not lead to an equivalent program in such situations.
Option Types. In OCaml, an optional argument is internally represented as an option type, which comprises two constructors: None and Some. Here is an equivalent definition for exp:
This encoding is similar to union types, but it depends on the option type in the standard library. Unfortunately, this specific kind of option is not a built-in type in many mainstream languages, especially in those languages that do not support algebraic data types.
Higher-Order Functions. A surprising gotcha in OCaml is that the commutativity breaks down when we pass a function with labeled arguments to another function. Real World OCaml [15] gives the following example:
Normally, the order of named arguments does not matter in OCaml, so it type-checks whether we call divide\(\sim \)fst\(\sim \)snd or divide\(\sim \)snd\(\sim \)fst. However, order matters when we pass divide to a higher-order function. That is why apply1 divide type-checks while apply2 divide does not. It turns out that the OCaml way of handling labeled arguments does not go well with other features like higher-order functions. Our approach scales better in this regard and the commutativity still holds in higher-order contexts via intersection subtyping.
In short, OCaml has a very powerful label-selective core calculus that reconciles commutativity and currying, but it is quite complicated and may hinder its integration with other language features. Another thing worth mentioning is that labeled arguments in OCaml are not first-class values, so they cannot be assigned to a variable or passed around by functions. In contrast to OCaml, our approach supports first-class named arguments and targets a minimal core calculus with intersection and union types, which is compatible with many popular languages like Python, Ruby, JavaScript, etc.
5.2 Scala
Rytz and Odersky [26] described the design of named and default arguments in Scala. Like in Python, parameter names in a method definition are non-mandatory keywords in Scala, and thus every argument can be passed with or without keywords. Furthermore, the parameter names are not part of the public interface of a method. This design is partly due to the backward compatibility with earlier versions of Scala, so the addition of named arguments will not break any existing code. As a result of the conservative treatment, named arguments are not first-class values in Scala and cannot be defined in an anonymous function. In short, named arguments are more like syntactic sugar in Scala and do not interact with the type system.
Below we show an example in Scala. In order to let the default value of c depend on a and b, we make the function partly curried:
The code will be translated to equivalent code without keywords or defaults:
There are two things to note here. First, a new function
is generated for the default value of c, taking two parameters a and b. Second, the call site is translated to a series of variable assignments for each argument and a keyword-free call to f with arguments reordered. The whole call site is wrapped in a block to avoid polluting the namespace.
In conclusion, named arguments in Scala are handled in a very different way from OCaml and our approach. The Scala way is more syntactic than type-theoretic, so it is hard to do an apples-to-apples comparison with our approach.
5.3 Racket
Flatt and Barzilay [7] introduced keyword and optional arguments into Racket, which was known as PLT Scheme at that time. A keyword is prefixed with
in syntax and is implemented as a new built-in type in Racket. Keyword arguments are supported by replacing
,
, and the core application form with newly defined macros that recognize keyword-argument forms. Here is an example of a function f with three keyword arguments a, b, and c, among which c is optional and defaults to a+b:
The function call with keywords seems hard to implement because it just lists the function and arguments in juxtaposition. In fact, an application form in Racket implicitly calls #%app in its lexical scope, so the support for keyword arguments is done by supplying an #%app macro. A new keyword-apply function is also defined to accept keyword arguments as first-class values. For example, we can rewrite the function call above as follows1:
Note that we need to separate keywords and corresponding arguments into two lists. The third list is for positional arguments, so it is empty in this case. We cannot list keywords in arbitrary order: a contract violation will be signaled unless the keywords are sorted in alphabetical order. In other words, commutativity is lost for first-class keyword arguments in Racket.
In Typed Racket [31], Racket’s gradually typed sister language, f can be typed as
. The first list contains the required arguments (
and
), and the second list contains the optional ones (
). However, Typed Racket does not provide a typed version of
, and it is unclear how to properly type it.
In conclusion, Racket supports keyword and optional arguments in a unique way via its powerful macro system. However, the support for first-class keyword arguments is very limited and cannot easily transfer to a type-safe setting.
5.4 Haskell
Unlike the aforementioned languages, Haskell does not support named arguments natively. However, the paradigm of named arguments as records has long existed in the Haskell community. Although we have to uncurry a function to have all parameters labeled in a record, it is clearer and more human-readable, especially when different parameters have the same type. For example, in the web server library warp [27], various server settings are bundled in the data type Settings, as shown in Fig. 7a. It is obvious how named arguments correspond to record fields, but it needs some thought on how to encode default values for optional arguments. The simplest approach, also used by warp, is to define a record defaultSettings, as shown in Fig. 7b. Users can update whatever fields they want to change while keeping others. For example, we update settingsPort and settingsHost while keeping the rest unchanged in Fig. 7c. Finally, we call the library function runSettings with the updated settings to run a server.
Fig. 7:
Named arguments as records in Haskell.
Such an approach works fine here but still has two drawbacks. The first issue is the dependency on defaultSettings. It is awkward for users to look for a record containing particular default values, especially when there are a few similar records in a library. A better solution is to change the parameter of runSettings from a complete Settings to a function that updates Settings:
With the new interface, users do not need to look for default values anymore. However, this design still has a second drawback: all arguments must have default values. Usually, we do not consider every argument to be optional. For example, we may want to require users to fill in settingsPort. A workaround employed by SqlBackend in the library persistent [21] is to have another function that asks for required arguments and supplements default values for optional arguments:
Best Practice. Although mkSettings resolves the second issue, there is a regression concerning the first issue: users have to look for mk* functions now. Fortunately, we can harmonize both design patterns to develop a third approach:
This last approach is probably the best practice in Haskell, though it is already quite complicated and requires two GHC language extensions. Of course, there could be other approaches to encoding named and optional arguments in Haskell. Users could get confused about the various available design patterns. This is largely due to lack of language-level support. We believe it is better for a language to natively support named and optional arguments.
Sidenote. The design pattern of named arguments as records can also be found in other functional languages like Standard ML, Elm, and PureScript, just to name a few. It is worth mentioning that these languages have first-class support for record types, so no separate type declarations are needed like in Fig. 7a. However, they still suffer from lack of native support for optional arguments.
5.5 Record Calculi
Ohori discussed how to model optional arguments in the future work of his seminal paper on compiling a polymorphic record calculus [19]. He proposed to extend a record calculus with optional-field selection (\(e.\ell \;?\;d\)) which behaves like \(e.\ell \) if \(\ell \) is present in the record e or evaluates to d otherwise. However, his proposal is subject to a similar type-safety issue as mypy. The static type of e can easily lose track of the optional field \(\ell \) and fail to ensure that \(e.\ell \) has the same type as d at run time. Since Ohori did not explicitly mention how to type-check optional-field selection, we cannot make any firm conclusion about the type safety of his proposal.
Osinski also discussed the support for optional arguments in Section 3.5 of his dissertation on compiling record concatenation [20]. His approach is based on row polymorphism and makes use of a sort of predicate on rows: \( row _1\blacktriangleright row _2\), which means that \( row _1\) consists of all the fields in \( row _2\). With this predicate, a function has type \(\forall \rho .\; row _o\blacktriangleright \rho \Rightarrow \{ row _r,\rho \}\rightarrow \tau \) if the required and optional arguments are denoted by \( row _r\) and \( row _o\), respectively. Roughly speaking, it means the parameter has a type between \(\{ row _r\}\) and \(\{ row _r, row _o\}\). At the term level, he introduced a compatible concatenation operator
, which allows overlapping fields with the same types and prefers the fields on the right-hand side when overlapping occurs. An example of their translation is as follows:
His approach is free from the type-safety issue, though based on a more sophisticated row-polymorphic system. There are two sorts of predicates and three variants of record concatenation operators in his calculus, for example, demonstrating some sophistication of his calculus.
It is worth noting that neither Ohori’s nor Osinski’s calculus supports subtyping. This is a significant limitation since subtyping is a common feature in many popular languages, especially object-oriented languages.
6 Conclusion
The benefits from named arguments are twofold. On the one hand, argument keywords serve as extra documentation at the language level. On the other hand, they lay the foundation for supporting commutativity and optionality.
Named and optional arguments are widely supported in mainstream programming languages but are hardly formalized. Our approach is inspired by existing mechanisms in OCaml and Haskell but further considers the interaction between first-class named arguments and subtyping. Static type checkers for Python and Ruby both suffer from a type-safety issue in this regard. We show that \(\lambda _\textsf{iu}\) can serve as a type-safe core calculus with compact support for intersection and union types.
We hope that this paper will call more attention to the foundation for named and optional arguments and inspire future language developers to consider potential type-safety issues more carefully in their designs.
Future Work. A natural extension of our work is to support omitting keywords if the order of arguments is not changed from how they are defined. In other words, this is a version without the property of distinctness as classified in Table 1. The syntactic approach employed by Scala can be a good reference. Another interesting direction is to evaluate our approach in a more practical setting, for example, by typing popular libraries like TensorFlow, where named and optional arguments are ubiquitous, and dependent default values can help simplify the functions and avoid some ill-defined parameter combinations.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
in this paper) is used to concatenate multiple single-field records to form multi-field records, reminiscent of Forsythe [24]. For example,
forms a two-field record from two single-field records.
.
.
.
. The 
is not equivalent to
because the former contains more information that prevents
and
implies a coercion function from subtype to supertype. In CP, such coercions are implicitly inserted to remove the forgotten fields (e.g. 
operator to examine the runtime type, which is generally known as type introspection and is similar to the type-based switch. C# also provides the null coalescing operator 
operator is the standard way to perform type introspection in TypeScript, and the type of 
to
in the true-branch. We assume the call sites have been rewritten in the code above. In this manner, named and optional arguments can be added to TypeScript as syntactic sugar.
, type-based switch expressions \(\textbf{switch} \, e_{{\textrm{0}}} \, \textbf{as} \, x \, \textbf{case} \, A \Rightarrow e_{{\textrm{1}}} \, \textbf{case} \, B \Rightarrow e_{{\textrm{2}}} \), and let-in bindings \( letin \, e \). The syntax of \( letin \) is as follows:The composition of two let-in bindings is denoted by \( letin_{{\textrm{1}}} \circ letin_{{\textrm{2}}} \), and an empty binding is denoted by \(\textbf{id}\).
reduces to \(\{ x = 1 \} . x \) via projective dispatch to select the needed field.
is generated for the default value of 
in syntax and is implemented as a new built-in type in Racket. Keyword arguments are supported by replacing
,
, and the core application form with newly defined macros that recognize keyword-argument forms. Here is an example of a function 
. The first list contains the required arguments (
and
), and the second list contains the optional ones (
). However, Typed Racket does not provide a typed version of
, and it is unclear how to properly type it.
, which allows overlapping fields with the same types and prefers the fields on the right-hand side when overlapping occurs. An example of their translation is as follows: 
