Introduction
The lambda calculus [7 ] provides a foundational model for computation and serves as the theoretical basis for modern functional programming languages. A lambda abstraction λ x . e \lambda x.e λ x . e x x x e e e β \beta β ( λ x . e 1 ) e 2 ⟶ e 1 [ e 2 / x ] (\lambda x.e_1)\ e_2 \longrightarrow e_1[e_2/x] ( λ x . e 1 ) e 2 ⟶ e 1 [ e 2 / x ]
However, managing variable bindings remains a classic challenge in language implementation, reasoning, and mechanization. In particular, ensuring variable freshness can be quite tricky. While paper formalisms and pen-and-paper proofs often assume α \alpha α [10 ] to define capture-avoiding substitution. De Bruijn indices, however, are famously difficult to formalise and implement correctly. Moreover, substitution and de Bruijn indices are often inefficient because reduction requires a traversal of the expression body. Finally, β \beta β named arguments , which allow arguments to be supplied by explicit parameter names.
In this paper, we show how standard record types can be leveraged to model first-class environments [17 , 34 , 37 ] and function arguments, establishing an environment-based model that sidesteps traditional binding and inefficiency issues while capturing diverse function application paradigms. Our design is remarkably simple and principled; it uncovers subtle interactions that emerge when combining features and provides a general framework for function application paradigms by exploiting inherent record properties.
We offer the following contributions:
Authors’ Contact Information: Matthew Toohey, University of Toronto, Toronto, Canada, mtoohey@cs.toronto.edu; Ara Jamalzadeh, University of Toronto, Toronto, Canada, a.jamalzadeh@mail.utoronto.ca; Ningning Xie, University of Toronto, Toronto, Canada, ningningxie@cs.toronto.edu.
Formalisation: We formalise this design as a core record calculus, λ ρ + \lambda^{\rho+} λ ρ + § 3 ). We establish key structural properties of its record operators (Lemmas 3.1 –3.6 ), determinacy (Theorem 3.7 ), type soundness (Theorems 3.8 and 3.9 ), and normalization (Theorem 3.11 ). We also prove that it simulates the simply typed lambda calculus (Theorems 3.14 and 3.15 ).
Imperative extension: We extend the calculus with mutable references, under which the precise behaviour of function application becomes important (§ 6 ). To safely handle type generalization in the presence of side-effects, we adopt the approach of Dolan [ [13 ] and adapt it to closures and applications.
Mechanization: The calculus, including its operational semantics and all stated lemmas and theorems, is fully mechanized in the Lean 4 proof assistant (§ 7 ). The complete proof artifact is provided in the supplementary materials.
Implementation: We implement an interpreter for λ ρ + \lambda^{\rho+} λ ρ + Theorem 5.1 ).
Lastly, we explore the broader design space in § 8 .
Overview
This section provides an overview of our design. We frequently draw on examples from various programming languages, ensuring the specific language is clear from the context. For further clarity, programs written in our own syntax are enclosed in gray boxes.
The Lambda Calculus with the Substitution Model
Functions, or lambdas, are the core abstraction in the lambda calculus [7 ] . Its two fundamental rules, governing typing and evaluation respectively, are presented below:
Γ , x : A ⊢ e : B Γ ⊢ λ x . e : A → B L A M ( λ x . e 1 ) e 2 ⟶ e 1 [ e 2 / x ] B E T A \frac{\Gamma, x : A \vdash e : B}{\Gamma\vdash\lambda x.e : A \to B}\quad\mathrm{LAM}
\qquad
(\lambda x.e_1)\ e_2 \longrightarrow e_1[e_2/x]\quad\mathrm{BETA} Γ ⊢ λ x . e : A → B Γ , x : A ⊢ e : B LAM ( λ x . e 1 ) e 2 ⟶ e 1 [ e 2 / x ] BETA Rule LAM type-checks a function by extending the typing context Γ \Gamma Γ e e e A → B A \to B A → B BETA substitutes the variable x x x e 2 e_2 e 2 e 1 e_1 e 1
However, while these two rules are standard in presenting the lambda calculus, they are not without issues. We discuss below some of the challenges of reasoning about and implementing them.
Reasoning about bindings. Reasoning about variable bindings is notoriously difficult, as substitution complicates the metatheory. The substitution function e 1 [ e 2 / x ] e_1[e_2/x] e 1 [ e 2 / x ] λ y . e \lambda y.e λ y . e x x x y y y e 2 e_2 e 2
To manage bindings, it is common to assume the alpha-convention, where a bound variable can be renamed at any point to ensure its freshness. While this convention is standard in the literature, it does not directly yield a straightforward algorithm for implementation or mechanization.
Another well-known alternative is the use of de Bruijn indices [10 ] , where variables are represented as natural numbers pointing to their corresponding binding sites. However, it is widely acknowledged that implementing and reasoning about shifting, the key operator in de Bruijn indices used to adjust binding numbers during substitution, can be error-prone and non-trivial.
Inefficiency of the substitution model. Another issue is that the substitution model is highly inefficient. Every substitution requires a full traversal of the expression, a process that becomes exceptionally expensive for functions with large bodies. Worse, nested applications trigger this substitution process multiple times, leading to a compounding cost.
Due to this inherent inefficiency, practical languages do not implement beta-reduction using the substitution model. Instead, it is much more common to utilize an environment-based model . Rather than eagerly rewriting the function body every time a variable is bound, the system maintains an environment that maps variable names to their actual values. Consequently, when a function is applied to an argument, the language simply adds that variable-value pairing to the current environment and proceeds to evaluate the function body. By avoiding substitution, an environment-based model also simplifies the metatheory [37 §2.2 and §4.1] .
In the literature, a body of work has focused on modelling environments, ranging from calculi with explicit substitutions [1 , 3 , 8 ] to the study of first-class environments [17 , 34 , 37 ] .
Missing function application paradigms. Furthermore, the vanilla lambda calculus does not natively support various function application paradigms common in practical programming languages. For example, many languages support named arguments , which significantly enhance programming convenience by allowing arguments to be provided with explicit names. To illustrate, consider a function written in Python syntax:
def transfer_funds(amount, from_account, to_account): ...When a programmer wants to call this function using standard positional arguments, they must remember the exact order of the parameters:
transfer_funds(1000, "Alice", "Bob")Without looking up the function’s definition, this code is difficult to read and highly error-prone. If a developer accidentally swaps "Alice" and "Bob", the code will still execute, but the funds will be transferred from and to the wrong person.
Languages that support named arguments, such as Python, allow programmers to specify the name of the parameter directly alongside the value at the call site:
transfer_funds(amount=1000, from_account="Alice", to_account="Bob")This way, it becomes immediately clear from the call site which account is transferring to which. Named arguments represent one example of function application paradigms; other important examples include, e.g. optional arguments, which we will discuss further in subsequent sections.
First-Class Environments as Records
In this paper, we develop an environment-based model for the lambda calculus by representing environments as records. This perspective is motivated by the close similarity between a typing context Γ \Gamma Γ ρ \rho ρ L A M \mathsf{LAM} LAM T - L A M \mathsf{T\text{-}LAM} T - LAM
record type ρ : : = ε ∣ ρ , i ▹ A \text{record type}\quad\rho::= \varepsilon\mid\rho, i \triangleright A record type ρ ::= ε ∣ ρ , i ▹ A ρ , i ▹ A ⊢ e : B ρ ⊢ λ i . e : A → B T - L A M \frac{\rho, i \triangleright A \vdash e : B}{\rho\vdash\lambda i.e : A \to B}\ \mathsf{T\text{-}LAM} ρ ⊢ λi . e : A → B ρ , i ▹ A ⊢ e : B T - LAM Records are typically expected to be commutative, a property usually captured by a subtyping rule that permutes fields. Under this view, for example, { name : String , age : Int } \{\,\text{name}:\text{String},\ \text{age}:\text{Int}\,\} { name : String , age : Int } { age : Int , name : String } \{\,\text{age}:\text{Int},\ \text{name}:\text{String}\,\} { age : Int , name : String } T - V A R \mathsf{T\text{-}VAR} T - VAR i ∈ ρ i \in\rho i ∈ ρ i i i
ρ , i ▹ A ⊢ i : A T - V A R \frac{\rho, i \triangleright A \vdash i : A}{\mathsf{T\text{-}VAR}} T - VAR ρ , i ▹ A ⊢ i : A Closures. Similarly, during evaluation, an environment record value o o o
record value o : : = ε ∣ o , i = v o ⊢ λ i . e ⟶ ⟨ o ∣ λ i . e ⟩ E-lam \text{record value }o ::= \varepsilon\mid o,i=v
\qquad
o \vdash\lambda i.\,e \longrightarrow\langle o \mid\lambda i.\,e\rangle
\quad\text{E-lam} record value o ::= ε ∣ o , i = v o ⊢ λi . e ⟶ ⟨ o ∣ λi . e ⟩ E-lam When the closure is applied to an argument, the function body e e e o o o i i i
First-class environments. With first-class environments [17 , 34 , 37 ] , we can treat environments as first-class objects that can be directly manipulated. For example, we can introduce an operator @ that reifies the environment into a record, with the typing rule \rho\vdash@ : \{\rho\} and the evaluation rule o \vdash@ \longrightarrow\{o\} . We can then apply record operators, such as projection, to the environment. In particular, a variable i i i i i i i i i e 1 ▶ e 2 e_1 \blacktriangleright e_2 e 1 ▶ e 2 e 2 e_2 e 2 e 1 e_1 e 1
As demonstrated by Tan and Oliveira [ [37 ] , first-class environments are useful for modelling first-class modules [5 ] , sandboxed modules, and object capabilities [25 , 26 ] . Our representation of environments as records naturally supports these paradigms, since record objects are themselves first-class.
Named Arguments as Records
Having observed how function applications with named arguments operate in our transfer_funds example, another natural perspective we take is to represent function arguments as records. That is, functions are now typed as { ρ } → A \{\rho\} \to A { ρ } → A c c c
record pattern c : : = ε ∣ c , i c : ρ 2 ρ 1 , ρ 2 ⊢ e : A ρ 1 ⊢ λ { c } . e : { ρ 2 } → A T-lam2 \begin{aligned}
&\text{record pattern }c ::= \varepsilon\mid c,i \\
&c : \rho_2 \qquad\rho_1,\rho_2 \vdash e : A \\
&\rho_1 \vdash\lambda\{c\}.\,e : \{\rho_2\} \to A
\end{aligned}
\qquad\text{T-lam2} record pattern c ::= ε ∣ c , i c : ρ 2 ρ 1 , ρ 2 ⊢ e : A ρ 1 ⊢ λ { c } . e : { ρ 2 } → A T-lam2 Here, the record pattern c c c ρ 2 \rho_2 ρ 2 c c c ρ 1 , ρ 2 \rho_1,\rho_2 ρ 1 , ρ 2 ρ 2 \rho_2 ρ 2 ρ 1 \rho_1 ρ 1
As an example, we can define transfer_funds as follows:
λ{ amount, from_account, to_account }. ...Function applications can now provide records as named arguments at the call site. For example, the previous example can be written as:
transfer_funds { amount=1000, from_account="Alice", to_account="Bob" }Thanks to record commutativity, this is equivalent to the following expression, as is desired:
transfer_funds { to_account="Bob", from_account="Alice", amount=1000 }Shadowing in first-class environments. One may wonder what happens when ρ 1 \rho_1 ρ 1 ρ 2 \rho_2 ρ 2 [21 ] ), which, as we represent environments as records, arise naturally in an environment when shadowing occurs. Duplicate labels are non-commutative with respect to each other, while remaining commutative with different labels. Specifically, projecting a duplicate label from a record returns the rightmost corresponding field (unlike [21 ] , which always returns the leftmost one). For example, { i = 2 , i = 1 } . i \{i=2,\ i=1\}.i { i = 2 , i = 1 } . i 1 1 1 ( i = 2 , i = 1 \ i ) . i ({i=2, i=1}\backslash i).i ( i = 2 , i = 1 \ i ) . i \ i \backslash i \ i i i i i i i i i i
The interpretation that projecting a duplicate label retrieves the rightmost corresponding field directly coincides with the fact that new variables are always appended to the right of an environment (as in rule T-LAM2), thus shadowing prior ones. Therefore, our previous syntactic sugar @.i for variable lookup still holds, as it accesses the latest i i i ( @ \ i ) . i (@\backslash i).i ( @\ i ) . i
Argument Labels and Parameter Names
We can further separate external argument labels , used at the call site, from internal parameter names , used within the function definition. This distinction allows a function call to read like a sentence, while keeping the function definition itself clear and logical.
The following Swift program, adapted from its official documentation, illustrates this distinction between argument labels and parameter names (the -> String annotation specifies the return type):
func greet(person: String, from hometown: String) -> String {
"Hello \(person) from \(hometown)."
}Here, person and hometown bind to the parameters within the function body, while from serves as the argument label used at the call site. We can then call the function as:
greet(person: "Alice", from: "Mars") // "Hello Alice from Mars"To support the distinction between argument labels and parameter names, we can generalize both record patterns and the typing rule T-LAM2 to rule T-LAM3:
record pattern c : : = ε ∣ c , i 1 ⋄ i 2 c : ρ 2 ⊙ ρ 3 ρ 1 , ρ 3 ⊢ e : A ρ 1 ⊢ λ { c } . e : { ρ 2 } → A \begin{aligned}
\text{record pattern}\quad c &::= \varepsilon\mid c, i_1 \mathbin{\diamond} i_2 \\
c &: \rho_2 \mathbin{\odot} \rho_3 \qquad\rho_1,\rho_3 \vdash e : A \\
\rho_1 &\vdash\lambda\{c\}.e : \{\rho_2\} \to A
\end{aligned} record pattern c c ρ 1 ::= ε ∣ c , i 1 ⋄ i 2 : ρ 2 ⊙ ρ 3 ρ 1 , ρ 3 ⊢ e : A ⊢ λ { c } . e : { ρ 2 } → A Here, the record pattern c c c ⋄ \diamond ⋄ ⊙ \odot ⊙ ρ 2 \rho_2 ρ 2 ρ 3 \rho_3 ρ 3 i 1 ⋄ i 2 i_1 \diamond i_2 i 1 ⋄ i 2 i 1 ▹ I n t i_1 \mathbin{\triangleright} \mathrm{Int} i 1 ▹ Int i 2 ▹ I n t i_2 \mathbin{\triangleright} \mathrm{Int} i 2 ▹ Int ρ 2 \rho_2 ρ 2 ρ 3 \rho_3 ρ 3 e e e § 3.2 additionally performs generalization over the function type; we omit this here for simplicity.
We can now express the example as follows, assuming string interpolation:
λ{ person, from ⋄ hometown }. "Hello \(person) from \(hometown)."For clarity, we often omit the argument label (e.g. person) when it is identical to the parameter name.
Positional Arguments
The design so far requires every argument to be named. However, positional arguments remain valuable when parameter roles are intuitive enough that explicit labels would only add visual noise. For instance, a function sub(x, y) is naturally expected to compute (x − y) rather than (y − x).
Languages that support named arguments often provide mechanisms for positional arguments as well. In Swift, for example, function arguments are named at the call site by default. When an argument label is unnecessary, Swift developers can use an underscore (_) as the argument label, for example, one can define sub in Swift as the following:
func sub(_ a: Int, _ b: Int) -> Int { a - b }Here the underscores indicate that the function can be called with positional arguments. This allows the argument labels to be omitted at the call site, e.g. sub(8, 3).
It turns out we can naturally support positional arguments using duplicate labels (§ 2.3 ). Specifically, by treating the underscore (_) as a normal field label, we can define sub as
s u b = λ { _ ⋄ a , _ ⋄ b } . a − b \mathsf{sub} = \lambda\{ \_ \diamond a, \_ \diamond b \}. a - b sub = λ { _ ⋄ a , _ ⋄ b } . a − b The positional application sub { 8 , 3 } \{8, 3\} { 8 , 3 } { _ = 8 , _ = 3 } \{\_ = 8, \_ = 3\} { _ = 8 , _ = 3 } { _ = 8 , _ = 3 } \{\_ = 8, \_ = 3\} { _ = 8 , _ = 3 }
Mixing named and positional arguments. By interpreting positional arguments as normal records with duplicate labels, our design interprets positional arguments as simply a special case of named arguments. As noted, non-duplicate labels are commutative, while duplicate labels (including the dedicated label for positional arguments) are non-commutative with respect to each other (thus preserving the significance of their order), yet remain commutative with other labels.
As an example, if div is defined with a named dividend and a positional divisor:
d i v = λ { d i v i d e n d , _ ⋄ d i v i s o r } . d i v i d e n d / d i v i s o r \mathsf{div} = \lambda\{ \mathsf{dividend},\ \_ \diamond\mathsf{divisor} \}. \mathsf{dividend} / \mathsf{divisor} div = λ { dividend , _ ⋄ divisor } . dividend / divisor then both (div { d i v i d e n d = 4 , 2 } \{\mathsf{dividend}=4, 2\} { dividend = 4 , 2 } { 2 , d i v i d e n d = 4 } \{2, \mathsf{dividend}=4\} { 2 , dividend = 4 } { 4 , 2 } \{4, 2\} { 4 , 2 }
Our design preserves simplicity by, like Swift, requiring arguments to be declared as named or positional (simply using a dedicated label) in the function definition, making the system easy to reason about. But unlike Swift, which requires the order of arguments at the call site to strictly match the order defined in the function declaration, our system ensures commutativity between distinct labels, allowing for expressive order mixing at the call site. This is particularly useful when combined with partial application, which we discuss below.
Partial Application
So far, we have assumed that all arguments are passed together in a single record. We now generalize this behaviour to support partial application, where only a subset of the arguments are provided at the call site. Partial application is particularly flexible when combined with named arguments and commutativity. For example, consider a function drop that takes a count and a list, and drops count elements from the list. We can fix the list argument and define a specialized dropN function simply by writing drop { l i s t = [ ’a’ , ’b’ , ’c’ , ’d’ ] } \{\mathsf{list} = [\text{'a'}, \text{'b'}, \text{'c'}, \text{'d'}]\} { list = [ ’a’ , ’b’ , ’c’ , ’d’ ]}
To achieve partial application, we introduce the following typing rule for function application:
ρ ⊢ e 1 : { ρ 1 } → A ρ ⊢ e 2 : { ρ 2 } ρ 1 ∙ ρ 2 ⇝ ρ 3 ρ ⊢ e 1 e 2 : { ρ 3 } → A T - A P P \frac{\rho\vdash e_1 : \{\rho_1\} \to A \qquad\rho\vdash e_2 : \{\rho_2\} \qquad\rho_1 \bullet\rho_2 \rightsquigarrow\rho_3}{\rho\vdash e_1\ e_2 : \{\rho_3\} \to A}\ \mathrm{T\text{-}APP} ρ ⊢ e 1 e 2 : { ρ 3 } → A ρ ⊢ e 1 : { ρ 1 } → A ρ ⊢ e 2 : { ρ 2 } ρ 1 ∙ ρ 2 ⇝ ρ 3 T - APP Here, the function e 1 e_1 e 1 ρ 1 \rho_1 ρ 1 e 2 e_2 e 2 ρ 2 \rho_2 ρ 2 ρ 1 ∙ ρ 2 ⇝ ρ 3 \rho_1 \bullet\rho_2 \rightsquigarrow\rho_3 ρ 1 ∙ ρ 2 ⇝ ρ 3 ρ 3 \rho_3 ρ 3 ρ 2 \rho_2 ρ 2 ρ 1 \rho_1 ρ 1 { ρ 3 } → A \{\rho_3\} \to A { ρ 3 } → A
This rule can be refined in several ways. First, if ρ 2 \rho_2 ρ 2 ρ 2 ≠ ε \rho_2 \ne\varepsilon ρ 2 = ε ρ 3 \rho_3 ρ 3 { } → A \{\} \to A { } → A A A A § 2.7 .
We now extend the evaluation rules to support partial application. Specifically, we extend closures to keep track of two record values: one for the environment, and the other for the arguments accumulated so far. This behaviour is captured by the following rules:
o ⊢ λ { c } . e ⟶ ⟨ o ; ε ∣ λ { c } . e ⟩ E - L A M 2 o \vdash\lambda\{c\}.e \longrightarrow\langle o;\varepsilon\mid\lambda\{c\}.e\rangle\quad\mathrm{E\text{-}LAM}_{2} o ⊢ λ { c } . e ⟶ ⟨ o ; ε ∣ λ { c } . e ⟩ E - LAM 2 ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ { o 3 } ⟶ ⟨ o 1 ; o 2 , o 3 ∣ λ { c } . e ⟩ E - A P P \langle o_1;o_2 \mid\lambda\{c\}.e\rangle\{o_3\} \longrightarrow\langle o_1;o_2,o_3 \mid\lambda\{c\}.e\rangle\quad\mathrm{E\text{-}APP} ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ { o 3 } ⟶ ⟨ o 1 ; o 2 , o 3 ∣ λ { c } . e ⟩ E - APP When a function abstraction evaluates to a closure, it initializes an empty record ε \varepsilon ε § 2.7 ).
Optional Arguments
In many programming languages, the developer can specify a default value for parameters. For example, we may want to define an exponential function that squares its input by default:
power = λ{ base, exponent := 2 }. base ** exponent
Calling (power { base=3 }) returns 9, while calling (power { base=3, exponent=3 }) returns 27. We refer to arguments with default values as optional arguments , as they can be omitted at the call site, while other parameters are considered required arguments .
Integrating optional arguments into the record pattern is straightforward; we extend c c c v v v
record pattern c : : = ε ∣ c , i 1 ⋄ i 2 ∣ c , i 1 ⋄ i 2 : = v \text{record pattern}\quad c ::= \varepsilon\mid c, i_1 \diamond i_2 \mid c, i_1 \diamond i_2 := v record pattern c ::= ε ∣ c , i 1 ⋄ i 2 ∣ c , i 1 ⋄ i 2 := v We now discuss the typing and evaluation rules for optional arguments.
Typing optional arguments. Since functions with optional arguments such as power can be called with only the required arguments or with optional arguments overwriting the default values, their type signatures must reflect both arities, so that both (power { base=3, exponent=3 }) and (power { base=3 }) type-check and saturate the application.
To this end, we introduce optional types in record types:
record type ρ : : = ε ∣ ρ , i ⋆ A strength ⋆ : : = ▹ ∣ ? \text{record type}\quad\rho::= \varepsilon\mid\rho, i \mathbin{\star} A
\qquad
\text{strength}\quad\star::= \triangleright\mid? record type ρ ::= ε ∣ ρ , i ⋆ A strength ⋆ ::= ▹ ∣ ? A record field i i i strength ⋆ \star ⋆ strong (▹ \triangleright ▹ optional (?). When used in function argument types, (▹ \triangleright ▹ ⊙ \odot ⊙ c c c ρ 2 \rho_2 ρ 2
{ base ▹ Int , exponent ? Int } → Int \{\, \text{base} \triangleright\text{Int},\ \text{exponent} ? \text{Int} \,\} \to\text{Int} { base ▹ Int , exponent ? Int } → Int The type indicates that base is a required argument while exponent is an optional argument.
To type-check function applications such as (power {base=3, exponent=3}) and (power {base=3 }), we introduce subtyping rules between records. Importantly, the subtyping relation includes the following two rules (omitting other rules such as reflexivity):
[ ρ ] ? ε ≤ ρ S-EMPTY \frac{[\rho]?}{\varepsilon\leq\rho}
\qquad\text{S-EMPTY} ε ≤ ρ [ ρ ]? S-EMPTY ρ 0 ≤ ρ 1 , ρ 2 i ∉ ρ 1 A ≤ B i ▹ A , ρ 0 ≤ i ⋆ B , ρ 2 S-EXT \frac{\rho_0 \leq\rho_1,\rho_2 \qquad i \notin\rho_1 \qquad A \leq B}
{i \triangleright A,\rho_0 \leq i \star B,\rho_2}
\qquad\text{S-EXT} i ▹ A , ρ 0 ≤ i ⋆ B , ρ 2 ρ 0 ≤ ρ 1 , ρ 2 i ∈ / ρ 1 A ≤ B S-EXT In the first subtyping rule S-EMPTY, the premise [ ρ ] ? [\rho]? [ ρ ]? ρ \rho ρ i i i ▹ \triangleright ▹ ▹ \triangleright ▹
With these subtyping rules, we can derive two subtyping relations on the type of power. First,
{ base ▹ Int , exponent ? Int } → Int ≤ { base ▹ Int , exponent ▹ Int } → Int . \{\, \text{base} \triangleright\text{Int},\ \text{exponent} ? \text{Int} \,\} \to\text{Int}
\;\leq\;
\{\, \text{base} \triangleright\text{Int},\ \text{exponent} \triangleright\text{Int} \,\} \to\text{Int}. { base ▹ Int , exponent ? Int } → Int ≤ { base ▹ Int , exponent ▹ Int } → Int . This relation holds because
{ base ▹ Int , exponent ▹ Int } ≤ { base ▹ Int , exponent ? Int } \{\, \text{base} \triangleright\text{Int},\ \text{exponent} \triangleright\text{Int} \,\}
\;\leq\;
\{\, \text{base} \triangleright\text{Int},\ \text{exponent} ? \text{Int} \,\} { base ▹ Int , exponent ▹ Int } ≤ { base ▹ Int , exponent ? Int } by rule S-EXT. Thus power can take two arguments, allowing (power {base=3, exponent=3}) to type-check.
Second, we can derive: { base ▹ Int , exponent ? Int } → Int ⪯ { base ▹ Int } → Int \{\,\text{base} \triangleright\text{Int},\ \text{exponent}\ ?\ \text{Int}\,\} \to\text{Int} \preceq\{\,\text{base} \triangleright\text{Int}\,\} \to\text{Int} { base ▹ Int , exponent ? Int } → Int ⪯ { base ▹ Int } → Int { base ▹ Int } ⪯ { base ▹ Int , exponent ? Int } \{\,\text{base} \triangleright\text{Int}\,\} \preceq\{\,\text{base} \triangleright\text{Int},\ \text{exponent}\ ?\ \text{Int}\,\} { base ▹ Int } ⪯ { base ▹ Int , exponent ? Int }
Evaluation with optional arguments. We now discuss the evaluation rule for function application with optional arguments. A subtle aspect is that these default values can be overwritten at the call site. Therefore, we must distinguish between arguments that can be updated and those that cannot. To achieve this, we update record values as follows:
record value o : : = ε ∣ o , i = v ∣ o , i : v ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ { o 3 } ⟶ ⟨ o 1 ; o 2 + + o 3 ∣ λ { c } . e ⟩ E-APP2 \begin{aligned}
\text{record value } o &::= \varepsilon\mid o,i=v \mid o,i:v \\
&\langle o_1; o_2 \mid\lambda\{c\}.\,e\rangle\{o_3\} \longrightarrow\langle o_1; o_2 \mathbin{++} o_3 \mid\lambda\{c\}.\,e\rangle\qquad\text{E-APP2}
\end{aligned} record value o ::= ε ∣ o , i = v ∣ o , i : v ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ { o 3 } ⟶ ⟨ o 1 ; o 2 + + o 3 ∣ λ { c } . e ⟩ E-APP2 Here, i = v i=v i = v i : v i:v i : v i i i v v v
Consequently, the previous evaluation rule E-LAM2 can be straightforwardly updated to retrieve all default parameters from the record pattern c c c i : v i:v i : v o 2 + + o 3 o_2 ++ o_3 o 2 + + o 3 ( o 2 , o 3 ) (o_2,o_3) ( o 2 , o 3 ) o 3 o_3 o 3 o 2 o_2 o 2 ( i : 1 ) + + ( i = 2 ) (i:1) ++ (i=2) ( i : 1 ) + + ( i = 2 ) i = 2 i=2 i = 2
Partial application with optional arguments. Now that we have the ability to overwrite optional arguments, a natural question arises: is the following expression well-typed?
power { base = 3 } { exponent = 3 }In other words, is power { base=3 } a partially applied function that still waits for a potential value to overwrite the optional argument, or is it a saturated application (using the default value) that immediately returns the evaluation result 9 and therefore cannot accept more arguments?
Swift does not natively support partial application. On the other hand, OCaml, for example, requires a positional argument to appear after any optional arguments, so that it can determine when those optional arguments should be “erased” and replaced with their default values. If an optional argument is placed last, OCaml issues a warning as it cannot determine when the caller has finished providing arguments. In this case, OCaml would issue this warning for the definition of power.
Our design prioritizes simplicity by requiring an explicit construct, denoted as force, to deterministically trigger the evaluation of an expression once it has received all its arguments, as given by rule T-FORCE. The rule states that when an expression e e e { } \{\} { } → A \to A → A e e e A A A [23 ] , which distinguishes a computation from its thunk, where the thunk is a value that can be forced at any time. In our setting, a partially applied function can be viewed as always producing a value (since it merely accumulates arguments via the evaluation rule E-APP2), while its actual computation is only triggered by an explicit force.
ρ ⊢ e : { } → A ρ ⊢ f o r c e e : A T-FORCE \frac{\rho\vdash e : \{\} \to A}{\rho\vdash\mathop{\mathrm{force}} e : A} \qquad\text{T-FORCE} ρ ⊢ force e : A ρ ⊢ e : { } → A T-FORCE Now, (power { base=3 }) can be considered either a partially applied function, meaning that (power { base=3 } { exponent=3 }) is well-typed, or a saturated application. This works because, in either case, the actual computation has not yet occurred, and power { base=3 } simply evaluates to a closure ⟨ base = 3 , exponent : 2 ∣ λ { base , exponent } . base ∗ ∗ exponent ⟩ \langle\text{base}=3,\ \text{exponent}:2 \mid\lambda\{\text{base},\text{exponent}\}.\ \text{base} ** \text{exponent}\rangle ⟨ base = 3 , exponent : 2 ∣ λ { base , exponent } . base ∗ ∗ exponent ⟩
Optional Values
So far, we have developed a system that integrates named, positional, and optional arguments, introducing both optional types and the necessary subtyping rules to handle them properly. However, one aspect of this design remains somewhat unsatisfying: although we introduced the optional type ( i ? A ) (i ? A) ( i ? A ) { i ? I n t } → I n t \{i ? \mathsf{Int}\} \to\mathsf{Int} { i ? Int } → Int { i ? I n t } \{i ? \mathsf{Int}\} { i ? Int } ( f : { i ? I n t , i ? I n t } → I n t ) (f : \{i ? \mathsf{Int}, i ? \mathsf{Int}\} \to\mathsf{Int}) ( f : { i ? Int , i ? Int } → Int ) ( i ? I n t ) (i ? \mathsf{Int}) ( i ? Int ) i i i _ \_ _ 3 3 3 5 5 5
{ i ? I n t , i ? I n t } → I n t ≤ { i ▹ I n t } → I n t \{i ? \mathsf{Int}, i ? \mathsf{Int}\} \to\mathsf{Int} \mathrel{\leq} \{i \mathrel{\triangleright} \mathsf{Int}\} \to\mathsf{Int} { i ? Int , i ? Int } → Int ≤ { i ▹ Int } → Int This holds because { i ▹ I n t } ≤ { i ? I n t , i ? I n t } \{i \mathrel{\triangleright} \mathsf{Int}\} \mathrel{\leq} \{i ? \mathsf{Int}, i ? \mathsf{Int}\} { i ▹ Int } ≤ { i ? Int , i ? Int } ( i ▹ I n t ) (i \mathrel{\triangleright} \mathsf{Int}) ( i ▹ Int ) ( i ? I n t ) (i ? \mathsf{Int}) ( i ? Int ) ( i ? I n t ) (i ? \mathsf{Int}) ( i ? Int )
ϵ ≤ i ? I n t S-EMPTY i ▹ I n t ≤ i ? I n t , i ? I n t S-EXT \begin{aligned}
\epsilon&\mathrel{\leq} i ? \mathsf{Int} && \text{S-EMPTY}\\
i \mathrel{\triangleright} \mathsf{Int} &\mathrel{\leq} i ? \mathsf{Int}, i ? \mathsf{Int} && \text{S-EXT}
\end{aligned} ϵ i ▹ Int ≤ i ? Int ≤ i ? Int , i ? Int S-EMPTY S-EXT Now, because ( f : { i ▹ I n t } → I n t ) (f : \{i \mathrel{\triangleright} \mathsf{Int}\} \to\mathsf{Int}) ( f : { i ▹ Int } → Int ) ( f { i = 1 } ) (f\ \{i = 1\}) ( f { i = 1 }) 1 1 1 ( f { i = 1 } ) (f\ \{i = 1\}) ( f { i = 1 }) i i i i i i f f f ( i = 1 , i : 5 ) (i=1, i:5) ( i = 1 , i : 5 ) ( i : 3 , i = 1 ) (i:3, i=1) ( i : 3 , i = 1 )
To resolve this issue, we extend record values to introduce optional values , written as i ? i ? i ?
record value o : : = ϵ ∣ o , i = v ∣ o , i : v ∣ o , i ? \text{record value}\quad o \mathrel{::=} \epsilon\mid o, i = v \mid o, i : v \mid o, i ? record value o ::= ϵ ∣ o , i = v ∣ o , i : v ∣ o , i ? Notably, an optional value ( i ? ) (i ?) ( i ?) not carry a concrete value for i i i { i ? A } \{i ? A\} { i ? A }
An optional value like { i ? } \{i ?\} { i ?} i i i i i i f f f
f { i ? , i = 1 } f\ \{i ?, i = 1\} f { i ? , i = 1 } In this case, the application leaves the first i i i i i i 1 1 1 ( o 2 ⊕ o 3 ) (o_2 \mathbin{\oplus} o_3) ( o 2 ⊕ o 3 ) o 2 o_2 o 2 ( i : 3 , i : 5 ) ⊕ ( i ? , i = 1 ) (i:3, i:5) \mathbin{\oplus} (i ?, i = 1) ( i : 3 , i : 5 ) ⊕ ( i ? , i = 1 ) ( i : 3 , i = 1 ) (i:3, i = 1) ( i : 3 , i = 1 ) f f f ( i : 3 , i = 1 ) (i:3, i=1) ( i : 3 , i = 1 ) undefined in JavaScript and TypeScript, where a default parameter is used if an argument is explicitly passed as undefined .
Overwriting Arguments
In the record typing literature, approaches to handling duplicate labels generally fall into two camps. The first employs scoped labels [21 ] , where both fields coexist in the record, but one shadows the other. The second employs overwriting [32 ] , where extending a record with an existing label overwrites the previous field. In our current formalism, duplicate labels correspond to the scoped approach. On the other hand, the behaviour of overwriting an optional argument closely resembles the latter camp.
Taking this observation further, it turns out that we can unify both approaches within our formalism by allowing record fields to specify whether they are overwritable. This design offers the benefit that it subsumes optional arguments as simply a special case of the unified design. Moreover, to our knowledge, this is the first system to combine scoped labels and overwriting labels, where all labels permit duplicates within a record, with overwriting behaviour managed via fine-grained, field-level specifications.
Specifically, we extend record types one final time to introduce the weak strength:
record type ρ : : = ε ∣ ρ , i ⋆ A strength ⋆ : : = ▹ ∣ : ∣ ? \text{record type }\rho::= \varepsilon\mid\rho, i \mathbin{\star} A \qquad\text{strength }\star::= \mathbin{\triangleright} \mid: \mid? record type ρ ::= ε ∣ ρ , i ⋆ A strength ⋆ ::= ▹ ∣:∣ ? Here, (▹ \mathbin{\triangleright} ▹ weak , that denotes an overwritable field.
Conveniently, we have already introduced weak values ( i : v ) (i : v) ( i : v ) § 2.7 , which we used there to represent default values that can be overwritten at runtime. Therefore, the definition of record values from § 2.8 (which previously incorporated optional values) serves as our final formulation.
Altogether, our system in its final form features three record strengths, along with their corresponding forms of record values. First, ( i = v ) (i = v) ( i = v ) ( i ▹ A ) (i \mathbin{\triangleright} A) ( i ▹ A ) ( i ? ) (i ?) ( i ?) ( i ? A ) (i ? A) ( i ? A ) ( i : v ) (i : v) ( i : v ) ( i : A ) (i : A) ( i : A ) § 3 formally defines the static and dynamic semantics of records. In particular, core operations, including application and concatenation, are systematically defined based on record strengths.
Introducing the weak strength offers several benefits. First, it shifts the decision of whether to overwrite or bind a parameter from the parameters to the arguments . Under this mechanism, functions only require parameters of strength (:). Thus, the separation operator ( c : ρ 2 ⊙ ρ 3 ) (c : \rho_2 \mathbin{\odot} \rho_3) ( c : ρ 2 ⊙ ρ 3 ) ρ 2 \rho_2 ρ 2 ρ 3 \rho_3 ρ 3
We can also simplify record patterns by removing patterns with default values, effectively returning to the definition in § 2.4 :
record pattern c : : = ε ∣ c , i 1 ⋄ i 2 \text{record pattern }c ::= \varepsilon\mid c, i_1 \mathbin{\diamond} i_2 record pattern c ::= ε ∣ c , i 1 ⋄ i 2 (from § 2.4 )
As an example, we can express the power function with a default exponent value of 2 simply as
power' = (λ{ base, exponent }. base ** exponent) { exponent : 2 }Here, the lambda has type { base : Int , exponent : Int } → Int {\{\,\text{base} : \operatorname{Int},\ \text{exponent} : \operatorname{Int}\,\} \to\operatorname{Int}} { base : Int , exponent : Int } → Int power' : { base : Int, exponent ? Int } → Int.
We can then apply, e.g. (power' {exponent : 3}) to overwrite the default value. Notably, since the argument is itself an overwritable field, the resulting expression can be further applied to overwrite the exponent value again. On the other hand, applying (power' {exponent = 2}) will fix the exponent parameter. That is, the argument decides whether it provides a (new) default value for the parameter, or fully fixes it.
Summary
We have discussed first-class environments represented via records, and demonstrated how records can also serve as function arguments, covering named, positional, and optional arguments, supported uniformly through three strengths over record types and values. Our design is certainly not the only viable one in the design space of function application paradigms. Indeed, different languages make different design choices, as we will discuss in § 8.1 . However, while many languages feature forms of named and optional arguments, their designs often exist only as implementation details rather than core formalisms.
The motivation for our formulation is threefold: first, to capture the core essence of these diverse paradigms and demonstrate how they can be expressed in a principled manner using familiar record types; second, to uncover the subtle interactions that arise when different features are combined; and third, to provide a framework that yields several advantages in terms of record commutativity, shadowing, and overwriting. The design also yields an intriguing record calculus by itself, naturally generalizing function application paradigms to general records such as optional and weak fields, which are useful for expressing various programs. Given that record types are widely utilized across various domains, we anticipate that our formulation can be inspiring in these areas as well; we expand on this discussion in § 8.2 .
A Record Calculus
This section presents the λ ϕ \lambda^{\phi} λ ϕ
Syntax
Figure 1 presents the syntax. Terms e e e n n n λ { c } . e \lambda\{c\}.e λ { c } . e ⟨ o 0 ; o 1 ∣ λ { c } . e ⟩ \langle o_0;o_1 \mid\lambda\{c\}.e\rangle ⟨ o 0 ; o 1 ∣ λ { c } . e ⟩ e 0 e 1 e_0\ e_1 e 0 e 1 force e \operatorname{force}\ e force e e 0 ▶ e 1 e_0 \blacktriangleright e_1 e 0 ▶ e 1 { r } \{r\} { r } e 0 + + e 1 e_0 \mathbin{++}e_1 e 0 + + e 1 e . i e.i e . i e . { i ‾ } e.\{ \overline{i} \} e . { i } e \ { i ‾ } e\backslash\{ \overline{i} \} e \ { i } let t = e 0 in e 1 \operatorname{let}\ t=e_0\ \operatorname{in}\ e_1 let t = e 0 in e 1 i i i
Figure 1. Syntax.
Record patterns c c c ε \varepsilon ε c , i ⋄ t c,i\diamond t c , i ⋄ t i i i t t t § 2 , here, it is either simply a parameter name i i i { c } \{c\} { c }
Records r r r ε \varepsilon ε r , i ⋆ e r,i\star e r , i ⋆ e r , i ? r,i? r , i ? ⋆ \star ⋆ = = = : : :
Values consist of natural numbers, as well as closures and records whose record entries are themselves values. Notably, they do not include lambdas, as we will discuss in § 3.6 .
\begin{aligned}
e &::= n \mid\lambda\{c\}.e \mid\langle o_0;o_1 \mid\lambda\{c\}.e\rangle\mid e_0\ e_1 \mid\operatorname{force}\ e \mid e_0 \blacktriangleright e_1 \mid@ \mid\{r\} \mid e_0 \mathbin{++}e_1 \mid e.i \mid e.\{\overline{i}\} \mid e\backslash\{\overline{i}\} \mid\operatorname{let}\ t=e_0\ \operatorname{in}\ e_1 && \text{term}\\
c &::= \varepsilon\mid c,i\diamond t && \text{record pattern}\\
t &::= i \mid\{c\} && \text{pattern}\\
r &::= \varepsilon\mid r,i\star e \mid r,i? && \text{record}\\
\star&::= = \mid: && \text{required strength}\\
v &::= n \mid\langle o_0;o_1 \mid\lambda\{c\}.e\rangle\mid\{o\} && \text{value}\\
o &::= \varepsilon\mid o,i\star v \mid o,i? && \text{record value}\\
A,B &::= a \mid\mathbb{N} \mid\{\rho\}\to A \mid\{\rho\} \mid\forall a.A && \text{type}\\
\rho&::= \varepsilon\mid\rho,i\star\tau&& \text{record type}\\
\tau&::= a \mid\mathbb{N} \mid\{\varrho\}\to\tau\mid\{\varrho\} && \text{monotype}\\
\varrho&::= \varepsilon\mid\varrho,i\star\tau&& \text{record monotype}
\end{aligned}
Types A A A a a a N \mathbb{N} N { ρ } → A \{\rho\} \to A { ρ } → A { ρ } \{\rho\} { ρ } ∀ a . A \forall a. A ∀ a . A ρ \rho ρ ε \varepsilon ε ( ρ , i ⋆ A ) (\rho, i \mathbin{\star} A) ( ρ , i ⋆ A ) ⋆ \star ⋆ ▹ \triangleright ▹ : : : ? ? ? τ \tau τ ϱ \varrho ϱ
As a notational convenience, we also allow the = = = ▹ \triangleright ▹ ( i = v ) : ( i = A ) (i = v) : (i = A) ( i = v ) : ( i = A ) ⋆ \star ⋆ ? ? ?
Typing
Figure 2 presents the typing rules of our calculus. The typing judgement ρ ⊢ e : A \rho\vdash e : A ρ ⊢ e : A ρ \rho ρ e e e A A A Figure 3 as well as auxiliary judgements in Figure 4 –Figure 6 , which we elaborate on after explaining the typing rules. During typing, we preserve the invariant that ρ \rho ρ ( : ) (:) ( : ) ⌊ ρ ⌋ \lfloor\rho\rfloor ⌊ ρ ⌋ … \dots …
Figure 2. Typing
Figure 3. Subtyping
Figure 4. Pattern separation
Figure 6. Concatenation
Rule T-SUB is the standard subsumption rule. Rule T-LAM uses record pattern separation (c : ρ 1 ⊙ ρ 2 c : \rho_1 \mathbin{\odot} \rho_2 c : ρ 1 ⊙ ρ 2 ρ 1 \rho_1 ρ 1 ρ 2 \rho_2 ρ 2 c c c a j ‾ \overline{a_j} a j § 6 . Rule T-CLOSURE type-checks the captured environment o 0 o_0 o 0 o 1 o_1 o 1 ⌊ ρ 1 ⌋ \lfloor\rho_1 \rfloor ⌊ ρ 1 ⌋ ρ 1 \rho_1 ρ 1 ρ 3 ∙ ρ 2 ↠ ρ 5 \rho_3 \mathbin{\bullet} \rho_2 \twoheadrightarrow\rho_5 ρ 3 ∙ ρ 2 ↠ ρ 5 § 6 , rule T-APP is straightforward. Rule T-FORCE eliminates a function type that expects an empty argument.
Rules T-BOX and T-ENV handle first-class environments, allowing records to be converted into environments and vice versa. Rule T-BOX also ensures that the entries of ρ 1 \rho_1 ρ 1
To type-check a record, rule T-RECORD delegates to the record typing judgement ρ 0 ⊢ r : ρ 1 \rho_0 \vdash r : \rho_1 ρ 0 ⊢ r : ρ 1 Figure 2 , which simply examines entries inductively. Rule T-CONCAT types record concatenation, where ρ 1 ⊕ ρ 2 ⇝ ρ 3 \rho_1 \oplus\rho_2 \leadsto\rho_3 ρ 1 ⊕ ρ 2 ⇝ ρ 3 T-PROJ , T-MPROJ , and T-DIFF follow a similar structure. Notably, all of them use required strengths, ensuring we can only project or subtract fields that actually exist.
Finally, T-LET first types e 0 e_0 e 0 t t t
Subtyping
The subtyping rules for types A ≤ B A \leq B A ≤ B S-QANTL handling type instantiation. Record subtyping ρ 0 ≤ ρ 1 \rho_0 \leq\rho_1 ρ 0 ≤ ρ 1 S-EMPTY allows a record type to be extended with entries at the end (as in § 2.7 ). The hypothesis ensures that all such entries must have optional strength. When applied to function arguments, this behaviour allows us to forget optional arguments, such that their defaults are used. This is a limited, inverted form of width subtyping: we omit the usual rule, which would allow arbitrary entries to be dropped (see § 8.2 ). Rule S-EMPTY has two important interactions with typing rules. First, it enables T-FORCE to expect a strictly empty argument list, instead of one containing an arbitrary amount of optional arguments. Second, it justifies why rules T-MPROJ and T-DIFF are restricted to fields with required strengths ⋆ \star ⋆ S-EMPTY could be applied to introduce ambiguity, where a label could refer to either an existing field or an optional one introduced by subtyping.
In rule S-EXT , the strengths ⋆ 0 \star_0 ⋆ 0 ⋆ 1 \star_1 ⋆ 1 i i i i i i ρ 1 \rho_1 ρ 1 i ∉ ρ 1 i \notin\rho_1 i ∈ / ρ 1 1 T-PROJ , T-MPROJ , and T-DIFF utilize this permutation behaviour (through subtyping) to ensure the entries they manipulate are positioned at the tail of the record types within their premises.
Lastly, strength subtyping ⋆ 0 ⪯ ⋆ 1 \star_0 \preceq\star_1 ⋆ 0 ⪯ ⋆ 1 : : : ? ? ? S-LT ). When considered from the perspective of function arguments, this allows us to discard the default value of an optional argument, thereby converting it into a required one. Strength subtyping does not relate ▹ \triangleright ▹
Pattern separation
The judgement c : ρ 0 ⊙ ρ 1 c : \rho_0 \mathbin{\odot} \rho_1 c : ρ 0 ⊙ ρ 1 ρ 0 \rho_0 ρ 0 ρ 1 \rho_1 ρ 1 c c c P-EXT is more interesting: it recurses on the record pattern c c c t : A ⊙ ρ 2 t : A \mathbin{\odot} \rho_2 t : A ⊙ ρ 2 t t t A A A ρ 2 \rho_2 ρ 2 ρ 0 \rho_0 ρ 0 i : A i : A i : A ρ 1 \rho_1 ρ 1 ρ 2 \rho_2 ρ 2 : : : t t t
P-LABEL guesses a type A A A ( i : A ) (i : A) ( i : A ) P-RECORD handles nested record patterns. As a simple example, i ⋄ { a g e ⋄ n } : ( i : { a g e : Nat } ) ⊙ ( n : Nat ) i \diamond\{ age \diamond n \} : (i : \{ age : \operatorname{Nat} \}) \mathbin{\odot} (n : \operatorname{Nat}) i ⋄ { a g e ⋄ n } : ( i : { a g e : Nat }) ⊙ ( n : Nat )
Application (Figure 5 ). The judgement ρ 0 ∙ ρ 1 ⇝ ρ 2 \rho_0 \mathbin{\bullet} \rho_1 \mathrel{\rightsquigarrow} \rho_2 ρ 0 ∙ ρ 1 ⇝ ρ 2 ρ 0 \rho_0 ρ 0 ρ 1 \rho_1 ρ 1 ρ 2 \rho_2 ρ 2 ρ 0 \rho_0 ρ 0 ρ 1 \rho_1 ρ 1
Figure 5. Application
These rules directly reflect the behaviour of strengths outlined in §2.9. Rule A-EMPTY is straightforward. Rules A-WEAKSTRONG and A-OPTIONALSTRONG handle cases where a strong argument is supplied, thereby eliminating the parameter from the resulting type. Otherwise, the parameter remains in some form via rule A-EXT , where its resulting strength is determined by a strength-specific variant of the judgement, ⋆ 0 ∙ ⋆ 1 ⇝ ⋆ 2 \star_0 \mathbin{\bullet} \star_1 \mathrel{\rightsquigarrow} \star_2 ⋆ 0 ∙ ⋆ 1 ⇝ ⋆ 2 A-LATER ), and becomes optional when provided with a weak argument (rule A-SET ). Finally, an optional parameter remains optional regardless of the argument’s strength in rules A-LEAVE and A-REPLACE .
Concatenation (Figure 6 ). The record concatenation judgement ρ 0 ⊕ ρ 1 ⇀ ρ 2 \rho_0 \mathbin{\oplus} \rho_1 \mathrel{\rightharpoonup} \rho_2 ρ 0 ⊕ ρ 1 ⇀ ρ 2 ρ 2 \rho_2 ρ 2 ρ 0 \rho_0 ρ 0 ρ 1 \rho_1 ρ 1 C-STRONGL always preserves a strong entry on the left; otherwise C-EXT combines the two strengths via ⋆ 0 ⊕ ⋆ 1 ⇀ ⋆ 2 \star_0 \mathbin{\oplus} \star_1 \mathrel{\rightharpoonup} \star_2 ⋆ 0 ⊕ ⋆ 1 ⇀ ⋆ 2 C-STRONGR ), an optional entry is overwritten (C-LATER ) or ignored when the left entry is weak (C-LEAVE ), and a weak entry replaces a matching weak entry (C-REPLACE ).
Example
To illustrate how application interacts with subtyping, consider the partial application
( λ { ⋄ i 0 , ⋄ i 1 } . @ . i 0 − @ . i 1 ) { _ = 2 } (\lambda\{\,\diamond\, i_0,\,\diamond\, i_1\}.@.i_0 - @.i_1)\{\,\_ = 2\} ( λ { ⋄ i 0 , ⋄ i 1 } .@. i 0 − @. i 1 ) { _ = 2 }
which supplies only the first of two positional arguments (we assume simple arithmetic operators and omit uninteresting derivation details). To type it, subtyping first adds an optional entry for the missing second argument through S-empty:
ε ⊢ { _ = 2 } : { _ ▹ N } T-record ⌊ _ ? N ⌋ ε ≤ _ ? N S-empty ⋯ _ ▹ N ≤ _ ▹ N , _ ? N S-ext { _ ▹ N } ≤ { _ ▹ N , _ ? N } S-record ε ⊢ { _ = 2 } : { _ ▹ N , _ ? N } T-sub \begin{aligned}
\varepsilon&\vdash\{\,\_ = 2\,\} : \{\,\_ \triangleright N\,\} && \text{T-record}\\
\lfloor\,\_ \mathbin{?} N\rfloor&&& \\
\varepsilon&\mathrel{\leq} \_ \mathbin{?} N && \text{S-empty}\\
\cdots&&& \\
\_ \triangleright N &\mathrel{\leq} \_ \triangleright N,\,\_ \mathbin{?} N && \text{S-ext}\\
\{\,\_ \triangleright N\,\} &\mathrel{\leq} \{\,\_ \triangleright N,\,\_ \mathbin{?} N\,\} && \text{S-record}\\
\varepsilon&\vdash\{\,\_ = 2\,\} : \{\,\_ \triangleright N,\,\_ \mathbin{?} N\,\} && \text{T-sub}
\end{aligned} ε ⌊ _ ? N ⌋ ε ⋯ _ ▹ N { _ ▹ N } ε ⊢ { _ = 2 } : { _ ▹ N } ≤ _ ? N ≤ _ ▹ N , _ ? N ≤ { _ ▹ N , _ ? N } ⊢ { _ = 2 } : { _ ▹ N , _ ? N } T-record S-empty S-ext S-record T-sub The application judgement then eliminates the first parameter but leaves the second one:
ε ∙ ε ⇝ ε A-empty _ : N ∙ _ ▹ N ⇝ ε A-weakStrong : ∙ ? ⇝ : A-later _ : N , _ : N ∙ _ ▹ N , _ ? N ⇝ _ : N A-ext \begin{aligned}
\varepsilon\mathbin{\bullet} \varepsilon&\mathrel{\rightsquigarrow} \varepsilon&& \text{A-empty}\\
\_ : N \mathbin{\bullet} \_ \triangleright N &\mathrel{\rightsquigarrow} \varepsilon&& \text{A-weakStrong}\\
: \mathbin{\bullet} \mathbin{?} &\mathrel{\rightsquigarrow} : && \text{A-later}\\
\_ : N,\,\_ : N \mathbin{\bullet} \_ \triangleright N,\,\_ \mathbin{?} N &\mathrel{\rightsquigarrow} \_ : N && \text{A-ext}
\end{aligned} ε ∙ ε _ : N ∙ _ ▹ N : ∙ ? _ : N , _ : N ∙ _ ▹ N , _ ? N ⇝ ε ⇝ ε ⇝ : ⇝ _ : N A-empty A-weakStrong A-later A-ext Finally, rule T-app combines the two, yielding a function that still expects the second argument:
ε ⊢ λ { ⋄ i 0 , ⋄ i 1 } . @ . i 0 − @ . i 1 : { _ : N , _ : N } → N T-lam ε ⊢ ( λ { ⋄ i 0 , ⋄ i 1 } . @ . i 0 − @ . i 1 ) { _ = 2 } : { _ : N } → N T-app \begin{aligned}
\varepsilon&\vdash\lambda\{\,\diamond\, i_0,\,\diamond\, i_1\}.@.i_0 - @.i_1 : \{\,\_ : N,\,\_ : N\,\} \to N && \text{T-lam}\\
\varepsilon&\vdash(\lambda\{\,\diamond\, i_0,\,\diamond\, i_1\}.@.i_0 - @.i_1)\{\,\_ = 2\,\} : \{\,\_ : N\,\} \to N && \text{T-app}
\end{aligned} ε ε ⊢ λ { ⋄ i 0 , ⋄ i 1 } .@. i 0 − @. i 1 : { _ : N , _ : N } → N ⊢ ( λ { ⋄ i 0 , ⋄ i 1 } .@. i 0 − @. i 1 ) { _ = 2 } : { _ : N } → N T-lam T-app The appendix contains further examples involving pattern separation and concatenation.
Evaluation
Figure 7 presents the operational semantics: ρ ⊢ e → e ′ \rho\vdash e \to e' ρ ⊢ e → e ′ e e e e ′ e' e ′ ρ \rho ρ
Figure 7. Operational semantics
First, rule E-lam evaluates lambdas into closures with an empty record of accumulated arguments. The current environment is captured inside the closure to preserve an important invariant: values (e.g. closures) are self-contained and do not depend on the surrounding scope. In rule E-app, the accumulated arguments in ρ 2 \rho_2 ρ 2 ρ 3 \rho_3 ρ 3
Closures are eliminated via rule E-forceClosure, which converts them into boxes. Here, the expand( c ; ρ 2 ) (c; \rho_2) ( c ; ρ 2 ) ρ 2 \rho_2 ρ 2 c c c e e e ρ 1 \rho_1 ρ 1 ρ 3 \rho_3 ρ 3
Rule E-boxr is the only rule that updates the evaluation environment. Specifically, the rule ignores the current environment ρ 0 \rho_0 ρ 0 e e e ρ 1 \rho_1 ρ 1
Finally, rules E-projRecord, E-mprojRecord, and E-diffRecord handle the basic record operations. Auxiliary meta-operations proj, mproj, and diff behave straightforwardly; their full definitions are omitted for brevity and included in the appendix. Mechanically, these notations traverse ρ 1 \rho_1 ρ 1
Desirable Properties and Type Soundness
In this section, we demonstrate that our calculus enjoys several desirable properties, which facilitate reasoning about system behaviour, and we then prove type soundness and normalization.
E-LAM
o ⊢ λ { c } . e ⟶ ⟨ o ; ε ∣ λ { c } . e ⟩ o \vdash\lambda\{c\}.e \longrightarrow\langle o;\varepsilon\mid\lambda\{c\}.e\rangle o ⊢ λ { c } . e ⟶ ⟨ o ; ε ∣ λ { c } . e ⟩ E-APPL
o ⊢ e 0 ⟶ e 0 ′ o ⊢ e 0 e 1 ⟶ e 0 ′ e 1 \frac{o \vdash e_0 \longrightarrow e_0'}{o \vdash e_0\ e_1 \longrightarrow e_0'\ e_1} o ⊢ e 0 e 1 ⟶ e 0 ′ e 1 o ⊢ e 0 ⟶ e 0 ′ E-APPR
o ⊢ e ⟶ e ′ o ⊢ v e ⟶ v e ′ \frac{o \vdash e \longrightarrow e'}{o \vdash v\ e \longrightarrow v\ e'} o ⊢ v e ⟶ v e ′ o ⊢ e ⟶ e ′ E-APP
o 0 ⊢ ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ { o 3 } ⟶ ⟨ o 1 ; o 2 + + o 3 ∣ λ { c } . e ⟩ o_0 \vdash\langle o_1;o_2 \mid\lambda\{c\}.e\rangle\{o_3\} \longrightarrow\langle o_1;o_2 \mathbin{++} o_3 \mid\lambda\{c\}.e\rangle o 0 ⊢ ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ { o 3 } ⟶ ⟨ o 1 ; o 2 + + o 3 ∣ λ { c } . e ⟩ E-FORCECLOSURE
expand ( c ; o 2 ) = o 3 o 0 ⊢ force ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ ⟶ { o 1 , o 3 } ▶ e \frac{\operatorname{expand}(c;o_2)=o_3}{o_0 \vdash\operatorname{force}\langle o_1;o_2 \mid\lambda\{c\}.e\rangle\longrightarrow\{o_1,o_3\}\mathbin{\blacktriangleright}e} o 0 ⊢ force ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ ⟶ { o 1 , o 3 } ▶ e expand ( c ; o 2 ) = o 3 E-BOXL
o ⊢ e 0 ⟶ e 0 ′ o ⊢ e 0 ▶ e 1 ⟶ e 0 ′ ▶ e 1 \frac{o \vdash e_0 \longrightarrow e_0'}{o \vdash e_0\mathbin{\blacktriangleright}e_1 \longrightarrow e_0'\mathbin{\blacktriangleright}e_1} o ⊢ e 0 ▶ e 1 ⟶ e 0 ′ ▶ e 1 o ⊢ e 0 ⟶ e 0 ′ E-BOXR
o 1 ⊢ e ⟶ e ′ o 0 ⊢ { o 1 } ▶ e ⟶ { o 1 } ▶ e ′ \frac{o_1 \vdash e \longrightarrow e'}{o_0 \vdash\{o_1\}\mathbin{\blacktriangleright}e \longrightarrow\{o_1\}\mathbin{\blacktriangleright}e'} o 0 ⊢ { o 1 } ▶ e ⟶ { o 1 } ▶ e ′ o 1 ⊢ e ⟶ e ′ E-BOX
o 0 ⊢ { o 1 } ▶ v ⟶ v o_0 \vdash\{o_1\}\mathbin{\blacktriangleright}v \longrightarrow v o 0 ⊢ { o 1 } ▶ v ⟶ v E-ENV
o \vdash@ \longrightarrow\{o\}
E-EXTL
o ⊢ { r } ⟶ { r ′ } o ⊢ { r , i ∗ e } ⟶ { r ′ , i ∗ e } \frac{o \vdash\{r\} \longrightarrow\{r'\}}{o \vdash\{r,i*e\} \longrightarrow\{r',i*e\}} o ⊢ { r , i ∗ e } ⟶ { r ′ , i ∗ e } o ⊢ { r } ⟶ { r ′ } E-EXTL?
o ⊢ { r } ⟶ { r ′ } o ⊢ { r , i ? } ⟶ { r ′ , i ? } \frac{o \vdash\{r\} \longrightarrow\{r'\}}{o \vdash\{r,i?\} \longrightarrow\{r',i?\}} o ⊢ { r , i ?} ⟶ { r ′ , i ?} o ⊢ { r } ⟶ { r ′ } E-EXTR
o 0 ⊢ e ⟶ e ′ o 0 ⊢ { o 1 , i ∗ ∗ e } ⟶ { o 1 , i ∗ ∗ e ′ } \frac{o_0 \vdash e \longrightarrow e'}{o_0 \vdash\{o_1,i**e\} \longrightarrow\{o_1,i**e'\}} o 0 ⊢ { o 1 , i ∗ ∗ e } ⟶ { o 1 , i ∗ ∗ e ′ } o 0 ⊢ e ⟶ e ′ E-CONCATL
o ⊢ e 0 ⟶ e 0 ′ o ⊢ e 0 + + e 1 ⟶ e 0 ′ + + e 1 \frac{o \vdash e_0 \longrightarrow e_0'}{o \vdash e_0 ++ e_1 \longrightarrow e_0' ++ e_1} o ⊢ e 0 + + e 1 ⟶ e 0 ′ + + e 1 o ⊢ e 0 ⟶ e 0 ′ E-CONCATR
o ⊢ e ⟶ e ′ o ⊢ v + + e ⟶ v + + e ′ \frac{o \vdash e \longrightarrow e'}{o \vdash v ++ e \longrightarrow v ++ e'} o ⊢ v + + e ⟶ v + + e ′ o ⊢ e ⟶ e ′ E-CONCAT
o 0 ⊢ { o 1 } + + { o 2 } ⟶ { o 1 + + o 2 } o_0 \vdash\{o_1\} ++ \{o_2\} \longrightarrow\{o_1 ++ o_2\} o 0 ⊢ { o 1 } + + { o 2 } ⟶ { o 1 + + o 2 } E-PROJ
o ⊢ e ⟶ e ′ o ⊢ e . i ⟶ e ′ . i \frac{o \vdash e \longrightarrow e'}{o \vdash e.i \longrightarrow e'.i} o ⊢ e . i ⟶ e ′ . i o ⊢ e ⟶ e ′ E-PROJRECORD
proj ( o 1 ; i ) = v o 0 ⊢ { o 1 } . i ⟶ v \frac{\operatorname{proj}(o_1;i)=v}{o_0 \vdash\{o_1\}.i \longrightarrow v} o 0 ⊢ { o 1 } . i ⟶ v proj ( o 1 ; i ) = v E-MPROJ
o ⊢ e ⟶ e ′ o ⊢ e . { i j } ⟶ e ′ . { i j } \frac{o \vdash e \longrightarrow e'}{o \vdash e.\{ij\} \longrightarrow e'.\{ij\}} o ⊢ e . { ij } ⟶ e ′ . { ij } o ⊢ e ⟶ e ′ E-MPROJRECORD
mproj ( o 1 ; i j ) = o 2 o 0 ⊢ { o 1 } . { i j } ⟶ { o 2 } \frac{\operatorname{mproj}(o_1;ij)=o_2}{o_0 \vdash\{o_1\}.\{ij\} \longrightarrow\{o_2\}} o 0 ⊢ { o 1 } . { ij } ⟶ { o 2 } mproj ( o 1 ; ij ) = o 2 E-DIFF
o ⊢ e ⟶ e ′ o ⊢ e \ { i j } ⟶ e ′ \ { i j } \frac{o \vdash e \longrightarrow e'}{o \vdash e\backslash\{ij\} \longrightarrow e'\backslash\{ij\}} o ⊢ e \ { ij } ⟶ e ′ \ { ij } o ⊢ e ⟶ e ′ E-DIFFRECORD
diff ( o 1 ; i j ) = o 2 o 0 ⊢ { o 1 } \ { i j } ⟶ { o 2 } \frac{\operatorname{diff}(o_1;ij)=o_2}{o_0 \vdash\{o_1\}\backslash\{ij\} \longrightarrow\{o_2\}} o 0 ⊢ { o 1 } \ { ij } ⟶ { o 2 } diff ( o 1 ; ij ) = o 2 E-LET
o ⊢ e 0 ⟶ e 0 ′ o ⊢ let t = e 0 in e 1 ⟶ let t = e 0 ′ in e 1 \frac{o \vdash e_0 \longrightarrow e_0'}{o \vdash\operatorname{let}t=e_0\ \operatorname{in}e_1 \longrightarrow\operatorname{let}t=e_0'\ \operatorname{in}e_1} o ⊢ let t = e 0 in e 1 ⟶ let t = e 0 ′ in e 1 o ⊢ e 0 ⟶ e 0 ′ E-LETV
expand ( t ; v ) = o 1 o 0 ⊢ let t = v in e ⟶ { o 0 , o 1 } ▶ e \frac{\operatorname{expand}(t;v)=o_1}{o_0 \vdash\operatorname{let}t=v\ \operatorname{in}e \longrightarrow\{o_0,o_1\}\mathbin{\blacktriangleright}e} o 0 ⊢ let t = v in e ⟶ { o 0 , o 1 } ▶ e expand ( t ; v ) = o 1 Subtyping
First, we prove that subtyping is reflexive and transitive:
Lemma 3.1 (Subtyping reflexivity). A ≤ A A \le A A ≤ A A A A
Lemma 3.2 (Subtyping transitivity). If A ≤ B A \le B A ≤ B B ≤ C B \le C B ≤ C A ≤ C A \le C A ≤ C
Record subtyping is preserved when entries are appended; the ⌊ ρ 1 ⌋ \lfloor\rho_1\rfloor ⌊ ρ 1 ⌋ ρ 2 \rho_2 ρ 2
Lemma 3.3 (Record subtyping appending). If ρ 0 ≤ ρ 1 \rho_0 \le\rho_1 ρ 0 ≤ ρ 1 ρ 2 ≤ ρ 3 \rho_2 \le\rho_3 ρ 2 ≤ ρ 3 ⌊ ρ 1 ⌋ \lfloor\rho_1\rfloor ⌊ ρ 1 ⌋ ρ 0 , ρ 2 ≤ ρ 1 , ρ 3 \rho_0,\rho_2 \le\rho_1,\rho_3 ρ 0 , ρ 2 ≤ ρ 1 , ρ 3
Moreover, subtyping on the environment is admissible:
Lemma 3.4 (Environment subtyping). If ρ 0 ⊢ e : A \rho_0 \vdash e : A ρ 0 ⊢ e : A ⌊ ρ 0 ⌋ \lfloor\rho_0\rfloor ⌊ ρ 0 ⌋ ρ 1 ≤ ρ 0 \rho_1 \le\rho_0 ρ 1 ≤ ρ 0 ρ 1 ⊢ e : A \rho_1 \vdash e : A ρ 1 ⊢ e : A
Intuitively, this holds since the only way to access the environment is via @ through rule T-ENV, and we can always apply the subsumption rule (T-SUB) and the record subtyping rule (S-RECORD) immediately after. The second hypothesis ensures the subtyping relationship can be maintained using Lemma 3.3 even when new bindings are introduced.
Concatenation
The following lemma establishes the associativity property of concatenation. For concision, we often embed record operators directly within other relations. For instance, we write ( ρ 0 ⊕ ρ 1 ) ⊕ ρ 2 ⇝ ρ 3 (\rho_0 \oplus\rho_1) \oplus\rho_2 \rightsquigarrow\rho_3 ( ρ 0 ⊕ ρ 1 ) ⊕ ρ 2 ⇝ ρ 3 ρ \rho ρ ρ 0 ⊕ ρ 1 ⇝ ρ \rho_0 \oplus\rho_1 \rightsquigarrow\rho ρ 0 ⊕ ρ 1 ⇝ ρ ρ ⊕ ρ 2 ⇝ ρ 3 \rho\oplus\rho_2 \rightsquigarrow\rho_3 ρ ⊕ ρ 2 ⇝ ρ 3
Lemma 3.5 (Associativity of ⊕ \oplus ⊕ ( ρ 0 ⊕ ρ 1 ) ⊕ ρ 2 ⇝ ρ 3 (\rho_0 \oplus\rho_1) \oplus\rho_2 \rightsquigarrow\rho_3 ( ρ 0 ⊕ ρ 1 ) ⊕ ρ 2 ⇝ ρ 3 ρ 0 ⊕ ( ρ 1 ⊕ ρ 2 ) ⇝ ρ 3 \rho_0 \oplus(\rho_1 \oplus\rho_2) \rightsquigarrow\rho_3 ρ 0 ⊕ ( ρ 1 ⊕ ρ 2 ) ⇝ ρ 3
Application and record concatenation. The next lemma establishes an associativity-like property between application and concatenation. Intuitively, it shows that given an initial ρ 0 \rho_0 ρ 0 ρ 1 \rho_1 ρ 1 ρ 2 \rho_2 ρ 2 ρ 1 \rho_1 ρ 1 ρ 2 \rho_2 ρ 2 ρ 0 \rho_0 ρ 0
Lemma 3.6 (Associativity of ∙ \bullet ∙ ⊕ \oplus ⊕ ( ρ 0 ∙ ρ 1 ) ∙ ρ 2 ⇀ ρ 3 (\rho_0 \mathbin{\bullet} \rho_1) \mathbin{\bullet} \rho_2 \mathrel{\rightharpoonup} \rho_3 ( ρ 0 ∙ ρ 1 ) ∙ ρ 2 ⇀ ρ 3 ρ 0 ∙ ( ρ 1 ⊕ ρ 2 ) ⇀ ρ 3 \rho_0 \mathbin{\bullet} (\rho_1 \mathbin{\oplus} \rho_2) \mathrel{\rightharpoonup} \rho_3 ρ 0 ∙ ( ρ 1 ⊕ ρ 2 ) ⇀ ρ 3
Type soundness. First, we prove that the operational semantics enjoy determinacy:
Theorem 3.7 (Determinacy). If ρ ⊢ e → e 0 \rho\vdash e \mathrel{\to} e_0 ρ ⊢ e → e 0 ρ ⊢ e → e 1 \rho\vdash e \mathrel{\to} e_1 ρ ⊢ e → e 1 e 0 = e 1 e_0 = e_1 e 0 = e 1
We then establish type soundness for λ ρ \lambda^\rho λ ρ
Theorem 3.8 (Preservation). Given ϵ ⊢ { o } : { ρ } \epsilon\vdash\{o\} : \{\rho\} ϵ ⊢ { o } : { ρ } ⌊ ρ ⌋ \lfloor\rho\rfloor ⌊ ρ ⌋ ρ ⊢ e : A \rho\vdash e : A ρ ⊢ e : A o ⊢ e → e ′ o \vdash e \mathrel{\to} e' o ⊢ e → e ′ ρ ⊢ e ′ : A \rho\vdash e' : A ρ ⊢ e ′ : A
Theorem 3.9 (Progress). Given ϵ ⊢ { o } : { ρ } \epsilon\vdash\{o\} : \{\rho\} ϵ ⊢ { o } : { ρ } ⌊ ρ ⌋ \lfloor\rho\rfloor ⌊ ρ ⌋ ρ ⊢ e : A \rho\vdash e : A ρ ⊢ e : A e e e e ′ e' e ′ o ⊢ e → e ′ o \vdash e \mathrel{\to} e' o ⊢ e → e ′
Normalization. Additionally, since our reduction is non-standard, we also formally prove its normalization property. The proof proceeds via a logical relation [36 ] :
ρ ; o ⊢ SN { ρ 0 } → A ( e ) = ρ ⊢ e : { ρ 0 } → A ∧ o ⊢ SN ( e ) ∧ ∀ ρ 1 , ρ 2 , ρ 0 ∙ ρ 1 ⇀ ρ 2 ⇒ ⌊ ρ 2 ⌋ ⇒ \rho; o \vdash\operatorname{SN}_{\{\rho_0\}\to A}(e) = \rho\vdash e : \{\rho_0\}\to A \land o \vdash\operatorname{SN}(e) \land\forall\rho_1,\rho_2,\ \rho_0 \mathbin{\bullet} \rho_1 \mathrel{\rightharpoonup} \rho_2 \Rightarrow\lfloor\rho_2\rfloor\Rightarrow ρ ; o ⊢ SN { ρ 0 } → A ( e ) = ρ ⊢ e : { ρ 0 } → A ∧ o ⊢ SN ( e ) ∧ ∀ ρ 1 , ρ 2 , ρ 0 ∙ ρ 1 ⇀ ρ 2 ⇒ ⌊ ρ 2 ⌋ ⇒ ∀ v , ( ∀ ρ ′ , ϵ ⊢ { o ′ } : { ρ ′ } ⇒ ⌊ ρ ′ ⌋ ⇒ ρ ′ ; o ′ ⊢ SN { ρ 1 } ( v ) ) ⇒ ρ ; o ⊢ SN A ( force ( e v ) ) \forall v,\ \left(\forall\rho',\ \epsilon\vdash\{o'\} : \{\rho'\} \Rightarrow\lfloor\rho'\rfloor\Rightarrow\rho';o' \vdash\operatorname{SN}_{\{\rho_1\}}(v)\right) \Rightarrow\rho;o \vdash\operatorname{SN}_A(\operatorname{force}(e\,v)) ∀ v , ( ∀ ρ ′ , ϵ ⊢ { o ′ } : { ρ ′ } ⇒ ⌊ ρ ′ ⌋ ⇒ ρ ′ ; o ′ ⊢ SN { ρ 1 } ( v ) ) ⇒ ρ ; o ⊢ SN A ( force ( e v )) ρ ; o ⊢ SN { ρ ′ } ( e ) = ρ ⊢ e : { ρ ′ } ∧ ∃ r , o ⊢ e → ∗ { r } ∧ ∀ ( e ′ , A ) ∈ ( r , ρ ′ ) , ρ ; o ⊢ SN A ( e ′ ) \rho; o \vdash\operatorname{SN}_{\{\rho'\}}(e) = \rho\vdash e : \{\rho'\} \land\exists r,\ o \vdash e \mathrel{\overset{*}{\to}} \{r\} \land\forall(e',A)\in(r,\rho'),\ \rho;o\vdash\operatorname{SN}_A(e') ρ ; o ⊢ SN { ρ ′ } ( e ) = ρ ⊢ e : { ρ ′ } ∧ ∃ r , o ⊢ e → ∗ { r } ∧ ∀ ( e ′ , A ) ∈ ( r , ρ ′ ) , ρ ; o ⊢ SN A ( e ′ ) ρ ; o ⊢ SN N ( e ) = ρ ⊢ e : N ∧ o ⊢ SN ( e ) ρ ; o ⊢ SN ∀ a . A ( e ) = ρ ⊢ e : ∀ a . A ∧ ∀ τ , ρ ; o ⊢ SN A [ τ / a ] ( e ) \rho;o\vdash\operatorname{SN}_{N}(e)=\rho\vdash e:N\land o\vdash\operatorname{SN}(e)
\qquad
\rho;o\vdash\operatorname{SN}_{\forall a.A}(e)=\rho\vdash e:\forall a.A\land\forall\tau,\ \rho;o\vdash\operatorname{SN}_{A[\tau/a]}(e) ρ ; o ⊢ SN N ( e ) = ρ ⊢ e : N ∧ o ⊢ SN ( e ) ρ ; o ⊢ SN ∀ a . A ( e ) = ρ ⊢ e : ∀ a . A ∧ ∀ τ , ρ ; o ⊢ SN A [ τ / a ] ( e ) In the function case, we quantify over record types whose application leaves only entries of optional strength (⌊ ρ 2 ⌋ \lfloor\rho_2\rfloor ⌊ ρ 2 ⌋
Theorem 3.10 (Fundamental). Given ρ ⊢ e : A \rho\vdash e:A ρ ⊢ e : A ⌊ ρ ⌋ \lfloor\rho\rfloor ⌊ ρ ⌋ ϵ ; ϵ ⊢ SN { ρ } ( { o } ) \epsilon;\epsilon\vdash\operatorname{SN}_{\{\rho\}}(\{o\}) ϵ ; ϵ ⊢ SN { ρ } ({ o }) ρ ; o ⊢ SN A ( e ) \rho;o\vdash\operatorname{SN}_A(e) ρ ; o ⊢ SN A ( e )
Theorem 3.11 (Normalization). If ρ ; o ⊢ SN A ( e ) \rho;o\vdash\operatorname{SN}_A(e) ρ ; o ⊢ SN A ( e ) e e e
Syntax-Directed Typing
The declarative typing rules are not syntax-directed: subsumption (T-sub) may be applied anywhere, and quantifiers are instantiated implicitly through subtyping. In this section we present a syntax-directed variant that is sound and complete with respect to the declarative system. Full algorithmic type inference is outside the scope of this paper, but the syntax-directed rules show how our features can be handled without guessing where to apply subsumption. Selected rules are given in Figure 8 ; the full set of typing and updated auxiliary judgement rules can be found in the appendix.
Figure 8. Syntax-directed typing
The usual approach of instantiating quantifiers eagerly at variables and re-generalizing at lets does not fit our language: variables are projections out of a first-class environment, types
ends_mid=1 higher-rank, and we generalize at abstractions rather than lets. We therefore instantiate lazily , in the elimination rules. In rule ST-force, for instance, the first hypothesis accepts any number of quantifiers, which are instantiated in the conclusion. Without subtyping to discard optional entries (S-empty), ρ 1 \rho_1 ρ 1 { ρ } → A \{\rho\} \to A { ρ } → A ⌊ ρ ⌋ \lfloor\rho\rfloor ⌊ ρ ⌋ A A A [14 ] , where the expected type is available in checking mode; we leave this to future work. The double-colon hypothesis invokes a helper judgement (ST-instantiate) for types such as ∀ a . a \forall a.\ a ∀ a . a
We prove that our syntax-directed typing is sound and complete:
Theorem 3.12 (Soundness). If ρ ⊢ s e : A \rho\vdash_{\mathrm{s}} e : A ρ ⊢ s e : A ρ ⊢ e : A \rho\vdash e : A ρ ⊢ e : A
Theorem 3.13 (Completeness). If ρ ⊢ e : A \rho\vdash e : A ρ ⊢ e : A ⌊ ρ ⌋ \lfloor\rho\rfloor ⌊ ρ ⌋ B B B B ≤ A B \leq A B ≤ A ρ ⊢ s e : B \rho\vdash_{\mathrm{s}} e : B ρ ⊢ s e : B
Translating the Lambda Calculus
To demonstrate that the use of explicit environments preserves the semantics of the substitution model, we present a translation from the simply typed lambda calculus (STLC) to λ ρ + \lambda^{\rho^+} λ ρ +
Translations. The translation of types, environments, and terms from STLC to λ ρ + \lambda^{\rho^+} λ ρ + ι \iota ι [6 ] .)
⟦ τ ⟧ = ⟦ τ 0 → τ 1 ⟧ = { _ : ⟦ τ 0 ⟧ } → ⟦ τ 1 ⟧ ⟦ N ⟧ = N ⟦ ι ⊢ Γ ⟧ = ⟦ ε ⊢ ε ⟧ = ε ⟦ ι , x ∼ i ⊢ Γ , x : τ ⟧ = ⟦ ι ⊢ Γ ⟧ , i : ⟦ τ ⟧ ⟦ ι ⊢ e ⟧ = ⟦ ι ⊢ x ⟧ = @ . i if x ∼ i ∈ ι ⟦ ι ⊢ λ x . e ⟧ = λ { _ ⋄ i } . ⟦ ι , x ∼ i ⊢ e ⟧ ⟦ ι ⊢ e 0 e 1 ⟧ = force ⟦ ι ⊢ e 0 ⟧ { _ : ⟦ ι ⊢ e 1 ⟧ } ⟦ ι ⊢ n ⟧ = n \begin{aligned}
\llbracket\tau\rrbracket&= \llbracket\tau_0 \to\tau_1 \rrbracket= \{\,\_ : \llbracket\tau_0 \rrbracket\,\} \to\llbracket\tau_1 \rrbracket\\
\llbracket N \rrbracket&= N \\
\llbracket\iota\vdash\Gamma\rrbracket&= \llbracket\varepsilon\vdash\varepsilon\rrbracket= \varepsilon\\
\llbracket\iota, x \mathrel{\sim} i \vdash\Gamma, x : \tau\rrbracket&= \llbracket\iota\vdash\Gamma\rrbracket, i : \llbracket\tau\rrbracket\\
\llbracket\iota\vdash e \rrbracket&= \llbracket\iota\vdash x \rrbracket= @.i \quad\text{if } x \mathrel{\sim} i \in\iota\\
\llbracket\iota\vdash\lambda x.e \rrbracket&= \lambda\{\,\_ \mathbin{\diamond} i\,\}.\llbracket\iota, x \mathrel{\sim} i \vdash e \rrbracket\\
\llbracket\iota\vdash e_0\ e_1 \rrbracket&= \operatorname{force}\llbracket\iota\vdash e_0 \rrbracket\{\,\_ : \llbracket\iota\vdash e_1 \rrbracket\,\} \\
\llbracket\iota\vdash n \rrbracket&= n
\end{aligned} [ [ τ ] ] [ [ N ] ] [ [ ι ⊢ Γ ] ] [ [ ι , x ∼ i ⊢ Γ , x : τ ] ] [ [ ι ⊢ e ] ] [ [ ι ⊢ λ x . e ] ] [ [ ι ⊢ e 0 e 1 ] ] [ [ ι ⊢ n ] ] = [ [ τ 0 → τ 1 ] ] = { _ : [ [ τ 0 ] ] } → [ [ τ 1 ] ] = N = [ [ ε ⊢ ε ] ] = ε = [ [ ι ⊢ Γ ] ] , i : [ [ τ ] ] = [ [ ι ⊢ x ] ] = @. i if x ∼ i ∈ ι = λ { _ ⋄ i } . [ [ ι , x ∼ i ⊢ e ] ] = force [ [ ι ⊢ e 0 ] ] { _ : [ [ ι ⊢ e 1 ] ] } = n The translation rules are then largely straightforward. STLC lambdas are mapped to λ ρ + \lambda^{\rho^+} λ ρ +
Simulation. First, we prove that typing is preserved under translation:
Theorem 3.14 (Preservation of typing). If Γ ⊢ e : τ \Gamma\vdash e : \tau Γ ⊢ e : τ ⟦ ι ⊢ Γ ⟧ ⊢ ⟦ ι ⊢ e ⟧ : ⟦ τ ⟧ \llbracket\iota\vdash\Gamma\rrbracket\vdash\llbracket\iota\vdash e \rrbracket: \llbracket\tau\rrbracket [ [ ι ⊢ Γ ] ] ⊢ [ [ ι ⊢ e ] ] : [ [ τ ] ]
Relating the evaluation behaviour of the two calculi is slightly more involved. We utilize a term approximation relation δ e S ≈ e \delta\ e_{\mathrm{S}} \approx e δ e S ≈ e e S e_{\mathrm{S}} e S λ ρ + \lambda^{\rho^+} λ ρ + e e e δ \delta δ
Theorem 3.15 (Correspondence of semantics). e ⟶ ∗ n e \longrightarrow^{*} n e ⟶ ∗ n e ⊢ ⟦ e ⊢ e ⟧ ⟶ ∗ n e \vdash\llbracket e \vdash e \rrbracket\longrightarrow^{*} n e ⊢ [ [ e ⊢ e ] ] ⟶ ∗ n
Extension: References
In this section, we extend λ ρ + \lambda^{\rho^+} λ ρ +
Syntax and semantics. Figure 9 presents the extended syntax, typing, and operational semantics. Congruence reduction rules and syntax-directed typing are omitted for space but can be found in the appendix. Types now include the reference type Ref A \operatorname{Ref}\ A Ref A l l l ref e \operatorname{ref}\ e ref e ! e !e ! e e 0 : = e 1 e_0 := e_1 e 0 := e 1 o o o ρ s \rho_s ρ s \left\llbracket\rho_s \right\rrbracket , when all its entries have strength (: : :
Figure 9. Extension with references (selected rules)
The extended subtyping and typing are standard. Subtyping of references is invariant. The typing judgement ρ s ; ρ ⊢ e : A \rho_s;\rho\vdash e : A ρ s ; ρ ⊢ e : A ρ s \rho_s ρ s
The evaluation judgement is also extended to thread the store through each step. Rule E-REFV allocates a fresh name in the store. (In the mechanization, the operational semantics maintain determinacy by picking the fresh name to be the maximal variable index in the store plus one.) Rule E-DEREFLOC projects the corresponding entry out of the store. Finally, rule E-SET leverages the overwriting behaviour of record concatenation to update the corresponding store entry.
Generalization and the value restriction. It may seem surprising that we did not modify any of the original typing rules. In systems with polymorphism and generalization, it is well-known that adding mutable state can easily yield type unsoundness. As an example, consider the program on the right. Naive let-generalization will assign x x x ∀ a . Ref ( { i : a } → a ) \forall a.\operatorname{Ref}\ (\{i:a\}\to a) ∀ a . Ref ({ i : a } → a ) a a a N \mathbb{N} N B \mathbb{B} B
let x = ref (λ{ i }. i) in
let { } = (x := (λ{ i }. i + 1)) in
force !x { i = true }To preserve safety, a standard remedy is the value restriction [40 ] , which limits let-generalization to syntactic values. Applying this restriction would prevent x x x
We therefore adapt the approach recently proposed by Dolan [ [13 ] , which performs generalization at functions (specifically rules T-LAM and T-CLOSURE in our case), rather than let-bindings. This approach can be considered a more fine-grained variant of the value restriction. It restores type soundness; for example, in the program above x x x Ref ( ∀ a . { i : a } → a ) \operatorname{Ref}\ (\forall a.\{i:a\}\to a) Ref ( ∀ a . { i : a } → a )
typeability, as it allows the individual components of a non-value compound expression to generalize independently. In our calculus, this design naturally facilitates the construction of records with polymorphic fields, e.g. let x = {id = λ{i}. i, incr = λ{j}. j + 1} in e assigns x x x { i d ▹ ∀ a . { i : a } → a , i n c r ▹ { j : N } → N } \{id \mathrel{\triangleright} \forall a.\{i : a\} \to a, incr \mathrel{\triangleright} \{j : \mathbb{N}\} \to\mathbb{N}\} { i d ▹ ∀ a . { i : a } → a , in cr ▹ { j : N } → N }
Type soundness. We have proven the determinacy, progress, and preservation theorems for the extended semantics, where the theorems are now adapted to account for the presence of stores; we omit their statements for space. The syntax-directed system likewise extends to references and remains sound and complete.
Mechanization and Implementation
Mechanization. We have mechanized λ ρ ⊢ \lambda^{\rho\vdash} λ ρ ⊢ [28 ] , covering all semantics and theorems. Table 1 summarizes the statistics. By using explicit environments, we avoid the term-level binding complications described in § 2.1 , allowing labels and locations to be represented simply as natural numbers. However, without explicit type environments, we adopt the locally nameless representation [6 ] for type variables.
Table 1. Code stats of mechanization and implementation
Most of the proofs proceeded without significant difficulty. One particular challenge in a few cases, such as Lemma 3.2 , was to show that the induction used to prove them was well-founded. This arose as Lean has proof irrelevance: since Lean treats all propositions of the same type as equal, the depth of a derivation cannot be used directly in termination measures. We circumvented this limitation by defining versions of subtyping and multi-step evaluation that are explicitly indexed by their derivation depth, and using these numerical indices as well-founded measures.
Implementation. Since one of our motivations for using first-class environments is to close the gap between specification and implementation identified by Tan and Oliveira [ [37 ] , we have implemented an interpreter and verified it against our operational semantics. Because the extended λ ρ ⊢ \lambda^{\rho\vdash} λ ρ ⊢ [19 ] ), well-typed programs are not guaranteed to terminate. We thus leverage Lean’s partial_fixpoint feature2
We then prove the equivalence of the operational semantics and the evaluation function eval. The first clause of the following theorem expresses that for terminating inputs, the operational semantics and eval agree. The second clause states that for well-typed inputs, eval yields none precisely when there are infinite reduction steps (denoted by ω → \omega\to ω →
Theorem 5.1 (Interpreter correctness).
ρ ⊢ e ; o s → ∗ v ; o s ′ \rho\vdash e; o_s \overset{*}{\to} v; o_s' ρ ⊢ e ; o s → ∗ v ; o s ′ o o o e e e o s = some ( v , o s ′ ) o_s = \operatorname{some}(v, o_s') o s = some ( v , o s ′ )
Given ρ s ; ε ⊢ { o } : { ρ } \rho_s;\varepsilon\vdash\{o\} : \{\rho\} ρ s ; ε ⊢ { o } : { ρ } ⟦ ρ ⟧ \llbracket\rho\rrbracket [ [ ρ ] ] ρ s ; ε ⊢ { o s } : { ρ s } \rho_s;\varepsilon\vdash\{o_s\} : \{\rho_s\} ρ s ; ε ⊢ { o s } : { ρ s } ⟦ ρ s ⟧ \llbracket\rho_s\rrbracket [ [ ρ s ] ] ρ s ; ρ ⊢ e : A \rho_s;\rho\vdash e : A ρ s ; ρ ⊢ e : A o ⊢ e ; o s → ω o \vdash e; o_s \xrightarrow{\omega} o ⊢ e ; o s ω eval o e o s = none \operatorname{eval}\ o\ e\ o_s = \operatorname{none} eval o e o s = none
We prove this theorem by using the transitivity of equivalence, introducing an intermediate big-step operational semantics for λ ρ \lambda^\rho λ ρ eval function and the small-step operational semantics.
Discussion
The Design Space
Function application paradigms encompass a broad design space. In this section, we examine how these various features are supported across programming languages. The selected languages are (1) Python (dynamically typed), (2) TypeScript (gradually typed), (3) Swift, (4) OCaml, (5) Scala (all statically typed), and (6) Lean 4 (dependently typed). While many more languages exist, these languages offer a diverse and representative spectrum of modern language design decisions. We summarize the comparison in Table 2 :
Table 2. A comparison table of languages with named arguments (with † explained in § 8.1 )
All languages listed in the table offer some degree of support for named arguments . Although TypeScript†1 lacks native support, simulating this behaviour by passing a single object is a widespread idiom in its community; we thus record ticks for both named and first-class arguments.
Statically typed languages often support named arguments through elaboration, while dynamically typed ones typically resolve them by matching labels against function parameters at runtime.
We use first-class arguments to mean that a function’s arguments can be stored within a data structure and subsequently supplied to a function call. For example, in Python, the example in § 2.3 can be rewritten using the dictionary unpacking operator **:
transaction = { amount: 1000, "from_account": "Alice", "to_account": "Bob" }
transfer_funds(**transaction)Optional type checkers for Python can type such keyword arguments with a record type [24 ] . λ ρ \lambda^\rho λ ρ
All listed languages support certain forms of optional arguments that can be omitted at call sites. This unanimous adoption stems partly from our focus on languages with named arguments, which provide the parameter disambiguation necessary to make optional arguments viable. A few languages do not require default values for optional arguments. In TypeScript, for instance, an omitted argument defaults to undefined, and its presence must be checked by e.g. c === undefined.
In both Swift and OCaml, distinct argument labels and parameter names are specified within the function definition. TypeScript mimics this behaviour via property-renaming syntax during object destructuring. In Lean 4†2 , this feature emerges as a consequence of type equivalence, where the desired argument label can be set by annotating the function with a new type.
Commutative arguments are typical among named arguments, though exceptions like Swift exist. Positional arguments cannot commute with themselves, as their order determines their identity. It remains to ask whether positional arguments can commute with named ones. In Python3 4 5 g g g f : { a g e : Int , n a m e : String } → Int f : \{ age: \operatorname{Int}, name: \operatorname{String} \} \to\operatorname{Int} f : { a g e : Int , nam e : String } → Int λ ρ \lambda^\rho λ ρ
With partial application , applying a function to a subset of its arguments results in a new function taking the remaining parameters. Unlike traditional currying, which is constrained by strict sequential evaluation, general partial application allows a function to be partially applied to an arbitrary subset of arguments. Scala achieves this via wildcard placeholder syntax: transfer_from_alice = transfer_funds(_:Int, "Alice", _:String). Nevertheless, Scala requires programmers to explicitly mark each unapplied parameter with _. This mechanism also replaces the original parameter names with compiler-generated names (v1, v2, …), obscuring the purpose of the remaining arguments. As discussed in §2.7, partial application interacts with optional arguments. While OCaml requires a subsequent positional argument after optional ones, Scala and Lean 4 automatically fill in missing optional arguments with their default values during compilation.
Discussion: Broader Applications
In this section, we broaden our scope to examine how various components of our design can be helpful in alternative contexts, highlighting the underlying principles of our design; the appendix discusses further applications.
Safe interface upgrades with optional subtyping. Record-like data structures are widely used to describe software interfaces, which naturally evolve over time. As a simple example, consider the user profile interface (a) in Figure 10 , which specifies a profile sent from a client to a server:
# (a) profile interface # (b) upgraded interface # (c) safe upgraded interface
type profile = { type profile = { type profile = {
bio : text bio : text bio : text
theme_color : num theme_color : num theme_color : num
+ dark_mode : bool + dark_mode : opt bool }Figure 10. Interface upgrades (specified with +)
A new software release may introduce additional features and consequently update the interface. For example, interface (b) upgrades the profile interface with a dark_mode field to specify whether the server should render a dark theme. However, legacy clients that have not upgraded will now send profiles lacking this field, creating a type mismatch and causing runtime errors. In this context, an upgrade is considered safe if a client sending data according to the old format does not cause a failure when the server expects the new format (and vice versa).
To resolve this challenge, the interface description language Candid [DFINITY 2026a] requires that an interface for inbound data (i.e. data sent from the client to the server) may only be replaced by a supertype (e.g. fewer fields); therefore, the upgrade (b) is rejected. On the other hand, Candid permits a record subtyping rule that is “unusual but necessary in practice” [12 ] ,
, Vol. 1, No. 1, Article . Publication date: October 2026. new fields are allowed in the supertype as long as they are optional. Under this rule, interface (a) is considered a subtype of (c), where the newly added dark_mode field has type opt bool. Thus interface (c) is accepted as a safe upgraded interface. We note that this use of optional types is similar to ours, and the subtyping rule corresponds to the extra right entries in our S-empty rule.
Interestingly, Candid combines the standard record width subtyping with the above subtyping rule for optionals, which leads to surprising consequences. Specifically, via record width subtyping, interface (a) is a subtype of { bio : text }, which removed the theme_color field. Via subtyping for optionals, { bio : text } is a subtype of { bio : text, theme_color : opt string }. It follows, via subtyping transitivity, that (a) is a subtype of { bio : text, theme_color : opt string }; effectively, this changes the type of theme_color from nat to opt string. However, if one were to compare nat and opt string directly, subtyping would fail. Since subtyping transitivity is crucial for supporting sequences of upgrades, Candid’s subtyping tolerates such type mismatches at runtime, yielding null values for the affected fields. On the other hand, our system omits the record width subtyping rule entirely, and thus this specific issue does not arise. Specifically, width subtyping effectively allows a function to accept extraneous arguments (e.g. sub { name = "Alice" }) that serve no purpose. Such applications are disallowed; instead, a programmer can use record projection to extract the desired fields from an argument before passing it to a function.
Packaging with overwritable fields. The Nix language is a functional domain-specific language that powers the Nix packaging system [Dolstra and The Nix contributors 2026]. Nix evaluates expressions to create derivations , which describe how to build reproducible packages. For example, consider a package recipe defined as a function of its dependencies, including an openssl argument:
let app = { stdenv, openssl }:
stdenv.mkDerivation { name = "app"; buildInputs = [ openssl ]; };We can instantiate this recipe using the callPackage function, providing an attribute set that explicitly binds stdenv, as well as the openssl argument to the openssl_1_1 package:
myApp = pkgs.callPackage app { stdenv = pkgs.stdenv; openssl = pkgs.openssl_1_1; };More interestingly, callPackage allows arguments to be customized after the fact using a derivation’s override function. For example, even after myApp has been instantiated, we can override its openssl argument with a new value to update the package to OpenSSL 3.0:
mySecuredApp = myApp.override { openssl = pkgs.openssl_3; };Here, myApp.override overrides the openssl argument originally supplied by callPackage, producing a new derivation with the exact same arguments as myApp except for the updated openssl dependency. Note that since Nix is functional, this does not mutate the original package. This style of overriding is made possible by Nix’s evaluation strategy, which evaluates expressions to construct a derivation graph but defers the actual compilation and building of binaries until a build is explicitly requested (e.g. via nix-build). This behaviour aligns with our overwritable arguments feature, which allows a function’s arguments to be overwritten even after the function has been applied, and the evaluation of a function is deferred until it is explicitly forced.
Related Work
We have discussed comparisons to various formalisms and languages throughout the paper. While many production languages feature forms of named and optional arguments, their designs are mostly described informally [33 ] (Flatt and Barzilay 2009). Formally, Garrigue [15 ] presented typing rules for labelled and optional arguments for OCaml, noting that the application rule becomes complex because it “integrates all the commuting and discarding machinery”. More recently, Sun and Oliveira [35 ] modelled named arguments using intersection types and opti arguments using union types; they identified a tension with record width subtyping that closely mirrors the Candid issue discussed in § 8.2 .
One recent exploration of first-class environments is by Tan and Oliveira [ [37 ] . Our approach differs from theirs in several significant ways. First, their calculus λ E \lambda_E λ E λ E \lambda_E λ E
Row calculi have a rich history in the literature. Most relevant to our setting are Leijen [ [21 ] , which supports duplicate labels, and Rémy [ [32 ] , which allows existing labels to be overwritten. Furthermore, Osinski [ [29 ] introduced a record concatenation operator (&) that permits duplicate labels only when they have the same type, in which case the value of the field in the second operand is selected (similarly to our shadowing behaviour). CDuce Benzaken et al. [2 ] supports optional fields in record types and distinguishes open record types, which admit extra fields, from closed ones. Read this way, λ ρ \lambda^{\rho} λ ρ [27 ] .
Data Availability Statement
The Lean 4 development accompanying this paper is provided in the supplementary materials. It contains the mechanized proofs of all stated lemmas and theorems, as well as the code of the interpreter and the proof of its equivalence with the operational semantics.
References
More Discussions
Broader Applications
Typed XML documents with optional values. CDuce [2 ] is a typed functional language targeted at XML applications, in which the attributes of an XML element form a record. Since XML attributes are often optional, a record type can mark a field as optional, e.g. { k i n d = ? S t r i n g } \{\,\mathit{kind} =? \mathit{String}\,\} { kind = ? String } open record types, which admit new fields, from closed ones, which do not. Since subtyping in CDuce is defined as set inclusion, width subtyping requires an open supertype, while a closed type may only add optional fields. Read this way, λ ρ \lambda^{\rho} λ ρ { b i o : t e x t } \{\,\mathit{bio} : \mathit{text}\,\} { bio : text } § 8.2 admits a theme_color field of any type, and is therefore not a subtype of { b i o : t e x t , t h e m e _ c o l o r : o p t s t r i n g } \{\,\mathit{bio} : \mathit{text},\ \mathit{theme\_color} : \mathit{opt}\ \mathit{string}\,\} { bio : text , theme_color : opt string } λ ρ \lambda^{\rho} λ ρ
Masking effects with optionals. Optional values emerge naturally in the presence of scoped labels. In particular, our formulation of optional values is closely related to the mask (also called inject or lift ) operation found in algebraic effect handlers [30 , 31 ] when effects are represented as scoped labels [4 , 9 ] . In such systems, the effect type system tracks effect operations performed within an expression, and handlers eliminate these effects, with operations being handled dynamically by default with the innermost enclosing handler. If a developer intends for an effect to be handled by the second innermost handler instead, they can explicitly mask the innermost handler. For instance, m a s k ⟨ p r i n t ⟩ ( p r i n t ( ) ) \mathit{mask}\langle\mathit{print}\rangle\ (\mathit{print}\ ()) mask ⟨ print ⟩ ( print ( )) { p r i n t , p r i n t } \{\mathit{print},\mathit{print}\} { print , print }
Presence types with strength subtyping. Consider a function e q : ∀ a . { _ : a , _ : a } → b o o l \mathit{eq} : \forall a.\ \{\_ : a,\ \_ : a\} \to\mathit{bool} eq : ∀ a . { _ : a , _ : a } → bool a l i c e : { n a m e : S t r i n g , a g e : I n t } \mathit{alice} : \{\mathit{name} : \mathit{String},\ \mathit{age} : \mathit{Int}\} alice : { name : String , age : Int } b o b : { n a m e : S t r i n g , a g e ? I n t } \mathit{bob} : \{\mathit{name} : \mathit{String},\ \mathit{age}\ ?\ \mathit{Int}\} bob : { name : String , age ? Int } ( e q a l i c e b o b ) (\mathit{eq}\ \mathit{alice}\ \mathit{bob}) ( eq alice bob ) a a a a l i c e : { n a m e : S t r i n g , a g e ? I n t } \mathit{alice} : \{\mathit{name} : \mathit{String},\ \mathit{age}\ ?\ \mathit{Int}\} alice : { name : String , age ? Int } ( e q { a l i c e , b o b } ) (\mathit{eq}\ \{\mathit{alice},\ \mathit{bob}\}) ( eq { alice , bob }) a a a { n a m e : S t r i n g , a g e ? I n t } \{\mathit{name} : \mathit{String},\ \mathit{age}\ ?\ \mathit{Int}\} { name : String , age ? Int }
This approach is reminiscent of record calculi where labels have presence types [32 ] . In such a system, one can write a l i c e : { n a m e : p r e ( S t r i n g ) , a g e : p r e ( I n t ) ; a b s } \mathit{alice} : \{\mathit{name} : \mathit{pre}(\mathit{String}),\ \mathit{age} : \mathit{pre}(\mathit{Int});\ \mathit{abs}\} alice : { name : pre ( String ) , age : pre ( Int ) ; abs } b o b : { n a m e : p r e ( S t r i n g ) ; a b s } \mathit{bob} : \{\mathit{name} : \mathit{pre}(\mathit{String});\ \mathit{abs}\} bob : { name : pre ( String ) ; abs } ( e q { a l i c e , b o b } ) (\mathit{eq}\ \{\mathit{alice},\ \mathit{bob}\}) ( eq { alice , bob }) p r e ( I n t ) \mathit{pre}(\mathit{Int}) pre ( Int ) a b s \mathit{abs} abs poisoning problem [38 ] (Peyton Jones 1999), where type information from one expression pollutes another, here, via the presence of the a b s \mathit{abs} abs p r e ≤ a b s \mathit{pre} \leq\mathit{abs} pre ≤ abs
Extensions
This section explores several potential extensions to our design.
Variadic arguments. Another common paradigm for function application is variadic arguments (or variable-length arguments). If the arguments are homogeneous, this feature can be considered as passing a list. More interestingly, in dynamically typed languages like Python, we can pass a variable number of arguments of different types, as demonstrated in the program on
@page 27/37 starts_mid=0 ends_mid=1
More Discussions
Broader Applications
Typed XML documents with optional values. CDuce [2 ] is a typed functional language targeted at XML applications, in which the attributes of an XML element form a record. Since XML attributes are often optional, a record type can mark a field as optional, e.g. { k i n d = ? S t r i n g } \{\,\mathit{kind} =? \mathit{String}\,\} { kind = ? String } open record types, which admit new fields, from closed ones, which do not. Since subtyping in CDuce is defined as set inclusion, width subtyping requires an open supertype, while a closed type may only add optional fields. Read this way, λ ρ \lambda^{\rho} λ ρ { b i o : t e x t } \{\,\mathit{bio} : \mathit{text}\,\} { bio : text } § 8.2 admits a theme_color field of any type, and is therefore not a subtype of { b i o : t e x t , t h e m e _ c o l o r : o p t s t r i n g } \{\,\mathit{bio} : \mathit{text},\ \mathit{theme\_color} : \mathit{opt}\ \mathit{string}\,\} { bio : text , theme_color : opt string } λ ρ \lambda^{\rho} λ ρ
Masking effects with optionals. Optional values emerge naturally in the presence of scoped labels. In particular, our formulation of optional values is closely related to the mask (also called inject or lift ) operation found in algebraic effect handlers [30 , 31 ] when effects are represented as scoped labels [4 , 9 ] . In such systems, the effect type system tracks effect operations performed within an expression, and handlers eliminate these effects, with operations being handled dynamically by default with the innermost enclosing handler. If a developer intends for an effect to be handled by the second innermost handler instead, they can explicitly mask the innermost handler. For instance, m a s k ⟨ p r i n t ⟩ ( p r i n t ( ) ) \mathit{mask}\langle\mathit{print}\rangle\ (\mathit{print}\ ()) mask ⟨ print ⟩ ( print ( )) { p r i n t , p r i n t } \{\mathit{print},\mathit{print}\} { print , print }
Presence types with strength subtyping. Consider a function e q : ∀ a . { _ : a , _ : a } → b o o l \mathit{eq} : \forall a.\ \{\_ : a,\ \_ : a\} \to\mathit{bool} eq : ∀ a . { _ : a , _ : a } → bool a l i c e : { n a m e : S t r i n g , a g e : I n t } \mathit{alice} : \{\mathit{name} : \mathit{String},\ \mathit{age} : \mathit{Int}\} alice : { name : String , age : Int } b o b : { n a m e : S t r i n g , a g e ? I n t } \mathit{bob} : \{\mathit{name} : \mathit{String},\ \mathit{age}\ ?\ \mathit{Int}\} bob : { name : String , age ? Int } ( e q a l i c e b o b ) (\mathit{eq}\ \mathit{alice}\ \mathit{bob}) ( eq alice bob ) a a a a l i c e : { n a m e : S t r i n g , a g e ? I n t } \mathit{alice} : \{\mathit{name} : \mathit{String},\ \mathit{age}\ ?\ \mathit{Int}\} alice : { name : String , age ? Int } ( e q { a l i c e , b o b } ) (\mathit{eq}\ \{\mathit{alice},\ \mathit{bob}\}) ( eq { alice , bob }) a a a { n a m e : S t r i n g , a g e ? I n t } \{\mathit{name} : \mathit{String},\ \mathit{age}\ ?\ \mathit{Int}\} { name : String , age ? Int }
This approach is reminiscent of record calculi where labels have presence types [32 ] . In such a system, one can write a l i c e : { n a m e : p r e ( S t r i n g ) , a g e : p r e ( I n t ) ; a b s } \mathit{alice} : \{\mathit{name} : \mathit{pre}(\mathit{String}),\ \mathit{age} : \mathit{pre}(\mathit{Int});\ \mathit{abs}\} alice : { name : pre ( String ) , age : pre ( Int ) ; abs } b o b : { n a m e : p r e ( S t r i n g ) ; a b s } \mathit{bob} : \{\mathit{name} : \mathit{pre}(\mathit{String});\ \mathit{abs}\} bob : { name : pre ( String ) ; abs } ( e q { a l i c e , b o b } ) (\mathit{eq}\ \{\mathit{alice},\ \mathit{bob}\}) ( eq { alice , bob }) p r e ( I n t ) \mathit{pre}(\mathit{Int}) pre ( Int ) a b s \mathit{abs} abs poisoning problem [38 ] (Peyton Jones 1999), where type information from one expression pollutes another, here, via the presence of the a b s \mathit{abs} abs p r e ≤ a b s \mathit{pre} \leq\mathit{abs} pre ≤ abs
Extensions
This section explores several potential extensions to our design.
Variadic arguments. Another common paradigm for function application is variadic arguments (or variable-length arguments). If the arguments are homogeneous, this feature can be considered as passing a list. More interestingly, in dynamically typed languages like Python, we can pass a variable number of arguments of different types, as demonstrated in the program on the right. Here, display_info first takes name, and then a variable number of named arguments via kwargs and simply prints each key-value pair. We can then call it like this: display_info(name="Alice", age=2, is_logged_in=True). In Python, varying named arguments can only be at the tail of a function.
def display_info(name, **kwargs):
for key, value in kwargs.items():
print(f"{key}: {value}")Intuitively, this feature aligns well with row polymorphism featuring a polymorphic tail [38 ] . Specifically, we can define a function with type ∀ t . { n a m e ▹ S t r i n g ∣ t } → U n i t \forall t.\ \{ \mathit{name} \mathbin{\triangleright} \mathrm{String} \mid t \} \to\mathrm{Unit} ∀ t . { name ▹ String ∣ t } → Unit t t t [20 ] realize this idea for R with set-theoretic types, encoding argument lists as records whose tail is closed, open, or a row variable that captures the arguments of the ellipsis parameter (… \ldots …
While promising, in the presence of duplicated labels, this design is most effective when paired with qualified types [18 ] to enforce constraints on the tail. For example, consider using the name variable within the body of the function above. If the tail t t t t t t t t t ( n a m e ∉ t ) (\mathit{name} \notin t) ( name ∈ / t ) [16 ] , which restricts t t t [27 ] for more general row theories). We leave the exploration of this approach to future work.
Dependent default parameters. Dependent default parameters are evaluated at call-time and can refer to previously declared parameters. For example, we can define a JavaScript function: function add(x, y, z = x + y) { return z; }. This feature is, however, not widely supported among programming languages, especially those (e.g. OCaml) that do not guarantee a strict left-to-right evaluation order for function arguments. In Scala, this behaviour can be encoded via currying: def add(x:Int, y:Int)(z:Int = x + y):Int = z. We can achieve a similar encoding in our calculus: λ { x , y } . ( ( λ { z } . z ) { z : x + y } ) \lambda\{x,y\}.((\lambda\{z\}.z)\{z:x+y\}) λ { x , y } . (( λ { z } . z ) { z : x + y }) forces.
Type components. Another potential extension is to include type components within records, thereby enabling System F-style type abstractions and applications. This extension on its own should be straightforward. On the other hand, we may want to allow subsequent fields to depend on earlier type components in the record, which approaches OCaml-style modules. In either case, it may be more practical to erase types before evaluation. We leave this investigation to future work.
Additional Typing Examples
This section presents two further typing derivations. As before, we omit uninteresting derivation details.
Let-binding with pattern separation. Consider the following let-binding, whose pattern lists its labels in a different order from the record it destructures:
let { i j , i k } = { i k : 3 , i j : 5 } i n @ . i j + @ . i k \operatorname{let}\ \{i_j,i_k\}=\{i_k:3,i_j:5\}\ \mathbin{\mathsf{in}}\ @_ . i_j + @_ . i_k let { i j , i k } = { i k : 3 , i j : 5 } in @ . i j + @ . i k To type this example, subtyping first permutes the entries of the record type through S-EXT, so that they follow the order of the pattern:
B ε ; ε ⊢ { i k : 3 , i j : 5 } : { i k : N , i j : N } ⌊ ε ⌋ ε ≤ ε S-EMPTY ⋯ ε ; ε ⊢ { i k : 3 , i j : 5 } : { i j : N , i k : N } T-SUB i j : N ≤ i j : N i j : N ≤ i j : N S-EXT i k : N , i j : N ≤ i j : N , i k : N i k : N , i j : N ≤ i j : N , i k : N S-EXT { i k : N , i j : N } ≤ { i j : N , i k : N } { i k : N , i j : N } ≤ { i j : N , i k : N } S-RECORD \begin{aligned}
&\boxed{\mathrm{B}}\quad
\frac{\varepsilon;\varepsilon\vdash\{i_k:3,i_j:5\}:\{i_k:\mathbb{N},i_j:\mathbb{N}\}\quad
\frac{\lfloor\varepsilon\rfloor}{\varepsilon\le\varepsilon}\ \text{\rm S-EMPTY}\quad\cdots}
{\varepsilon;\varepsilon\vdash\{i_k:3,i_j:5\}:\{i_j:\mathbb{N},i_k:\mathbb{N}\}}\ \text{\rm T-SUB}\\
&\frac{i_j:\mathbb{N}\le i_j:\mathbb{N}}{\phantom{i_j:\mathbb{N}\le i_j:\mathbb{N}}}\ \text{\rm S-EXT}
\qquad
\frac{i_k:\mathbb{N},i_j:\mathbb{N}\le i_j:\mathbb{N},i_k:\mathbb{N}}{\phantom{i_k:\mathbb{N},i_j:\mathbb{N}\le i_j:\mathbb{N},i_k:\mathbb{N}}}\ \text{\rm S-EXT}\\
&\frac{\{i_k:\mathbb{N},i_j:\mathbb{N}\}\le\{i_j:\mathbb{N},i_k:\mathbb{N}\}}{\phantom{\{i_k:\mathbb{N},i_j:\mathbb{N}\}\le\{i_j:\mathbb{N},i_k:\mathbb{N}\}}}\ \text{\rm S-RECORD}
\end{aligned} B ε ; ε ⊢ { i k : 3 , i j : 5 } : { i j : N , i k : N } ε ; ε ⊢ { i k : 3 , i j : 5 } : { i k : N , i j : N } ε ≤ ε ⌊ ε ⌋ S-EMPTY ⋯ T-SUB i j : N ≤ i j : N i j : N ≤ i j : N S-EXT i k : N , i j : N ≤ i j : N , i k : N i k : N , i j : N ≤ i j : N , i k : N S-EXT { i k : N , i j : N } ≤ { i j : N , i k : N } { i k : N , i j : N } ≤ { i j : N , i k : N } S-RECORD Pattern separation then splits the pattern into the type of the record it destructures and the parameter names it binds:
P ε : ε ⊙ ε P-EMPTY i j : N ⊙ i j : N P-LABEL i k : N ⊙ i k : N P-LABEL i j : i j : N ⊙ i j : N i j , i k : i j : N , i k : N ⊙ i j : N , i k : N { i j , i k } : { i j : N , i k : N } ⊙ i j : N , i k : N { i j , i k } : { i j : N , i k : N } ⊙ i j : N , i k : N P-RECORD \begin{aligned}
&\boxed{\mathrm{P}}\quad
\frac{\varepsilon:\varepsilon\mathbin{\odot}\varepsilon\ \text{\rm P-EMPTY}\qquad
i_j:\mathbb{N}\mathbin{\odot}i_j:\mathbb{N}\ \text{\rm P-LABEL}\qquad
i_k:\mathbb{N}\mathbin{\odot}i_k:\mathbb{N}\ \text{\rm P-LABEL}}
{i_j:i_j:\mathbb{N}\mathbin{\odot}i_j:\mathbb{N}\qquad
i_j,i_k:i_j:\mathbb{N},i_k:\mathbb{N}\mathbin{\odot}i_j:\mathbb{N},i_k:\mathbb{N}}
\\
&\frac{\{i_j,i_k\}:\{i_j:\mathbb{N},i_k:\mathbb{N}\}\mathbin{\odot}i_j:\mathbb{N},i_k:\mathbb{N}}{\phantom{\{i_j,i_k\}:\{i_j:\mathbb{N},i_k:\mathbb{N}\}\mathbin{\odot}i_j:\mathbb{N},i_k:\mathbb{N}}}\ \text{\rm P-RECORD}
\end{aligned} P i j : i j : N ⊙ i j : N i j , i k : i j : N , i k : N ⊙ i j : N , i k : N ε : ε ⊙ ε P-EMPTY i j : N ⊙ i j : N P-LABEL i k : N ⊙ i k : N P-LABEL { i j , i k } : { i j : N , i k : N } ⊙ i j : N , i k : N { i j , i k } : { i j : N , i k : N } ⊙ i j : N , i k : N P-RECORD Finally, rule T-LET combines the two derivations, typing the body under the environment extended with the parameter names:
\frac{
\boxed{\mathrm{B}}\qquad
\boxed{\mathrm{P}}\qquad
\varepsilon;i_j:\mathbb{N},i_k:\mathbb{N}\vdash@.i_j+@.i_k:\mathbb{N}\ \text{\rm T-OP}
}{
\varepsilon;\varepsilon\vdash\mathrm{let}\ \{i_j,i_k\}=\{i_k:3,i_j:5\}\ \mathrm{in}\ @.i_j+@.i_k:\mathbb{N}
}\ \text{\rm T-LET}
Concatenation with duplicate labels. Consider the following concatenation of two records that share the label i i i
{ i = 3 } + + { i = { } } \{i=3\}++\{i=\{\}\} { i = 3 } + + { i = { }} The concatenation judgement assumes that the entries of its operands line up. Subtyping therefore first adds an optional entry to the type of the left operand through S-EMPTY:
L ε ; ε ⊢ { i = 3 } : { i ▹ N } T-RECORD ⌊ i ? { } ⌋ ? ε ≤ i ? { } S-EMPTY ⋯ ε ; ε ⊢ { i = 3 } : { i ▹ N , i ? { } } T-SUB i ▹ N ≤ i ▹ N , i ? { } i ▹ N ≤ i ▹ N , i ? { } S-EXT { i ▹ N } ≤ { i ▹ N , i ? { } } { i ▹ N } ≤ { i ▹ N , i ? { } } S-RECORD \begin{aligned}
&\boxed{\mathrm{L}}\quad
\frac{\varepsilon;\varepsilon\vdash\{i=3\}:\{i\triangleright\mathbb{N}\}\ \text{\rm T-RECORD}\qquad
\frac{\lfloor i?\{\}\rfloor?}{\varepsilon\le i?\{\}}\ \text{\rm S-EMPTY}\qquad\cdots}
{\varepsilon;\varepsilon\vdash\{i=3\}:\{i\triangleright\mathbb{N},i?\{\}\}}\ \text{\rm T-SUB}\\
&\frac{i\triangleright\mathbb{N}\le i\triangleright\mathbb{N},i?\{\}}{\phantom{i\triangleright\mathbb{N}\le i\triangleright\mathbb{N},i?\{\}}}\ \text{\rm S-EXT}\\
&\frac{\{i\triangleright\mathbb{N}\}\le\{i\triangleright\mathbb{N},i?\{\}\}}{\phantom{\{i\triangleright\mathbb{N}\}\le\{i\triangleright\mathbb{N},i?\{\}\}}}\ \text{\rm S-RECORD}
\end{aligned} L ε ; ε ⊢ { i = 3 } : { i ▹ N , i ? { }} ε ; ε ⊢ { i = 3 } : { i ▹ N } T-RECORD ε ≤ i ? { } ⌊ i ? { }⌋? S-EMPTY ⋯ T-SUB i ▹ N ≤ i ▹ N , i ? { } i ▹ N ≤ i ▹ N , i ? { } S-EXT { i ▹ N } ≤ { i ▹ N , i ? { }} { i ▹ N } ≤ { i ▹ N , i ? { }} S-RECORD Concatenation then preserves the strong entry of the left operand, while the entry of the right operand overwrites the optional one:
ε ⊕ ε ⇝ ε ε ⊕ ε ⇝ ε C-EMPTY i ▹ N ⊕ ε ⇝ i ▹ N i ▹ N ⊕ ε ⇝ i ▹ N C-STRONGL ? ⊕ ▹ ⇝ ▹ ? ⊕ ▹ ⇝ ▹ C-LATER i ▹ N , i ? { } ⊕ i ▹ { } ⇝ i ▹ N , i ▹ { } i ▹ N , i ? { } ⊕ i ▹ { } ⇝ i ▹ N , i ▹ { } C-EXT \begin{aligned}
&\frac{\varepsilon\oplus\varepsilon\rightsquigarrow\varepsilon}{\phantom{\varepsilon\oplus\varepsilon\rightsquigarrow\varepsilon}}\ \text{\rm C-EMPTY}
\qquad
\frac{i\triangleright\mathbb{N}\oplus\varepsilon\rightsquigarrow i\triangleright\mathbb{N}}{\phantom{i\triangleright\mathbb{N}\oplus\varepsilon\rightsquigarrow i\triangleright\mathbb{N}}}\ \text{\rm C-STRONGL}\\
&\frac{?\oplus\triangleright\rightsquigarrow\triangleright}{\phantom{?\oplus\triangleright\rightsquigarrow\triangleright}}\ \text{\rm C-LATER}\\
&\frac{i\triangleright\mathbb{N},i?\{\}\oplus i\triangleright\{\}\rightsquigarrow i\triangleright\mathbb{N},i\triangleright\{\}}{\phantom{i\triangleright\mathbb{N},i?\{\}\oplus i\triangleright\{\}\rightsquigarrow i\triangleright\mathbb{N},i\triangleright\{\}}}\ \text{\rm C-EXT}
\end{aligned} ε ⊕ ε ⇝ ε ε ⊕ ε ⇝ ε C-EMPTY i ▹ N ⊕ ε ⇝ i ▹ N i ▹ N ⊕ ε ⇝ i ▹ N C-STRONGL ? ⊕ ▹ ⇝ ▹ ? ⊕ ▹ ⇝ ▹ C-LATER i ▹ N , i ? { } ⊕ i ▹ { } ⇝ i ▹ N , i ▹ { } i ▹ N , i ? { } ⊕ i ▹ { } ⇝ i ▹ N , i ▹ { } C-EXT Finally, rule T-CONCAT combines the two derivations, yielding a record with two entries labelled i i i
L ε ; ε ⊢ { i = { } } : { i ▹ { } } T-RECORD C ε ; ε ⊢ { i = 3 } + + { i = { } } : { i ▹ N , i ▹ { } } T-CONCAT \frac{
\boxed{\mathrm{L}}\qquad
\varepsilon;\varepsilon\vdash\{i=\{\}\}:\{i\triangleright\{\}\}\ \text{\rm T-RECORD}\qquad
\boxed{\mathrm{C}}
}{
\varepsilon;\varepsilon\vdash\{i=3\}++\{i=\{\}\}:\{i\triangleright\mathbb{N},i\triangleright\{\}\}
}\ \text{\rm T-CONCAT} ε ; ε ⊢ { i = 3 } + + { i = { }} : { i ▹ N , i ▹ { }} L ε ; ε ⊢ { i = { }} : { i ▹ { }} T-RECORD C T-CONCAT Complete Syntax and Semantics of λ ρ ⊢ \lambda^{\rho\vdash} λ ρ ⊢
\begin{aligned}
e &::= n \mid\lambda\{c\}.e \mid\langle o_0;o_1 \mid\lambda\{c\}.e\rangle\mid e_0\ e_1 \mid\operatorname{force}\ e \mid e_0 \blacktriangleright e_1 \mid@ \mid\{r\} \mid{}\\
&\quad e_0 \mathbin{++} e_1 \mid e.i \mid e.\{i_j\} \mid e\backslash\{i_j\} \mid\operatorname{let}\ t=e_0\ \operatorname{in}\ e_1 \mid l \mid\operatorname{ref}\ e \mid{!}e \mid e_0 \mathrel{:=}e_1
\end{aligned}
term
c : : = ε ∣ c , i ⋄ t c ::= \varepsilon\mid c,i\mathbin{\diamond}t c ::= ε ∣ c , i ⋄ t record pattern
t : : = i ∣ { c } t ::= i \mid\{c\} t ::= i ∣ { c } pattern
r : : = ε ∣ r , i ⋆ e ∣ r , i ? r ::= \varepsilon\mid r,i\mathbin{\star}e \mid r,i? r ::= ε ∣ r , i ⋆ e ∣ r , i ? record
⋆ : : = = ∣ : \star::= = \mid: ⋆ ::==∣: required strength
v : : = n ∣ ⟨ o 0 ; o 1 ∣ λ { c } . e ⟩ ∣ { o } ∣ l v ::= n \mid\langle o_0;o_1 \mid\lambda\{c\}.e\rangle\mid\{o\} \mid l v ::= n ∣ ⟨ o 0 ; o 1 ∣ λ { c } . e ⟩ ∣ { o } ∣ l value
o : : = ε ∣ o , i ⋆ v ∣ o , i ? o ::= \varepsilon\mid o,i\mathbin{\star}v \mid o,i? o ::= ε ∣ o , i ⋆ v ∣ o , i ? record value
A , B : : = a ∣ N ∣ { ρ } → A ∣ { ρ } ∣ ∀ a . A ∣ Ref A A,B ::= a \mid\mathbb{N} \mid\{\rho\}\to A \mid\{\rho\} \mid\forall a.A \mid\operatorname{Ref} A A , B ::= a ∣ N ∣ { ρ } → A ∣ { ρ } ∣ ∀ a . A ∣ Ref A type
ρ : : = ε ∣ ρ , i ⋆ A \rho::= \varepsilon\mid\rho,i\mathbin{\star}A ρ ::= ε ∣ ρ , i ⋆ A record type
⋆ : : = ▹ ∣ : ∣ ? \star::= \triangleright\mid: \mid? ⋆ ::= ▹ ∣:∣ ? strength
τ : : = a ∣ N ∣ { ϱ } → τ ∣ { ϱ } ∣ Ref τ \tau::= a \mid\mathbb{N} \mid\{\varrho\}\to\tau\mid\{\varrho\} \mid\operatorname{Ref}\tau τ ::= a ∣ N ∣ { ϱ } → τ ∣ { ϱ } ∣ Ref τ monotype
ϱ : : = ε ∣ ϱ , i ⋆ τ \varrho::= \varepsilon\mid\varrho,i\mathbin{\star}\tau ϱ ::= ε ∣ ϱ , i ⋆ τ record monotype
ρ s ; ρ ⊢ e : A \rho_s;\rho\vdash e:A ρ s ; ρ ⊢ e : A (Typing)
\begin{aligned}
&\frac{\rho_s;\rho\vdash e:A \qquad A\leq B}{\rho_s;\rho\vdash e:B}
&&\text{T-sub}\\[1em]
&\frac{}{\,\rho_s;\rho\vdash n:\mathbb{N}\,}
&&\text{T-nat}\\[1em]
&\frac{a_j\notin\operatorname{ftv}(\rho_s)\qquad a_j\notin\operatorname{ftv}(\rho_0)\qquad c:\rho_1\mathbin{\odot}\rho_2\qquad\rho_s;\rho_0,\rho_2\vdash e:A}{\rho_s;\rho_0\vdash\lambda\{c\}.e:\forall a_j.\{\rho_1\}\to A}
&&\text{T-lam}\\[1em]
&\frac{a_j\notin\operatorname{ftv}(\rho_s)\qquad\rho_s;\varepsilon\vdash\{o_0\}:\{\rho_1\}\qquad\lfloor\rho_1\rfloor_{a_j}\notin\operatorname{ftv}(\rho_1)\qquad\rho_s;\varepsilon\vdash\{o_1\}:\forall a_j.\{\rho_2\}\qquad c:\rho_3\mathbin{\odot}\rho_4\qquad\rho_3\mathbin{\bullet}\rho_2\rightsquigarrow\rho_5\qquad\rho_s;\rho_1,\rho_4\vdash e:A}{\rho_s;\rho_0\vdash\langle o_0;o_1\mid\lambda\{c\}.e\rangle:\forall a_j.\{\rho_5\}\to A}
&&\text{T-closure}\\[1em]
&\frac{\rho_s;\rho_0\vdash e_0:\forall a_j.\{\rho_1\}\to A\qquad\rho_s;\rho_0\vdash e_1:\forall a_j.\{\rho_2\}\qquad\rho_1\mathbin{\bullet}\rho_2\rightsquigarrow\rho_3}{\rho_s;\rho_0\vdash e_0\ e_1:\forall a_j.\{\rho_3\}\to A}
&&\text{T-app}\\[1em]
&\frac{\rho_s;\rho\vdash e:\{\}\to A}{\rho_s;\rho\vdash\operatorname{force}\ e:A}
&&\text{T-force}\\[1em]
&\frac{\rho_s;\rho_0\vdash e_0:\{\rho_1\}\qquad\lfloor\rho_1\rfloor\qquad\rho_s;\rho_1\vdash e_1:A}{\rho_s;\rho_0\vdash e_0\blacktriangleright e_1:A}
&&\text{T-box}\\[1em]
&\frac{}{\rho_s;\rho\vdash@:\{\rho\}}
&&\text{T-env}\\[1em]
&\frac{\rho_s;\rho_0\vdash r:\rho_1}{\rho_s;\rho_0\vdash\{r\}:\{\rho_1\}}
&&\text{T-record}\\[1em]
&\frac{\rho_s;\rho_0\vdash e_0:\{\rho_1\}\qquad\rho_s;\rho_0\vdash e_1:\{\rho_2\}\qquad\rho_1\oplus\rho_2\rightsquigarrow\rho_3}{\rho_s;\rho_0\vdash e_0\mathbin{++}e_1:\{\rho_3\}}
&&\text{T-concat}\\[1em]
&\frac{\rho_s;\rho_0\vdash e:\{\rho_1,i\mathbin{\star}A\}}{\rho_s;\rho_0\vdash e.i:A}
&&\text{T-proj}\\[1em]
&\frac{\rho_s;\rho_0\vdash e:\{\rho_1,i_j\mathbin{\star_j}A_j\}}{\rho_s;\rho_0\vdash e.\{i_j\}:\{i_j\mathbin{\star_j}A_j\}}
&&\text{T-mproj}\\[1em]
&\frac{\rho_s;\rho_0\vdash e:\{\rho_1,i_j\mathbin{\star_j}A_j\}}{\rho_s;\rho_0\vdash e\backslash\{i_j\}:\{\rho_1\}}
&&\text{T-diff}\\[1em]
&\frac{\rho_s;\rho_0\vdash e_0:A\qquad t:A\mathbin{\odot}\rho_1\qquad\rho_s;\rho_0,\rho_1\vdash e_1:B}{\rho_s;\rho_0\vdash\operatorname{let}\ t=e_0\ \operatorname{in}\ e_1:B}
&&\text{T-let}\\[1em]
&\frac{}{\rho_{s0},l:A,\rho_{s1};\rho\vdash l:\operatorname{Ref}A}
&&\text{T-loc}\\[1em]
&\frac{\rho_s;\rho\vdash e:A}{\rho_s;\rho\vdash\operatorname{ref}\ e:\operatorname{Ref}A}
&&\text{T-ref}\\[1em]
&\frac{\rho_s;\rho\vdash e:\operatorname{Ref}A}{\rho_s;\rho\vdash{!}e:A}
&&\text{T-deref}\\[1em]
&\frac{\rho_s;\rho\vdash e_0:\operatorname{Ref}A\qquad\rho_s;\rho\vdash e_1:A}{\rho_s;\rho\vdash e_0\mathrel{:=}e_1:\{\}}
&&\text{T-set}
\end{aligned}
ρ s ; ρ 0 ⊢ r : ρ 1 (Record Typing) \rho_s;\rho_0 \vdash r:\rho_1 \qquad\text{(Record Typing)} ρ s ; ρ 0 ⊢ r : ρ 1 (Record Typing) ρ s ; ρ ⊢ ε : ε T-empty \frac{}{\rho_s;\rho\vdash\varepsilon:\varepsilon}\ \text{T-empty} ρ s ; ρ ⊢ ε : ε T-empty ρ s ; ρ 0 ⊢ r : ρ 1 ρ s ; ρ 0 ⊢ e : A ρ s ; ρ 0 ⊢ r , i ⋆ e : ρ 1 , i ⋆ A T-ext \frac{\rho_s;\rho_0 \vdash r:\rho_1 \qquad\rho_s;\rho_0 \vdash e:A}{\rho_s;\rho_0 \vdash r,i\star e:\rho_1,i\star A}\ \text{T-ext} ρ s ; ρ 0 ⊢ r , i ⋆ e : ρ 1 , i ⋆ A ρ s ; ρ 0 ⊢ r : ρ 1 ρ s ; ρ 0 ⊢ e : A T-ext ρ s ; ρ 0 ⊢ r : ρ 1 ρ s ; ρ 0 ⊢ e : A ρ s ; ρ 0 ⊢ r , i ? e : ρ 1 , i ? A T-ext? \frac{\rho_s;\rho_0 \vdash r:\rho_1 \qquad\rho_s;\rho_0 \vdash e:A}{\rho_s;\rho_0 \vdash r,i?e:\rho_1,i?A}\ \text{T-ext?} ρ s ; ρ 0 ⊢ r , i ? e : ρ 1 , i ? A ρ s ; ρ 0 ⊢ r : ρ 1 ρ s ; ρ 0 ⊢ e : A T-ext? A ≤ B (Subtyping) A\le B \qquad\text{(Subtyping)} A ≤ B (Subtyping) a ≤ a S-var N ≤ N S-nat \frac{}{a\le a}\ \text{S-var}
\qquad
\frac{}{\mathbb{N}\le\mathbb{N}}\ \text{S-nat} a ≤ a S-var N ≤ N S-nat ρ 1 ≤ ρ 0 A ≤ B { ρ 0 } → A ≤ { ρ 1 } → B S-arr \frac{\rho_1\le\rho_0 \qquad A\le B}{\{\rho_0\}\to A\le\{\rho_1\}\to B}\ \text{S-arr} { ρ 0 } → A ≤ { ρ 1 } → B ρ 1 ≤ ρ 0 A ≤ B S-arr ρ 0 ≤ ρ 1 { ρ 0 } ≤ { ρ 1 } S-record \frac{\rho_0\le\rho_1}{\{\rho_0\}\le\{\rho_1\}}\ \text{S-record} { ρ 0 } ≤ { ρ 1 } ρ 0 ≤ ρ 1 S-record A [ τ / a ] ≤ B ∀ a . A ≤ B S-quantL \frac{A[\tau/a]\le B}{\forall a.A\le B}\ \text{S-quantL} ∀ a . A ≤ B A [ τ / a ] ≤ B S-quantL a ∉ ftv ( A ) A ≤ B A ≤ ∀ a . B S-quantR \frac{a\notin\operatorname{ftv}(A) \qquad A\le B}{A\le\forall a.B}\ \text{S-quantR} A ≤ ∀ a . B a ∈ / ftv ( A ) A ≤ B S-quantR Ref A ≤ Ref A S-ref \frac{}{\operatorname{Ref}\ A\le\operatorname{Ref}\ A}\ \text{S-ref} Ref A ≤ Ref A S-ref ρ 0 ≤ ρ 1 (Record Subtyping) \rho_0\le\rho_1 \qquad\text{(Record Subtyping)} ρ 0 ≤ ρ 1 (Record Subtyping) ε ≤ ρ S-empty \frac{}{\varepsilon\le\rho}\ \text{S-empty} ε ≤ ρ S-empty ρ 0 ≤ ρ 1 , ρ 2 i ∉ ρ 1 ⋆ 0 ≤ ⋆ 1 A ≤ B i ⋆ 0 A , ρ 0 ≤ ρ 1 , i ⋆ 1 B , ρ 2 S-ext \frac{\rho_0\le\rho_1,\rho_2 \qquad i\notin\rho_1 \qquad\star_0\le\star_1 \qquad A\le B}{i\star_0 A,\rho_0\le\rho_1,i\star_1 B,\rho_2}\ \text{S-ext} i ⋆ 0 A , ρ 0 ≤ ρ 1 , i ⋆ 1 B , ρ 2 ρ 0 ≤ ρ 1 , ρ 2 i ∈ / ρ 1 ⋆ 0 ≤ ⋆ 1 A ≤ B S-ext ⋆ 0 ≤ ⋆ 1 (Strength Subtyping) \star_0\le\star_1 \qquad\text{(Strength Subtyping)} ⋆ 0 ≤ ⋆ 1 (Strength Subtyping) ⋆ ≤ ⋆ S-refl : ≤ ? S-lt \frac{}{\star\le\star}\ \text{S-refl}
\qquad
\frac{}{:}\le?\ \text{S-lt} ⋆ ≤ ⋆ S-refl : ≤ ? S-lt c : ρ 0 ⊙ ρ 1 (Record Pattern Separation) c:\rho_0\mathbin{\odot}\rho_1 \qquad\text{(Record Pattern Separation)} c : ρ 0 ⊙ ρ 1 (Record Pattern Separation) ε : ε ⊙ ε P-empty \frac{}{\varepsilon:\varepsilon\mathbin{\odot}\varepsilon}\ \text{P-empty} ε : ε ⊙ ε P-empty c : ρ 0 ⊙ ρ 1 t : A ⊙ ρ 2 ( c , i ⋄ t ) : ( ρ 0 , i : A ) ⊙ ρ 1 , ρ 2 P-ext \frac{c:\rho_0\mathbin{\odot}\rho_1 \qquad t:A\mathbin{\odot}\rho_2}{(c,i\diamond t):(\rho_0,i:A)\mathbin{\odot}\rho_1,\rho_2}\ \text{P-ext} ( c , i ⋄ t ) : ( ρ 0 , i : A ) ⊙ ρ 1 , ρ 2 c : ρ 0 ⊙ ρ 1 t : A ⊙ ρ 2 P-ext t : A ⊙ ρ (Pattern Separation) t:A\mathbin{\odot}\rho\qquad\text{(Pattern Separation)} t : A ⊙ ρ (Pattern Separation) i : A ⊙ ( i : A ) P-label \frac{}{i:A\mathbin{\odot}(i:A)}\ \text{P-label} i : A ⊙ ( i : A ) P-label c : ρ 0 ⊙ ρ 1 { c } : { ρ 0 } ⊙ ρ 1 P-record \frac{c:\rho_0\mathbin{\odot}\rho_1}{\{c\}:\{\rho_0\}\mathbin{\odot}\rho_1}\ \text{P-record} { c } : { ρ 0 } ⊙ ρ 1 c : ρ 0 ⊙ ρ 1 P-record ρ 0 ∙ ρ 1 ↠ ρ 2 (Record Type App) \rho_0\mathbin{\bullet}\rho_1\mathrel{\twoheadrightarrow}\rho_2 \qquad\text{(Record Type App)} ρ 0 ∙ ρ 1 ↠ ρ 2 (Record Type App) ε ∙ ε ↠ ε A-empty \frac{}{\varepsilon\mathbin{\bullet}\varepsilon\mathrel{\twoheadrightarrow}\varepsilon}\ \text{A-empty} ε ∙ ε ↠ ε A-empty ρ 0 ∙ ρ 1 ↠ ρ 2 ρ 0 , i : A ∙ ρ 1 , i ▹ A ↠ ρ 2 A-weakStrong \frac{\rho_0\mathbin{\bullet}\rho_1\mathrel{\twoheadrightarrow}\rho_2}{\rho_0,i:A\mathbin{\bullet}\rho_1,i\triangleright A\mathrel{\twoheadrightarrow}\rho_2}\ \text{A-weakStrong} ρ 0 , i : A ∙ ρ 1 , i ▹ A ↠ ρ 2 ρ 0 ∙ ρ 1 ↠ ρ 2 A-weakStrong ρ 0 ∙ ρ 1 ↠ ρ 2 ρ 0 , i ? A ∙ ρ 1 , i ▹ A ↠ ρ 2 A-optionalStrong \frac{\rho_0\mathbin{\bullet}\rho_1\mathrel{\twoheadrightarrow}\rho_2}{\rho_0,i?A\mathbin{\bullet}\rho_1,i\triangleright A\mathrel{\twoheadrightarrow}\rho_2}\ \text{A-optionalStrong} ρ 0 , i ? A ∙ ρ 1 , i ▹ A ↠ ρ 2 ρ 0 ∙ ρ 1 ↠ ρ 2 A-optionalStrong ρ 0 ∙ ρ 1 ↠ ρ 2 ⋆ 0 ∙ ⋆ 1 ↠ ⋆ 2 ρ 0 , i ⋆ 0 A ∙ ρ 1 , i ⋆ 1 A ↠ ρ 2 , i ⋆ 2 A A-ext \frac{\rho_0\mathbin{\bullet}\rho_1\mathrel{\twoheadrightarrow}\rho_2 \qquad\star_0\mathbin{\bullet}\star_1\mathrel{\twoheadrightarrow}\star_2}{\rho_0,i\star_0 A\mathbin{\bullet}\rho_1,i\star_1 A\mathrel{\twoheadrightarrow}\rho_2,i\star_2 A}\ \text{A-ext} ρ 0 , i ⋆ 0 A ∙ ρ 1 , i ⋆ 1 A ↠ ρ 2 , i ⋆ 2 A ρ 0 ∙ ρ 1 ↠ ρ 2 ⋆ 0 ∙ ⋆ 1 ↠ ⋆ 2 A-ext ⋆ 0 ∙ ⋆ 1 ↠ ⋆ 2 (Strength App) \star_0\mathbin{\bullet}\star_1\mathrel{\twoheadrightarrow}\star_2 \qquad\text{(Strength App)} ⋆ 0 ∙ ⋆ 1 ↠ ⋆ 2 (Strength App) : ∙ ? ↠ : A-later : ∙ : ↠ ? A-set \frac{}{:\mathbin{\bullet}?\mathrel{\twoheadrightarrow}:}\ \text{A-later}
\qquad
\frac{}{:\mathbin{\bullet}:\mathrel{\twoheadrightarrow}?}\ \text{A-set} : ∙ ? ↠ : A-later : ∙ : ↠ ? A-set ? ∙ ? ↠ ? A-leave ? ∙ : ↠ ? A-replace \frac{}{?\mathbin{\bullet}?\mathrel{\twoheadrightarrow}?}\ \text{A-leave}
\qquad
\frac{}{?\mathbin{\bullet}:\mathrel{\twoheadrightarrow}?}\ \text{A-replace} ? ∙ ? ↠ ? A-leave ? ∙ : ↠ ? A-replace ρ 0 ⊕ ρ 1 ⇀ ρ 2 (Record Type Concat) \rho_0\mathbin{\oplus}\rho_1\mathrel{\rightharpoonup}\rho_2 \qquad\text{(Record Type Concat)} ρ 0 ⊕ ρ 1 ⇀ ρ 2 (Record Type Concat) ε ⊕ ε ⇀ ε C-empty \frac{}{\varepsilon\mathbin{\oplus}\varepsilon\mathrel{\rightharpoonup}\varepsilon}\ \text{C-empty} ε ⊕ ε ⇀ ε C-empty ρ 0 ⊕ ρ 1 ⇀ ρ 2 ρ 0 , i ▹ A ⊕ ρ 1 ⇀ ρ 2 , i ▹ A C-strongL \frac{\rho_0\mathbin{\oplus}\rho_1\mathrel{\rightharpoonup}\rho_2}{\rho_0,i\triangleright A\mathbin{\oplus}\rho_1\mathrel{\rightharpoonup}\rho_2,i\triangleright A}\ \text{C-strongL} ρ 0 , i ▹ A ⊕ ρ 1 ⇀ ρ 2 , i ▹ A ρ 0 ⊕ ρ 1 ⇀ ρ 2 C-strongL ρ 0 ⊕ ρ 1 ⇀ ρ 2 ⋆ 0 ⊕ ⋆ 1 ⇀ ⋆ 2 ρ 0 , i ⋆ 0 A ⊕ ρ 1 , i ⋆ 1 A ⇀ ρ 2 , i ⋆ 2 A C-ext \frac{\rho_0\mathbin{\oplus}\rho_1\mathrel{\rightharpoonup}\rho_2 \qquad\star_0\mathbin{\oplus}\star_1\mathrel{\rightharpoonup}\star_2}{\rho_0,i\star_0 A\mathbin{\oplus}\rho_1,i\star_1 A\mathrel{\rightharpoonup}\rho_2,i\star_2 A}\ \text{C-ext} ρ 0 , i ⋆ 0 A ⊕ ρ 1 , i ⋆ 1 A ⇀ ρ 2 , i ⋆ 2 A ρ 0 ⊕ ρ 1 ⇀ ρ 2 ⋆ 0 ⊕ ⋆ 1 ⇀ ⋆ 2 C-ext ⋆ 0 ⊕ ⋆ 1 → ⋆ 2 \star_{0} \oplus\star_{1} \mathrel{\to} \star_{2} ⋆ 0 ⊕ ⋆ 1 → ⋆ 2 C-strongR
: ⊕ ▹ → ▹ : \oplus\triangleright\mathrel{\to} \triangleright : ⊕ ▹ → ▹ C-later
? ⊕ ⋆ → ⋆ ? \oplus\star\mathrel{\to} \star ? ⊕ ⋆ → ⋆ C-leave
: ⊕ ? → : : \oplus? \mathrel{\to} : : ⊕ ? → : C-replace
: ⊕ : → : : \oplus: \mathrel{\to} : : ⊕ : → : ⌊ ρ ⌋ ⋆ \lfloor\rho\rfloor^{\star} ⌊ ρ ⌋ ⋆ U-empty
[ ε ] ⋆ \frac{}{[\varepsilon]^{\star}} [ ε ] ⋆ U-ext
[ ρ ] ⋆ [ ρ , ı ⋆ A ] ⋆ \frac{[\rho]^{\star}}{[\rho,\imath\star A]^{\star}} [ ρ , ⋆ A ] ⋆ [ ρ ] ⋆ o ⊢ e ⟶ e ′ o \vdash e \mathrel{\longrightarrow} e' o ⊢ e ⟶ e ′ E-lam
o ⊢ λ { c } . e ; o s ⟶ ⟨ o ; ε ∣ λ { c } . e ⟩ ; o s \frac{}{o \vdash\lambda\{c\}.e;o_s \mathrel{\longrightarrow} \langle o;\varepsilon\mid\lambda\{c\}.e\rangle;o_s} o ⊢ λ { c } . e ; o s ⟶ ⟨ o ; ε ∣ λ { c } . e ⟩ ; o s E-appl
o ⊢ e 0 ; o s ⟶ e 0 ′ ; o s ′ o ⊢ e 0 e 1 ; o s ⟶ e 0 ′ e 1 ; o s ′ \frac{o \vdash e_0;o_s \mathrel{\longrightarrow} e_0';o_s'}{o \vdash e_0\ e_1;o_s \mathrel{\longrightarrow} e_0'\ e_1;o_s'} o ⊢ e 0 e 1 ; o s ⟶ e 0 ′ e 1 ; o s ′ o ⊢ e 0 ; o s ⟶ e 0 ′ ; o s ′ E-appr
o ⊢ e ; o s ⟶ e ′ ; o s ′ o ⊢ v e ; o s ⟶ v e ′ ; o s ′ \frac{o \vdash e;o_s \mathrel{\longrightarrow} e';o_s'}{o \vdash v\ e;o_s \mathrel{\longrightarrow} v\ e';o_s'} o ⊢ v e ; o s ⟶ v e ′ ; o s ′ o ⊢ e ; o s ⟶ e ′ ; o s ′ E-app
o 0 ⊢ ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ { o 3 } ; o s ⟶ ⟨ o 1 ; o 2 + + o 3 ∣ λ { c } . e ⟩ ; o s \frac{o_0 \vdash\langle o_1;o_2 \mid\lambda\{c\}.e\rangle\{o_3\};o_s \mathrel{\longrightarrow} \langle o_1;o_2 \mathbin{++} o_3 \mid\lambda\{c\}.e\rangle;o_s}{} o 0 ⊢ ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ { o 3 } ; o s ⟶ ⟨ o 1 ; o 2 + + o 3 ∣ λ { c } . e ⟩ ; o s E-force
o ⊢ e ; o s ⟶ e ′ ; o s ′ o ⊢ force e ; o s ⟶ force e ′ ; o s ′ \frac{o \vdash e;o_s \mathrel{\longrightarrow} e';o_s'}{o \vdash\operatorname{force}\ e;o_s \mathrel{\longrightarrow} \operatorname{force}\ e';o_s'} o ⊢ force e ; o s ⟶ force e ′ ; o s ′ o ⊢ e ; o s ⟶ e ′ ; o s ′ E-forceClosure
expand ( c ; o 2 ) = o 3 o 0 ⊢ force ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ ; o s ⟶ { o 1 , o 3 } ▹ e ; o s \frac{\operatorname{expand}(c;o_2)=o_3}{o_0 \vdash\operatorname{force}\langle o_1;o_2 \mid\lambda\{c\}.e\rangle;o_s \mathrel{\longrightarrow} \{o_1,o_3\}\mathbin{\triangleright}e;o_s} o 0 ⊢ force ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ ; o s ⟶ { o 1 , o 3 } ▹ e ; o s expand ( c ; o 2 ) = o 3 E-boxl
o ⊢ e 0 ; o s ⟶ e 0 ′ ; o s ′ o ⊢ e 0 ▹ e 1 ; o s ⟶ e 0 ′ ▹ e 1 ; o s ′ \frac{o \vdash e_0;o_s \mathrel{\longrightarrow} e_0';o_s'}{o \vdash e_0\mathbin{\triangleright}e_1;o_s \mathrel{\longrightarrow} e_0'\mathbin{\triangleright}e_1;o_s'} o ⊢ e 0 ▹ e 1 ; o s ⟶ e 0 ′ ▹ e 1 ; o s ′ o ⊢ e 0 ; o s ⟶ e 0 ′ ; o s ′ E-boxr
o 1 ⊢ e ; o s ⟶ e ′ ; o s ′ o 0 ⊢ { o 1 } ▹ e ; o s ⟶ { o 1 } ▹ e ′ ; o s ′ \frac{o_1 \vdash e;o_s \mathrel{\longrightarrow} e';o_s'}{o_0 \vdash\{o_1\}\mathbin{\triangleright}e;o_s \mathrel{\longrightarrow} \{o_1\}\mathbin{\triangleright}e';o_s'} o 0 ⊢ { o 1 } ▹ e ; o s ⟶ { o 1 } ▹ e ′ ; o s ′ o 1 ⊢ e ; o s ⟶ e ′ ; o s ′ E-box
o 0 ⊢ { o 1 } ▹ v ; o s ⟶ v ; o s \frac{o_0 \vdash\{o_1\}\mathbin{\triangleright}v;o_s \mathrel{\longrightarrow} v;o_s}{} o 0 ⊢ { o 1 } ▹ v ; o s ⟶ v ; o s E-env
\frac{}{o \vdash@;o_s \mathrel{\longrightarrow} \{o\};o_s}
E-extl
o ⊢ { r } ; o s ⟶ { r ′ } ; o s ′ o ⊢ { r , ı ⋆ e } ; o s ⟶ { r ′ , ı ⋆ e } ; o s ′ \frac{o \vdash\{r\};o_s \mathrel{\longrightarrow} \{r'\};o_s'}{o \vdash\{r,\imath\star e\};o_s \mathrel{\longrightarrow} \{r',\imath\star e\};o_s'} o ⊢ { r , ⋆ e } ; o s ⟶ { r ′ , ⋆ e } ; o s ′ o ⊢ { r } ; o s ⟶ { r ′ } ; o s ′ E-extl?
o ⊢ { r } ; o s ⟶ { r ′ } ; o s ′ o ⊢ { r , ı ? } ; o s ⟶ { r ′ , ı ? } ; o s ′ \frac{o \vdash\{r\};o_s \mathrel{\longrightarrow} \{r'\};o_s'}{o \vdash\{r,\imath?\};o_s \mathrel{\longrightarrow} \{r',\imath?\};o_s'} o ⊢ { r , ?} ; o s ⟶ { r ′ , ?} ; o s ′ o ⊢ { r } ; o s ⟶ { r ′ } ; o s ′ E-extr
o 0 ⊢ e ; o s ⟶ e ′ ; o s ′ o 0 ⊢ { o 1 , ı ⋆ e } ; o s ⟶ { o 1 , ı ⋆ e ′ } ; o s ′ \frac{o_0 \vdash e;o_s \mathrel{\longrightarrow} e';o_s'}{o_0 \vdash\{o_1,\imath\star e\};o_s \mathrel{\longrightarrow} \{o_1,\imath\star e'\};o_s'} o 0 ⊢ { o 1 , ⋆ e } ; o s ⟶ { o 1 , ⋆ e ′ } ; o s ′ o 0 ⊢ e ; o s ⟶ e ′ ; o s ′ E-concatl
o ⊢ e 0 ; o s ⟶ e 0 ′ ; o s ′ o ⊢ e 0 + + e 1 ; o s ⟶ e 0 ′ + + e 1 ; o s ′ \frac{o \vdash e_0;o_s \mathrel{\longrightarrow} e_0';o_s'}{o \vdash e_0 ++ e_1;o_s \mathrel{\longrightarrow} e_0' ++ e_1;o_s'} o ⊢ e 0 + + e 1 ; o s ⟶ e 0 ′ + + e 1 ; o s ′ o ⊢ e 0 ; o s ⟶ e 0 ′ ; o s ′ E-concatr
o ⊢ e ; o s ⟶ e ′ ; o s ′ o ⊢ v + + e ; o s ⟶ v + + e ′ ; o s ′ \frac{o \vdash e;o_s \mathrel{\longrightarrow} e';o_s'}{o \vdash v ++ e;o_s \mathrel{\longrightarrow} v ++ e';o_s'} o ⊢ v + + e ; o s ⟶ v + + e ′ ; o s ′ o ⊢ e ; o s ⟶ e ′ ; o s ′ E-concat
o 0 ⊢ { o 1 } + + { o 2 } ; o s ⟶ { o 1 + + o 2 } ; o s \frac{o_0 \vdash\{o_1\} ++ \{o_2\};o_s \mathrel{\longrightarrow} \{o_1 ++ o_2\};o_s}{} o 0 ⊢ { o 1 } + + { o 2 } ; o s ⟶ { o 1 + + o 2 } ; o s E-proj
o ⊢ e ; o s ⟶ e ′ ; o s ′ o ⊢ e . ı ; o s ⟶ e ′ . ı ; o s ′ \frac{o \vdash e;o_s \mathrel{\longrightarrow} e';o_s'}{o \vdash e.\imath;o_s \mathrel{\longrightarrow} e'.\imath;o_s'} o ⊢ e . ; o s ⟶ e ′ . ; o s ′ o ⊢ e ; o s ⟶ e ′ ; o s ′ E-projRecord
proj ( o 1 ; ı ) = v o 0 ⊢ { o 1 } . ı ; o s ⟶ v ; o s \frac{\operatorname{proj}(o_1;\imath)=v}{o_0 \vdash\{o_1\}.\imath;o_s \mathrel{\longrightarrow} v;o_s} o 0 ⊢ { o 1 } . ; o s ⟶ v ; o s proj ( o 1 ; ) = v E-mproj
o ⊢ e ; o s ⟶ e ′ ; o s ′ o ⊢ e . { ı ‾ } ; o s ⟶ e ′ . { ı ‾ } ; o s ′ \frac{o \vdash e;o_s \mathrel{\longrightarrow} e';o_s'}{o \vdash e.\{\overline{\imath}\};o_s \mathrel{\longrightarrow} e'.\{\overline{\imath}\};o_s'} o ⊢ e . { } ; o s ⟶ e ′ . { } ; o s ′ o ⊢ e ; o s ⟶ e ′ ; o s ′ E-mprojRecord
mproj ( o 1 ; ı ‾ ) = o 2 o 0 ⊢ { o 1 } . { ı ‾ } ; o s ⟶ { o 2 } ; o s \frac{\operatorname{mproj}(o_1;\overline{\imath})=o_2}{o_0 \vdash\{o_1\}.\{\overline{\imath}\};o_s \mathrel{\longrightarrow} \{o_2\};o_s} o 0 ⊢ { o 1 } . { } ; o s ⟶ { o 2 } ; o s mproj ( o 1 ; ) = o 2 E-diff
o ⊢ e ; o s ⟶ e ′ ; o s ′ o ⊢ e \ { ı ‾ } ; o s ⟶ e ′ \ { ı ‾ } ; o s ′ \frac{o \vdash e;o_s \mathrel{\longrightarrow} e';o_s'}{o \vdash e\backslash\{\overline{\imath}\};o_s \mathrel{\longrightarrow} e'\backslash\{\overline{\imath}\};o_s'} o ⊢ e \ { } ; o s ⟶ e ′ \ { } ; o s ′ o ⊢ e ; o s ⟶ e ′ ; o s ′ E-diffRecord
diff ( o 1 ; ı ‾ ) = o 2 o 0 ⊢ { o 1 } \ { ı ‾ } ; o s ⟶ { o 2 } ; o s \frac{\operatorname{diff}(o_1;\overline{\imath})=o_2}{o_0 \vdash\{o_1\}\backslash\{\overline{\imath}\};o_s \mathrel{\longrightarrow} \{o_2\};o_s} o 0 ⊢ { o 1 } \ { } ; o s ⟶ { o 2 } ; o s diff ( o 1 ; ) = o 2 E-let
o ⊢ e 0 ; o s ⟶ e 0 ′ ; o s ′ o ⊢ let t = e 0 in e 1 ; o s ⟶ let t = e 0 ′ in e 1 ; o s ′ \frac{o \vdash e_0;o_s \mathrel{\longrightarrow} e_0';o_s'}{o \vdash\operatorname{let}t=e_0\operatorname{ in}e_1;o_s \mathrel{\longrightarrow} \operatorname{let}t=e_0'\operatorname{ in}e_1;o_s'} o ⊢ let t = e 0 in e 1 ; o s ⟶ let t = e 0 ′ in e 1 ; o s ′ o ⊢ e 0 ; o s ⟶ e 0 ′ ; o s ′ E-letv
expand ( t ; v ) = o 1 o 0 ⊢ let t = v in e ; o s ⟶ { o 0 , o 1 } ▹ e ; o s \frac{\operatorname{expand}(t;v)=o_1}{o_0 \vdash\operatorname{let}t=v\operatorname{ in}e;o_s \mathrel{\longrightarrow} \{o_0,o_1\}\mathbin{\triangleright}e;o_s} o 0 ⊢ let t = v in e ; o s ⟶ { o 0 , o 1 } ▹ e ; o s expand ( t ; v ) = o 1 E-ref
o ⊢ e ; o s ⟶ e ′ ; o s ′ o ⊢ ref e ; o s ⟶ ref e ′ ; o s ′ \frac{o \vdash e;o_s \mathrel{\longrightarrow} e';o_s'}{o \vdash\operatorname{ref}\ e;o_s \mathrel{\longrightarrow} \operatorname{ref}\ e';o_s'} o ⊢ ref e ; o s ⟶ ref e ′ ; o s ′ o ⊢ e ; o s ⟶ e ′ ; o s ′ E-refv
l ∉ o s o ⊢ ref v ; o s ⟶ l ; o s , l : v \frac{l \notin o_s}{o \vdash\operatorname{ref}\ v;o_s \mathrel{\longrightarrow} l;o_s,l:v} o ⊢ ref v ; o s ⟶ l ; o s , l : v l ∈ / o s E-deref o ⊢ e ; o s ⟶ e ′ ; o s ′ o ⊢ ! e ; o s ⟶ ! e ′ ; o s ′ \begin{aligned}
&\text{E-deref}\\
&\frac{o \vdash e; o_s \longrightarrow e'; o'_s}{o \vdash!e; o_s \longrightarrow!e'; o'_s}
\end{aligned} E-deref o ⊢ ! e ; o s ⟶ ! e ′ ; o s ′ o ⊢ e ; o s ⟶ e ′ ; o s ′ E-derefLoc o ⊢ ! l ; o s ⟶ { o s } . l ; o s \begin{aligned}
&\text{E-derefLoc}\\
&\frac{}{o \vdash!l; o_s \longrightarrow\{o_s\}.l; o_s}
\end{aligned} E-derefLoc o ⊢ ! l ; o s ⟶ { o s } . l ; o s E-setl o ⊢ e 0 ; o s ⟶ e 0 ′ ; o s ′ o ⊢ e 0 : = e 1 ; o s ⟶ e 0 ′ : = e 1 ; o s ′ \begin{aligned}
&\text{E-setl}\\
&\frac{o \vdash e_0; o_s \longrightarrow e'_0; o'_s}{o \vdash e_0 := e_1; o_s \longrightarrow e'_0 := e_1; o'_s}
\end{aligned} E-setl o ⊢ e 0 := e 1 ; o s ⟶ e 0 ′ := e 1 ; o s ′ o ⊢ e 0 ; o s ⟶ e 0 ′ ; o s ′ E-setr o ⊢ e ; o s ⟶ e ′ ; o s ′ o ⊢ v : = e ; o s ⟶ v : = e ′ ; o s ′ \begin{aligned}
&\text{E-setr}\\
&\frac{o \vdash e; o_s \longrightarrow e'; o'_s}{o \vdash v := e; o_s \longrightarrow v := e'; o'_s}
\end{aligned} E-setr o ⊢ v := e ; o s ⟶ v := e ′ ; o s ′ o ⊢ e ; o s ⟶ e ′ ; o s ′ E-set o ⊢ l : = v ; o s ⟶ { } ; o s + + l : v \begin{aligned}
&\text{E-set}\\
&\frac{}{o \vdash l := v; o_s \longrightarrow\{\}; o_s \mathbin{+\!\!+} l:v}
\end{aligned} E-set o ⊢ l := v ; o s ⟶ { } ; o s + + l : v o ⊢ e ; o s ⟹ v ; o s ′ o \vdash e; o_s \Longrightarrow v; o'_s o ⊢ e ; o s ⟹ v ; o s ′ B-nat o ⊢ n ; o s ⟹ n ; o s \begin{aligned}
&\text{B-nat}\\
&\frac{}{o \vdash n; o_s \Longrightarrow n; o_s}
\end{aligned} B-nat o ⊢ n ; o s ⟹ n ; o s B-lam o ⊢ λ { c } . e ; o s ⟹ ⟨ o ; ε ∣ λ { c } . e ⟩ ; o s \begin{aligned}
&\text{B-lam}\\
&\frac{}{o \vdash\lambda\{c\}.e; o_s \Longrightarrow\langle o;\varepsilon\mid\lambda\{c\}.e\rangle; o_s}
\end{aligned} B-lam o ⊢ λ { c } . e ; o s ⟹ ⟨ o ; ε ∣ λ { c } . e ⟩ ; o s B-closure o 0 ⊢ ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ ; o s ⟹ ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ ; o s \begin{aligned}
&\text{B-closure}\\
&\frac{}{o_0 \vdash\langle o_1;o_2 \mid\lambda\{c\}.e\rangle; o_s \Longrightarrow\langle o_1;o_2 \mid\lambda\{c\}.e\rangle; o_s}
\end{aligned} B-closure o 0 ⊢ ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ ; o s ⟹ ⟨ o 1 ; o 2 ∣ λ { c } . e ⟩ ; o s B-app o 0 ⊢ e 0 ; o s 0 ⟹ ⟨ o 1 ; o 2 ∣ λ { c } . e ′ ⟩ ; o s 1 o 0 ⊢ e 1 ; o s 1 ⟹ { o 3 } ; o s 2 o 0 ⊢ e 0 e 1 ; o s 0 ⟹ ⟨ o 1 ; o 2 + + o 3 ∣ λ { c } . e ′ ⟩ ; o s 2 \begin{aligned}
&\text{B-app}\\
&\frac{o_0 \vdash e_0; o_{s0} \Longrightarrow\langle o_1;o_2 \mid\lambda\{c\}.e'\rangle; o_{s1}
\qquad
o_0 \vdash e_1; o_{s1} \Longrightarrow\{o_3\}; o_{s2}}
{o_0 \vdash e_0\ e_1; o_{s0} \Longrightarrow\langle o_1;o_2 \mathbin{+\!\!+} o_3 \mid\lambda\{c\}.e'\rangle; o_{s2}}
\end{aligned} B-app o 0 ⊢ e 0 e 1 ; o s 0 ⟹ ⟨ o 1 ; o 2 + + o 3 ∣ λ { c } . e ′ ⟩ ; o s 2 o 0 ⊢ e 0 ; o s 0 ⟹ ⟨ o 1 ; o 2 ∣ λ { c } . e ′ ⟩ ; o s 1 o 0 ⊢ e 1 ; o s 1 ⟹ { o 3 } ; o s 2 B-force o 0 ⊢ e ; o s 0 ⟹ ⟨ o 1 ; o 2 ∣ λ { c } . e ′ ⟩ ; o s 1 expand ( c ; o 2 ) = o 3 o 1 , o 3 ⊢ e ′ ; o s 1 ⟹ v ; o s 2 o 0 ⊢ force e ; o s 0 ⟹ v ; o s 2 \begin{aligned}
&\text{B-force}\\
&\frac{o_0 \vdash e; o_{s0} \Longrightarrow\langle o_1;o_2 \mid\lambda\{c\}.e'\rangle; o_{s1}
\qquad
\operatorname{expand}(c;o_2)=o_3
\qquad
o_1,o_3 \vdash e'; o_{s1} \Longrightarrow v; o_{s2}}
{o_0 \vdash\operatorname{force}\ e; o_{s0} \Longrightarrow v; o_{s2}}
\end{aligned} B-force o 0 ⊢ force e ; o s 0 ⟹ v ; o s 2 o 0 ⊢ e ; o s 0 ⟹ ⟨ o 1 ; o 2 ∣ λ { c } . e ′ ⟩ ; o s 1 expand ( c ; o 2 ) = o 3 o 1 , o 3 ⊢ e ′ ; o s 1 ⟹ v ; o s 2 B-box o 0 ⊢ e 0 ; o s 0 ⟹ { o 1 } ; o s 1 o 1 ⊢ e 1 ; o s 1 ⟹ v 1 ; o s 2 o 0 ⊢ e 0 ▶ e 1 ; o s 0 ⟹ v 1 ; o s 2 \begin{aligned}
&\text{B-box}\\
&\frac{o_0 \vdash e_0; o_{s0} \Longrightarrow\{o_1\}; o_{s1}
\qquad
o_1 \vdash e_1; o_{s1} \Longrightarrow v_1; o_{s2}}
{o_0 \vdash e_0 \mathbin{\blacktriangleright} e_1; o_{s0} \Longrightarrow v_1; o_{s2}}
\end{aligned} B-box o 0 ⊢ e 0 ▶ e 1 ; o s 0 ⟹ v 1 ; o s 2 o 0 ⊢ e 0 ; o s 0 ⟹ { o 1 } ; o s 1 o 1 ⊢ e 1 ; o s 1 ⟹ v 1 ; o s 2 \begin{aligned}
&\text{B-env}\\
&\frac{}{o \vdash@; o_s \Longrightarrow\{o\}; o_s}
\end{aligned}
B-empty o ⊢ { } ; o s ⟹ { } ; o s \begin{aligned}
&\text{B-empty}\\
&\frac{}{o \vdash\{\}; o_s \Longrightarrow\{\}; o_s}
\end{aligned} B-empty o ⊢ { } ; o s ⟹ { } ; o s B-ext o 0 ⊢ { r } ; o s 0 ⟹ { o 1 } ; o s 1 o 0 ⊢ e ; o s 1 ⟹ v ; o s 2 o 0 ⊢ { r , i ▶ e } ; o s 0 ⟹ { o 1 , i ▶ v } ; o s 2 \begin{aligned}
&\text{B-ext}\\
&\frac{o_0 \vdash\{r\}; o_{s0} \Longrightarrow\{o_1\}; o_{s1}
\qquad
o_0 \vdash e; o_{s1} \Longrightarrow v; o_{s2}}
{o_0 \vdash\{r,i \mathbin{\blacktriangleright} e\}; o_{s0} \Longrightarrow\{o_1,i \mathbin{\blacktriangleright} v\}; o_{s2}}
\end{aligned} B-ext o 0 ⊢ { r , i ▶ e } ; o s 0 ⟹ { o 1 , i ▶ v } ; o s 2 o 0 ⊢ { r } ; o s 0 ⟹ { o 1 } ; o s 1 o 0 ⊢ e ; o s 1 ⟹ v ; o s 2 B-ext? o 0 ⊢ { r } ; o s ⟹ { o 1 } ; o s ′ o 0 ⊢ { r , i ? } ; o s ⟹ { o 1 , i ? } ; o s ′ \begin{aligned}
&\text{B-ext?}\\
&\frac{o_0 \vdash\{r\}; o_s \Longrightarrow\{o_1\}; o'_s}
{o_0 \vdash\{r,i\mathbin{?}\}; o_s \Longrightarrow\{o_1,i\mathbin{?}\}; o'_s}
\end{aligned} B-ext? o 0 ⊢ { r , i ? } ; o s ⟹ { o 1 , i ? } ; o s ′ o 0 ⊢ { r } ; o s ⟹ { o 1 } ; o s ′ B-concat o 0 ⊢ e 0 ; o s 0 ⟹ { o 1 } ; o s 1 o 0 ⊢ e 1 ; o s 1 ⟹ { o 2 } ; o s 2 o 0 ⊢ e 0 + + e 1 ; o s 0 ⟹ { o 1 + + o 2 } ; o s 2 \begin{aligned}
&\text{B-concat}\\
&\frac{o_0 \vdash e_0; o_{s0} \Longrightarrow\{o_1\}; o_{s1}
\qquad
o_0 \vdash e_1; o_{s1} \Longrightarrow\{o_2\}; o_{s2}}
{o_0 \vdash e_0 ++ e_1; o_{s0} \Longrightarrow\{o_1 ++ o_2\}; o_{s2}}
\end{aligned} B-concat o 0 ⊢ e 0 + + e 1 ; o s 0 ⟹ { o 1 + + o 2 } ; o s 2 o 0 ⊢ e 0 ; o s 0 ⟹ { o 1 } ; o s 1 o 0 ⊢ e 1 ; o s 1 ⟹ { o 2 } ; o s 2 B-proj o 0 ⊢ e ; o s ⟹ { o 1 } ; o s ′ proj ( o 1 ; i ) = v o 0 ⊢ e . i ; o s ⟹ v ; o s ′ \begin{aligned}
&\text{B-proj}\\
&\frac{o_0 \vdash e; o_s \Longrightarrow\{o_1\}; o'_s
\qquad
\operatorname{proj}(o_1;i)=v}
{o_0 \vdash e.i; o_s \Longrightarrow v; o'_s}
\end{aligned} B-proj o 0 ⊢ e . i ; o s ⟹ v ; o s ′ o 0 ⊢ e ; o s ⟹ { o 1 } ; o s ′ proj ( o 1 ; i ) = v B-mproj o 0 ⊢ e ; o s ⟹ { o 1 } ; o s ′ mproj ( o 1 ; i j ) = o 2 o 0 ⊢ e . { i j } ; o s ⟹ { o 2 } ; o s ′ \begin{aligned}
&\text{B-mproj}\\
&\frac{o_0 \vdash e; o_s \Longrightarrow\{o_1\}; o'_s
\qquad
\operatorname{mproj}(o_1;i_j)=o_2}
{o_0 \vdash e.\{i_j\}; o_s \Longrightarrow\{o_2\}; o'_s}
\end{aligned} B-mproj o 0 ⊢ e . { i j } ; o s ⟹ { o 2 } ; o s ′ o 0 ⊢ e ; o s ⟹ { o 1 } ; o s ′ mproj ( o 1 ; i j ) = o 2 B-diff o 0 ⊢ e ; o s ⟹ { o 1 } ; o s ′ diff ( o 1 ; i j ) = o 2 o 0 ⊢ e \ { i j } ; o s ⟹ { o 2 } ; o s ′ \begin{aligned}
&\text{B-diff}\\
&\frac{o_0 \vdash e; o_s \Longrightarrow\{o_1\}; o'_s
\qquad
\operatorname{diff}(o_1;i_j)=o_2}
{o_0 \vdash e\backslash\{i_j\}; o_s \Longrightarrow\{o_2\}; o'_s}
\end{aligned} B-diff o 0 ⊢ e \ { i j } ; o s ⟹ { o 2 } ; o s ′ o 0 ⊢ e ; o s ⟹ { o 1 } ; o s ′ diff ( o 1 ; i j ) = o 2 B-let o 0 ⊢ e 0 ; o s 0 ⟹ v 0 ; o s 1 expand ( t ; v 0 ) = o 1 o 0 , o 1 ⊢ e 1 ; o s 1 ⟹ v 1 ; o s 2 o 0 ⊢ let t = e 0 in e 1 ; o s 0 ⟹ v 1 ; o s 2 \begin{aligned}
&\text{B-let}\\
&\frac{o_0 \vdash e_0; o_{s0} \Longrightarrow v_0; o_{s1}
\qquad
\operatorname{expand}(t;v_0)=o_1
\qquad
o_0,o_1 \vdash e_1; o_{s1} \Longrightarrow v_1; o_{s2}}
{o_0 \vdash\operatorname{let} t=e_0\ \operatorname{in} e_1; o_{s0} \Longrightarrow v_1; o_{s2}}
\end{aligned} B-let o 0 ⊢ let t = e 0 in e 1 ; o s 0 ⟹ v 1 ; o s 2 o 0 ⊢ e 0 ; o s 0 ⟹ v 0 ; o s 1 expand ( t ; v 0 ) = o 1 o 0 , o 1 ⊢ e 1 ; o s 1 ⟹ v 1 ; o s 2 B-loc o ⊢ l ; o s ⟹ l ; o s \begin{aligned}
&\text{B-loc}\\
&\frac{}{o \vdash l; o_s \Longrightarrow l; o_s}
\end{aligned} B-loc o ⊢ l ; o s ⟹ l ; o s B-ref o ⊢ e ; o s ⟹ v ; o s ′ l ∉ o s ′ o ⊢ ref e ; o s ⟹ l ; o s ′ , l : v \begin{aligned}
&\text{B-ref}\\
&\frac{o \vdash e; o_s \Longrightarrow v; o'_s
\qquad
l \notin o'_s}
{o \vdash\operatorname{ref}\ e; o_s \Longrightarrow l; o'_s,l:v}
\end{aligned} B-ref o ⊢ ref e ; o s ⟹ l ; o s ′ , l : v o ⊢ e ; o s ⟹ v ; o s ′ l ∈ / o s ′ B-deref o ⊢ e ; o s ⟹ l ; o s ′ proj ( o s ′ ; l ) = v o ⊢ ! e ; o s ⟹ v ; o s ′ \begin{aligned}
&\text{B-deref}\\
&\frac{o \vdash e; o_s \Longrightarrow l; o'_s
\qquad
\operatorname{proj}(o'_s;l)=v}
{o \vdash!e; o_s \Longrightarrow v; o'_s}
\end{aligned} B-deref o ⊢ ! e ; o s ⟹ v ; o s ′ o ⊢ e ; o s ⟹ l ; o s ′ proj ( o s ′ ; l ) = v B-set o ⊢ e 0 ; o s 0 ⟹ l ; o s 1 o ⊢ e 1 ; o s 1 ⟹ v ; o s 2 o ⊢ e 0 : = e 1 ; o s 0 ⟹ { } ; o s 2 + + l : v \begin{aligned}
&\text{B-set}\\
&\frac{o \vdash e_0; o_{s0} \Longrightarrow l; o_{s1}
\qquad
o \vdash e_1; o_{s1} \Longrightarrow v; o_{s2}}
{o \vdash e_0 := e_1; o_{s0} \Longrightarrow\{\}; o_{s2} \mathbin{+\!\!+} l:v}
\end{aligned} B-set o ⊢ e 0 := e 1 ; o s 0 ⟹ { } ; o s 2 + + l : v o ⊢ e 0 ; o s 0 ⟹ l ; o s 1 o ⊢ e 1 ; o s 1 ⟹ v ; o s 2 expand ( c ; o ) expand ( ε ; ε ) = ε expand ( c , i ⋄ t ; o 0 , i ▶ v , o 1 ) = expand ( c ; o 0 , o 1 ) , expand ( t ; v ) ( if i ∉ o 1 ) \begin{aligned}
&\operatorname{expand}(c;o)\\
&\operatorname{expand}(\varepsilon;\varepsilon)=\varepsilon\\
&\operatorname{expand}(c,i\mathbin{\diamond}t;o_0,i\mathbin{\blacktriangleright}v,o_1)
=\operatorname{expand}(c;o_0,o_1),\operatorname{expand}(t;v)
\qquad(\text{if }i\notin o_1)
\end{aligned} expand ( c ; o ) expand ( ε ; ε ) = ε expand ( c , i ⋄ t ; o 0 , i ▶ v , o 1 ) = expand ( c ; o 0 , o 1 ) , expand ( t ; v ) ( if i ∈ / o 1 ) expand ( t ; v ) expand ( i ; v ) = i : v expand ( { c } ; { o } ) = expand ( c ; o ) \begin{aligned}
&\operatorname{expand}(t;v)\\
&\operatorname{expand}(i;v)=i:v\\
&\operatorname{expand}(\{c\};\{o\})=\operatorname{expand}(c;o)
\end{aligned} expand ( t ; v ) expand ( i ; v ) = i : v expand ({ c } ; { o }) = expand ( c ; o ) proj ( o ; i ) proj ( o 0 , i ▶ v , o 1 ; i ) = v ( if i ∉ o 1 ) \begin{aligned}
&\operatorname{proj}(o;i)\\
&\operatorname{proj}(o_0,i\mathbin{\blacktriangleright}v,o_1;i)=v
\qquad(\text{if }i\notin o_1)
\end{aligned} proj ( o ; i ) proj ( o 0 , i ▶ v , o 1 ; i ) = v ( if i ∈ / o 1 ) mproj ( o ; i ) \operatorname{mproj}(o;i) mproj ( o ; i ) mproj ( o ; ε ) = ε \operatorname{mproj}(o;\varepsilon)=\varepsilon mproj ( o ; ε ) = ε mproj ( o 0 , i ⋆ v , o 1 ; i ‾ , i ) = mproj ( o 0 , o 1 ; i ‾ ) , i ⋆ v ( i ∉ o 1 ) \operatorname{mproj}(o_0,i\star v,o_1;\overline{i},i)=\operatorname{mproj}(o_0,o_1;\overline{i}),i\star v \qquad(i\notin o_1) mproj ( o 0 , i ⋆ v , o 1 ; i , i ) = mproj ( o 0 , o 1 ; i ) , i ⋆ v ( i ∈ / o 1 ) diff ( o ; i ‾ ) \operatorname{diff}(o;\overline{i}) diff ( o ; i ) diff ( o ; ε ) = o \operatorname{diff}(o;\varepsilon)=o diff ( o ; ε ) = o diff ( o 0 , i ⋆ v , o 1 ; i ‾ , i ) = diff ( o 0 , o 1 ; i ‾ ) ( i ∉ o 1 ) \operatorname{diff}(o_0,i\star v,o_1;\overline{i},i)=\operatorname{diff}(o_0,o_1;\overline{i}) \qquad(i\notin o_1) diff ( o 0 , i ⋆ v , o 1 ; i , i ) = diff ( o 0 , o 1 ; i ) ( i ∈ / o 1 ) ε + + o = o \varepsilon++ o=o ε + + o = o i = v , o 0 + + o 1 = i = v , ( o 0 + + o 1 ) i=v,\ o_0 ++ o_1=i=v,\ (o_0 ++ o_1) i = v , o 0 + + o 1 = i = v , ( o 0 + + o 1 ) i : v 0 , o 0 + + o 1 , i ⋆ v 1 , o 2 = i ⋆ v 1 , ( o 0 + + o 1 , o 2 ) ( i ∉ o 1 ) i:v_0,\ o_0 ++ o_1,i\star v_1,o_2=i\star v_1,\ (o_0 ++ o_1,o_2) \qquad(i\notin o_1) i : v 0 , o 0 + + o 1 , i ⋆ v 1 , o 2 = i ⋆ v 1 , ( o 0 + + o 1 , o 2 ) ( i ∈ / o 1 ) i : v , o 0 + + o 1 , i ? , o 2 = i : v , ( o 0 + + o 1 , o 2 ) ( i ∉ o 1 ) i:v,\ o_0 ++ o_1,i?,o_2=i:v,\ (o_0 ++ o_1,o_2) \qquad(i\notin o_1) i : v , o 0 + + o 1 , i ? , o 2 = i : v , ( o 0 + + o 1 , o 2 ) ( i ∈ / o 1 ) i : v , o 0 + + o 1 = i : v , ( o 0 + + o 1 ) ( i ∉ o 1 ) i:v,\ o_0 ++ o_1=i:v,\ (o_0 ++ o_1) \qquad(i\notin o_1) i : v , o 0 + + o 1 = i : v , ( o 0 + + o 1 ) ( i ∈ / o 1 ) i ? , o 0 + + o 1 , i ⋆ v , o 2 = i ⋆ v , ( o 0 + + o 1 , o 2 ) ( i ∉ o 1 ) i?,\ o_0 ++ o_1,i\star v,o_2=i\star v,\ (o_0 ++ o_1,o_2) \qquad(i\notin o_1) i ? , o 0 + + o 1 , i ⋆ v , o 2 = i ⋆ v , ( o 0 + + o 1 , o 2 ) ( i ∈ / o 1 ) i ? , o 0 + + o 1 , i ? , o 2 = i ? , ( o 0 + + o 1 , o 2 ) ( i ∉ o 1 ) i?,\ o_0 ++ o_1,i?,o_2=i?,\ (o_0 ++ o_1,o_2) \qquad(i\notin o_1) i ? , o 0 + + o 1 , i ? , o 2 = i ? , ( o 0 + + o 1 , o 2 ) ( i ∈ / o 1 ) i ? , o 0 + + o 1 = i ? , ( o 0 + + o 1 ) ( i ∉ o 1 ) i?,\ o_0 ++ o_1=i?,\ (o_0 ++ o_1) \qquad(i\notin o_1) i ? , o 0 + + o 1 = i ? , ( o 0 + + o 1 ) ( i ∈ / o 1 ) λ ⊢ ρ \lambda^\rho_{\vdash} λ ⊢ ρ The full collection of syntax-directed typing rules are as follows:
ρ s ; ρ ⊢ s e : : A \rho_s;\rho\vdash_s e::A ρ s ; ρ ⊢ s e :: A ρ s ; ρ ⊢ s e : ∀ a j ‾ . a k ρ s ; ρ ⊢ s e : : τ \begin{aligned}
\rho_s;\rho\vdash_s e:\forall\overline{a_j}.a_k\\
\rho_s;\rho\vdash_s e::\tau
\end{aligned} ρ s ; ρ ⊢ s e : ∀ a j . a k ρ s ; ρ ⊢ s e :: τ ρ s ; ρ ⊢ s e : A ∀ a k , A ≠ ∀ a j ‾ . a k ρ s ; ρ ⊢ s e : : A \begin{aligned}
\rho_s;\rho\vdash_s e:A \qquad\forall a_k,\ A\ne\forall\overline{a_j}.a_k\\
\rho_s;\rho\vdash_s e::A
\end{aligned} ρ s ; ρ ⊢ s e : A ∀ a k , A = ∀ a j . a k ρ s ; ρ ⊢ s e :: A ρ s ; ρ ⊢ s e : A \rho_s;\rho\vdash_s e:A ρ s ; ρ ⊢ s e : A ρ s ; ρ ⊢ s n : N \rho_s;\rho\vdash_s n:\mathbb{N} ρ s ; ρ ⊢ s n : N a j ‾ ∉ ftv ( ρ s ) a j ‾ ∉ ftv ( ρ 0 ) c : ρ 1 ⊙ ρ 2 ρ s ; ρ 0 , ρ 2 ⊢ s e : A ρ s ; ρ 0 ⊢ s λ { c } . e : ∀ a j ‾ . { ρ 1 } → A \frac{\overline{a_j}\notin\operatorname{ftv}(\rho_s)\qquad\overline{a_j}\notin\operatorname{ftv}(\rho_0)\qquad c:\rho_1\mathbin{\odot}\rho_2\qquad\rho_s;\rho_0,\rho_2\vdash_s e:A}{\rho_s;\rho_0\vdash_s\lambda\{c\}.e:\forall\overline{a_j}.\{\rho_1\}\to A} ρ s ; ρ 0 ⊢ s λ { c } . e : ∀ a j . { ρ 1 } → A a j ∈ / ftv ( ρ s ) a j ∈ / ftv ( ρ 0 ) c : ρ 1 ⊙ ρ 2 ρ s ; ρ 0 , ρ 2 ⊢ s e : A a j ‾ ∉ ftv ( ρ s ) ρ s ; ε ⊢ s { o 0 } : A ρ s ; ρ 0 ⊢ s ⟨ o 0 ; o 1 ∣ λ { c } . e ⟩ : ∀ a j ‾ . { ρ 5 } → C \frac{\overline{a_j}\notin\operatorname{ftv}(\rho_s)\qquad\rho_s;\varepsilon\vdash_s\{o_0\}:A}{\rho_s;\rho_0\vdash_s\langle o_0;o_1\mid\lambda\{c\}.e\rangle:\forall\overline{a_j}.\{\rho_5\}\to C} ρ s ; ρ 0 ⊢ s ⟨ o 0 ; o 1 ∣ λ { c } . e ⟩ : ∀ a j . { ρ 5 } → C a j ∈ / ftv ( ρ s ) ρ s ; ε ⊢ s { o 0 } : A A ≤ { ρ 1 } ⌊ ρ 1 ⌋ a j ‾ ∉ ftv ( ρ 1 ) ρ s ; ε ⊢ s { o 1 } : B B ≤ ∀ a j ‾ . { ρ 2 } c : ρ 3 ⊙ ρ 4 ρ 3 ∙ ρ 2 ⇝ ρ 5 ρ s ; ρ 1 , ρ 4 ⊢ s e : C \begin{gathered}
A\le\{\rho_1\}\qquad\lfloor\rho_1\rfloor\qquad\overline{a_j}\notin\operatorname{ftv}(\rho_1)\\
\rho_s;\varepsilon\vdash_s\{o_1\}:B\qquad B\le\forall\overline{a_j}.\{\rho_2\}\\
c:\rho_3\mathbin{\odot}\rho_4\qquad\rho_3\mathbin{\bullet}\rho_2\rightsquigarrow\rho_5\qquad\rho_s;\rho_1,\rho_4\vdash_s e:C
\end{gathered} A ≤ { ρ 1 } ⌊ ρ 1 ⌋ a j ∈ / ftv ( ρ 1 ) ρ s ; ε ⊢ s { o 1 } : B B ≤ ∀ a j . { ρ 2 } c : ρ 3 ⊙ ρ 4 ρ 3 ∙ ρ 2 ⇝ ρ 5 ρ s ; ρ 1 , ρ 4 ⊢ s e : C a 2 l ‾ ∉ ftv ( ρ 1 ) a 2 l ‾ ∉ ftv ( A ) a 2 l ‾ ∉ ftv ( ρ 2 ) ρ s ; ρ 0 ⊢ s e 0 : ∀ a 0 j ‾ . { ρ 1 } → A ρ s ; ρ 0 ⊢ s e 1 : ∀ a 1 k ‾ . { ρ 2 } ρ 1 [ τ 0 j / a 0 j ] ∙ s ρ 2 [ τ 1 j / a 1 k ] ⇝ ρ 3 ρ s ; ρ 0 ⊢ s e 0 e 1 : ∀ a 2 l ‾ . { ρ 3 } → A [ τ 0 j / a 0 j ] \frac{
\begin{gathered}
\overline{a_{2l}}\notin\operatorname{ftv}(\rho_1)\qquad
\overline{a_{2l}}\notin\operatorname{ftv}(A)\qquad
\overline{a_{2l}}\notin\operatorname{ftv}(\rho_2)\\
\rho_s;\rho_0\vdash_s e_0:\forall\overline{a_{0j}}.\{\rho_1\}\to A\\
\rho_s;\rho_0\vdash_s e_1:\forall\overline{a_{1k}}.\{\rho_2\}\\
\rho_1[\tau_{0j}/a_{0j}]\mathbin{\bullet_s}\rho_2[\tau_{1j}/a_{1k}]\rightsquigarrow\rho_3
\end{gathered}
}{\rho_s;\rho_0\vdash_s e_0e_1:\forall\overline{a_{2l}}.\{\rho_3\}\to A[\tau_{0j}/a_{0j}]} ρ s ; ρ 0 ⊢ s e 0 e 1 : ∀ a 2 l . { ρ 3 } → A [ τ 0 j / a 0 j ] a 2 l ∈ / ftv ( ρ 1 ) a 2 l ∈ / ftv ( A ) a 2 l ∈ / ftv ( ρ 2 ) ρ s ; ρ 0 ⊢ s e 0 : ∀ a 0 j . { ρ 1 } → A ρ s ; ρ 0 ⊢ s e 1 : ∀ a 1 k . { ρ 2 } ρ 1 [ τ 0 j / a 0 j ] ∙ s ρ 2 [ τ 1 j / a 1 k ] ⇝ ρ 3 a 2 l ‾ ∉ ftv ( ρ 2 ) ρ s ; ρ 0 ⊢ s e 0 : ∀ a 0 j ‾ . a m ρ s ; ρ 0 ⊢ s e 1 : ∀ a 1 k ‾ . { ρ 2 } ϱ ∙ ρ 2 [ τ 1 j / a 1 k ] ⇝ ρ 3 ρ s ; ρ 0 ⊢ s e 0 e 1 : ∀ a 2 l ‾ . { ρ 3 } → τ 0 \frac{
\begin{gathered}
\overline{a_{2l}}\notin\operatorname{ftv}(\rho_2)\\
\rho_s;\rho_0\vdash_s e_0:\forall\overline{a_{0j}}.a_m\\
\rho_s;\rho_0\vdash_s e_1:\forall\overline{a_{1k}}.\{\rho_2\}\\
\varrho\mathbin{\bullet}\rho_2[\tau_{1j}/a_{1k}]\rightsquigarrow\rho_3
\end{gathered}
}{\rho_s;\rho_0\vdash_s e_0e_1:\forall\overline{a_{2l}}.\{\rho_3\}\to\tau_0} ρ s ; ρ 0 ⊢ s e 0 e 1 : ∀ a 2 l . { ρ 3 } → τ 0 a 2 l ∈ / ftv ( ρ 2 ) ρ s ; ρ 0 ⊢ s e 0 : ∀ a 0 j . a m ρ s ; ρ 0 ⊢ s e 1 : ∀ a 1 k . { ρ 2 } ϱ ∙ ρ 2 [ τ 1 j / a 1 k ] ⇝ ρ 3 a 2 l ‾ ∉ ftv ( ρ 1 ) a 2 l ‾ ∉ ftv ( A ) ρ s ; ρ 0 ⊢ s e 0 : ∀ a 0 j ‾ . { ρ 1 } → A ρ s ; ρ 0 ⊢ s e 1 : ∀ a 1 k ‾ . a m ρ 1 [ τ j / a 0 j ] ∙ s ϱ ⇝ ρ 3 ρ s ; ρ 0 ⊢ s e 0 e 1 : ∀ a 2 l ‾ . { ρ 3 } → A [ τ j / a 0 j ] \frac{
\begin{gathered}
\overline{a_{2l}}\notin\operatorname{ftv}(\rho_1)\qquad
\overline{a_{2l}}\notin\operatorname{ftv}(A)\\
\rho_s;\rho_0\vdash_s e_0:\forall\overline{a_{0j}}.\{\rho_1\}\to A\\
\rho_s;\rho_0\vdash_s e_1:\forall\overline{a_{1k}}.a_m\\
\rho_1[\tau_j/a_{0j}]\mathbin{\bullet_s}\varrho\rightsquigarrow\rho_3
\end{gathered}
}{\rho_s;\rho_0\vdash_s e_0e_1:\forall\overline{a_{2l}}.\{\rho_3\}\to A[\tau_j/a_{0j}]} ρ s ; ρ 0 ⊢ s e 0 e 1 : ∀ a 2 l . { ρ 3 } → A [ τ j / a 0 j ] a 2 l ∈ / ftv ( ρ 1 ) a 2 l ∈ / ftv ( A ) ρ s ; ρ 0 ⊢ s e 0 : ∀ a 0 j . { ρ 1 } → A ρ s ; ρ 0 ⊢ s e 1 : ∀ a 1 k . a m ρ 1 [ τ j / a 0 j ] ∙ s ϱ ⇝ ρ 3 ρ s ; ρ 0 ⊢ s e 0 : ∀ a 0 ‾ j . a m 0 ρ s ; ρ 0 ⊢ s e 1 : ∀ a 1 ‾ k . a m 1 ρ 1 ∙ s ρ 2 ↠ ρ 3 ρ s ; ρ 0 ⊢ s e 0 e 1 : ∀ a 2 ‾ l . { ρ 3 } → τ ST-AppAny \begin{aligned}
&\rho_s;\rho_0 \vdash_s e_0 : \forall\overline{a_0}_j.a_{m_0}\\
&\rho_s;\rho_0 \vdash_s e_1 : \forall\overline{a_1}_k.a_{m_1}
\qquad
\rho_1 \mathbin{\bullet_s} \rho_2 \twoheadrightarrow\rho_3\\
&\frac{\rho_s;\rho_0 \vdash_s e_0\,e_1 : \forall\overline{a_2}_l.\{\rho_3\}\to\tau}{\text{ST-AppAny}}
\end{aligned} ρ s ; ρ 0 ⊢ s e 0 : ∀ a 0 j . a m 0 ρ s ; ρ 0 ⊢ s e 1 : ∀ a 1 k . a m 1 ρ 1 ∙ s ρ 2 ↠ ρ 3 ST-AppAny ρ s ; ρ 0 ⊢ s e 0 e 1 : ∀ a 2 l . { ρ 3 } → τ ρ s ; ρ 0 ⊢ s e 0 : : ∀ a 1 ‾ j . { ρ 1 } ρ s ; ρ 1 [ τ j a j ] ⊢ s e 1 : A ST-Box \frac{\rho_s;\rho_0 \vdash_s e_0 :: \forall\overline{a_1}_j.\{\rho_1\}}
{\rho_s;\rho_1\left[\frac{\tau_j}{a_j}\right]\vdash_s e_1:A}
\qquad
\text{ST-Box} ρ s ; ρ 1 [ a j τ j ] ⊢ s e 1 : A ρ s ; ρ 0 ⊢ s e 0 :: ∀ a 1 j . { ρ 1 } ST-Box ρ s ; ρ 0 ⊢ s e 0 ▶ e 1 : A \rho_s;\rho_0 \vdash_s e_0 \mathbin{\blacktriangleright} e_1:A ρ s ; ρ 0 ⊢ s e 0 ▶ e 1 : A ρ s ; ρ 0 ⊢ s e : : ∀ a ‾ j . { ρ 1 } → A ⌊ ρ 1 ⌋ [ τ j a j ] ρ s ; ρ 0 ⊢ s force e : A ST-Force \frac{\rho_s;\rho_0 \vdash_s e::\forall\overline{a}_j.\{\rho_1\}\to A
\qquad\lfloor\rho_1\rfloor\left[\frac{\tau_j}{a_j}\right]}
{\rho_s;\rho_0\vdash_s \operatorname{force}\ e:A}
\qquad
\text{ST-Force} ρ s ; ρ 0 ⊢ s force e : A ρ s ; ρ 0 ⊢ s e :: ∀ a j . { ρ 1 } → A ⌊ ρ 1 ⌋ [ a j τ j ] ST-Force ρ s ; ρ ⊢ s @ : { ρ } ST-Env \frac{\rho_s;\rho\vdash_s @:\{\rho\}}{\text{ST-Env}} ST-Env ρ s ; ρ ⊢ s @ : { ρ } ρ s ; ρ 0 ⊢ s r : ρ 1 ρ s ; ρ 0 ⊢ s { r } : { ρ 1 } ST-Record \frac{\rho_s;\rho_0\vdash_s r:\rho_1}{\rho_s;\rho_0\vdash_s\{r\}:\{\rho_1\}}
\qquad
\text{ST-Record} ρ s ; ρ 0 ⊢ s { r } : { ρ 1 } ρ s ; ρ 0 ⊢ s r : ρ 1 ST-Record ρ s ; ρ 0 ⊢ s e 0 : : ∀ a 1 ‾ j . { ρ 1 } ρ s ; ρ 0 ⊢ s e 1 : : ∀ a 2 ‾ k . { ρ 2 } ρ 1 [ τ 1 j a 1 j ] ⊕ s ρ 2 [ τ 2 j a 2 k ] ⇝ ρ 3 ρ s ; ρ 0 ⊢ s e 0 + + e 1 : { ρ 3 } ST-Concat \frac{\rho_s;\rho_0\vdash_s e_0::\forall\overline{a_1}_j.\{\rho_1\}
\qquad
\rho_s;\rho_0\vdash_s e_1::\forall\overline{a_2}_k.\{\rho_2\}
\qquad
\rho_1\left[\frac{\tau_{1j}}{a_{1j}}\right]\oplus_s\rho_2\left[\frac{\tau_{2j}}{a_{2k}}\right]\rightsquigarrow\rho_3}
{\rho_s;\rho_0\vdash_s e_0++e_1:\{\rho_3\}}
\qquad
\text{ST-Concat} ρ s ; ρ 0 ⊢ s e 0 + + e 1 : { ρ 3 } ρ s ; ρ 0 ⊢ s e 0 :: ∀ a 1 j . { ρ 1 } ρ s ; ρ 0 ⊢ s e 1 :: ∀ a 2 k . { ρ 2 } ρ 1 [ a 1 j τ 1 j ] ⊕ s ρ 2 [ a 2 k τ 2 j ] ⇝ ρ 3 ST-Concat ρ s ; ρ 0 ⊢ s e : : ∀ a ‾ j . { ρ 1 , i ⋆ A , ρ 2 } i ∉ ρ 2 ρ s ; ρ 0 ⊢ s e . i : A [ τ j a j ] ST-Proj \frac{\rho_s;\rho_0\vdash_s e::\forall\overline{a}_j.\{\rho_1,i\mathbin{\star}A,\rho_2\}
\qquad i\notin\rho_2}
{\rho_s;\rho_0\vdash_s e.i:A\left[\frac{\tau_j}{a_j}\right]}
\qquad
\text{ST-Proj} ρ s ; ρ 0 ⊢ s e . i : A [ a j τ j ] ρ s ; ρ 0 ⊢ s e :: ∀ a j . { ρ 1 , i ⋆ A , ρ 2 } i ∈ / ρ 2 ST-Proj ρ s ; ρ 0 ⊢ s e : : ∀ a ‾ j . { ρ 1 , i 0 k ⋆ 0 k A k ‾ k ∈ [ : n ] , ρ 2 k ‾ k ∈ [ : n ] } i 0 k ∉ ρ 2 l ‾ l ∈ [ : k + 1 ] , k ∈ [ : n ] i 0 k ⋆ 0 k A k ‾ k ∈ [ : n ] permutes i 1 k ⋆ 1 k B k ‾ k ∈ [ : n ] ρ s ; ρ 0 ⊢ s e . { i 1 k ‾ k ∈ [ : n ] } : { i 1 k ⋆ 1 k B k ‾ k ∈ [ : n ] } [ τ j a j ] ST-MProj \frac{
\rho_s;\rho_0\vdash_s e::\forall\overline{a}_j.\left\{\rho_1,\overline{i_{0k}\mathbin{\star_{0k}}A_k}_{k\in[:n]},\overline{\rho_{2k}}_{k\in[:n]}\right\}
\qquad
\overline{i_{0k}\notin\rho_{2l}}_{l\in[:k+1],\,k\in[:n]}
\qquad
\overline{i_{0k}\mathbin{\star_{0k}}A_k}_{k\in[:n]}
\qquad
\text{permutes }\overline{i_{1k}\mathbin{\star_{1k}}B_k}_{k\in[:n]}
}{
\rho_s;\rho_0\vdash_s e.\{\overline{i_{1k}}_{k\in[:n]}\}:
\{\overline{i_{1k}\mathbin{\star_{1k}}B_k}_{k\in[:n]}\}
\left[\frac{\tau_j}{a_j}\right]
}
\qquad
\text{ST-MProj} ρ s ; ρ 0 ⊢ s e . { i 1 k k ∈ [ : n ] } : { i 1 k ⋆ 1 k B k k ∈ [ : n ] } [ a j τ j ] ρ s ; ρ 0 ⊢ s e :: ∀ a j . { ρ 1 , i 0 k ⋆ 0 k A k k ∈ [ : n ] , ρ 2 k k ∈ [ : n ] } i 0 k ∈ / ρ 2 l l ∈ [ : k + 1 ] , k ∈ [ : n ] i 0 k ⋆ 0 k A k k ∈ [ : n ] permutes i 1 k ⋆ 1 k B k k ∈ [ : n ] ST-MProj ρ s ; ρ 0 ⊢ s e : : ∀ a ‾ j . { ρ 1 , i 0 k ⋆ 0 k A k ‾ k ∈ [ : n ] , ρ 2 k ‾ k ∈ [ : n ] } i 0 k ∉ ρ 2 l ‾ l ∈ [ : k + 1 ] , k ∈ [ : n ] i 0 k ⋆ 0 k A k ‾ k ∈ [ : n ] permutes i 1 k ⋆ 1 k B k ‾ k ∈ [ : n ] ρ s ; ρ 0 ⊢ s e { i 1 k ‾ k ∈ [ : n ] } : { ρ 1 [ τ j a j ] , ρ 2 k [ τ j a j ] ‾ k ∈ [ : n ] } ST-Diff \frac{
\rho_s;\rho_0\vdash_s e::\forall\overline{a}_j.\left\{\rho_1,\overline{i_{0k}\mathbin{\star_{0k}}A_k}_{k\in[:n]},\overline{\rho_{2k}}_{k\in[:n]}\right\}
\qquad
\overline{i_{0k}\notin\rho_{2l}}_{l\in[:k+1],\,k\in[:n]}
\qquad
\overline{i_{0k}\mathbin{\star_{0k}}A_k}_{k\in[:n]}
\qquad
\text{permutes }\overline{i_{1k}\mathbin{\star_{1k}}B_k}_{k\in[:n]}
}{
\rho_s;\rho_0\vdash_s e\{\overline{i_{1k}}_{k\in[:n]}\}:
\left\{\rho_1\left[\frac{\tau_j}{a_j}\right],
\overline{\rho_{2k}\left[\frac{\tau_j}{a_j}\right]}_{k\in[:n]}\right\}
}
\qquad
\text{ST-Diff} ρ s ; ρ 0 ⊢ s e { i 1 k k ∈ [ : n ] } : { ρ 1 [ a j τ j ] , ρ 2 k [ a j τ j ] k ∈ [ : n ] } ρ s ; ρ 0 ⊢ s e :: ∀ a j . { ρ 1 , i 0 k ⋆ 0 k A k k ∈ [ : n ] , ρ 2 k k ∈ [ : n ] } i 0 k ∈ / ρ 2 l l ∈ [ : k + 1 ] , k ∈ [ : n ] i 0 k ⋆ 0 k A k k ∈ [ : n ] permutes i 1 k ⋆ 1 k B k k ∈ [ : n ] ST-Diff ρ s ; ρ 0 ⊢ s e 0 : A t : s A ⊙ ρ 1 ρ s ; ρ 0 , ρ 1 ⊢ s e 1 : B ρ s ; ρ 0 ⊢ s let t = e 0 in e 1 : B ST-Let \frac{\rho_s;\rho_0\vdash_s e_0:A
\qquad
t:_s A\mathbin{\odot}\rho_1
\qquad
\rho_s;\rho_0,\rho_1\vdash_s e_1:B}
{\rho_s;\rho_0\vdash_s\operatorname{let}\ t=e_0\ \operatorname{in}\ e_1:B}
\qquad
\text{ST-Let} ρ s ; ρ 0 ⊢ s let t = e 0 in e 1 : B ρ s ; ρ 0 ⊢ s e 0 : A t : s A ⊙ ρ 1 ρ s ; ρ 0 , ρ 1 ⊢ s e 1 : B ST-Let ρ s 0 , l : A , ρ s 1 ; ρ ⊢ s l : Ref A ST-Loc \frac{\rho_{s0},l:A,\rho_{s1};\rho\vdash_s l:\operatorname{Ref} A}{\text{ST-Loc}} ST-Loc ρ s 0 , l : A , ρ s 1 ; ρ ⊢ s l : Ref A ρ s ; ρ ⊢ s e : A A ≤ B ρ s ; ρ ⊢ s ref e : Ref B ST-Ref \frac{\rho_s;\rho\vdash_s e:A\qquad A\leq B}
{\rho_s;\rho\vdash_s\operatorname{ref}\ e:\operatorname{Ref} B}
\qquad
\text{ST-Ref} ρ s ; ρ ⊢ s ref e : Ref B ρ s ; ρ ⊢ s e : A A ≤ B ST-Ref ρ s ; ρ ⊢ s e : : ∀ a ‾ j . Ref A ρ s ; ρ ⊢ s ! e : A [ τ j a j ] ST-Deref \frac{\rho_s;\rho\vdash_s e::\forall\overline{a}_j.\operatorname{Ref} A}
{\rho_s;\rho\vdash_s!e:A\left[\frac{\tau_j}{a_j}\right]}
\qquad
\text{ST-Deref} ρ s ; ρ ⊢ s ! e : A [ a j τ j ] ρ s ; ρ ⊢ s e :: ∀ a j . Ref A ST-Deref ρ s ; ρ ⊢ s e 0 : : ∀ a ‾ j . Ref A ρ s ; ρ ⊢ s e 1 : B B ≤ A ρ s ; ρ ⊢ s e 0 ≔ e 1 : { } ST-Set \frac{\rho_s;\rho\vdash_s e_0::\forall\overline{a}_j.\operatorname{Ref} A
\qquad
\rho_s;\rho\vdash_s e_1:B
\qquad B\leq A}
{\rho_s;\rho\vdash_s e_0\mathrel{\coloneqq}e_1:\{\}}
\qquad
\text{ST-Set} ρ s ; ρ ⊢ s e 0 : = e 1 : { } ρ s ; ρ ⊢ s e 0 :: ∀ a j . Ref A ρ s ; ρ ⊢ s e 1 : B B ≤ A ST-Set Record Syntax-Directed Typing
ρ s ; ρ 0 ⊢ s r : ρ 1 \boxed{\rho_s;\rho_0\vdash_s r:\rho_1} ρ s ; ρ 0 ⊢ s r : ρ 1 ρ s ; ρ ⊢ s ε : ε ST-Empty \frac{}{\rho_s;\rho\vdash_s\varepsilon:\varepsilon}
\qquad
\text{ST-Empty} ρ s ; ρ ⊢ s ε : ε ST-Empty ρ s ; ρ 0 ⊢ s r : ρ 1 ρ s ; ρ 0 ⊢ s e : A ρ s ; ρ 0 ⊢ s r , i ⋆ e : ρ 1 , i ⋆ A ST-Ext \frac{\rho_s;\rho_0\vdash_s r:\rho_1
\qquad
\rho_s;\rho_0\vdash_s e:A}
{\rho_s;\rho_0\vdash_s r,i\mathbin{\star}e:\rho_1,i\mathbin{\star}A}
\qquad
\text{ST-Ext} ρ s ; ρ 0 ⊢ s r , i ⋆ e : ρ 1 , i ⋆ A ρ s ; ρ 0 ⊢ s r : ρ 1 ρ s ; ρ 0 ⊢ s e : A ST-Ext ρ s ; ρ 0 ⊢ s r : ρ 1 ρ s ; ρ 0 ⊢ s r , i ? : ρ 1 , i ? A ST-Ext? \frac{\rho_s;\rho_0\vdash_s r:\rho_1}
{\rho_s;\rho_0\vdash_s r,i\mathbin{?}:\rho_1,i\mathbin{?}A}
\qquad
\text{ST-Ext?} ρ s ; ρ 0 ⊢ s r , i ? : ρ 1 , i ? A ρ s ; ρ 0 ⊢ s r : ρ 1 ST-Ext? Note that application is covered by four rules, ST-App, ST-AppAnyL, ST-AppAnyR, and ST-AppAny. This does not compromise syntax-directedness: the rules differ only in whether the type inferred for the function and for the argument is an “any” type (∀ a ‾ j . a k \forall\overline{a}_j.a_k ∀ a j . a k
C : s ρ 0 ⊙ ρ 1 \mathsf{C} :_{\mathsf{s}} \rho_0 \mathbin{\odot} \rho_1 C : s ρ 0 ⊙ ρ 1
SP-EMPTY
ε : s ε ⊙ ε \frac{\varepsilon:_{\mathsf{s}} \varepsilon\mathbin{\odot} \varepsilon}{} ε : s ε ⊙ ε SP-EXT
t : s A ⊙ ρ 1 c : s ρ 00 , ρ 01 ⊙ ρ 2 i ∉ ρ 00 ( i ⋄ t , c ) : s ( ρ 00 , i : A , ρ 01 ) ⊙ ρ 1 , ρ 2 \frac{t :_{\mathsf{s}} A \mathbin{\odot} \rho_1 \qquad c :_{\mathsf{s}} \rho_{00},\rho_{01} \mathbin{\odot} \rho_2 \qquad i \notin\rho_{00}}{(i \mathbin{\diamond} t,c) :_{\mathsf{s}} (\rho_{00},i:A,\rho_{01}) \mathbin{\odot} \rho_1,\rho_2} ( i ⋄ t , c ) : s ( ρ 00 , i : A , ρ 01 ) ⊙ ρ 1 , ρ 2 t : s A ⊙ ρ 1 c : s ρ 00 , ρ 01 ⊙ ρ 2 i ∈ / ρ 00 (Syntax-Directed Record Pattern Separation)
t : s A ⊙ ρ t :_{\mathsf{s}} A \mathbin{\odot} \rho t : s A ⊙ ρ
SP-LABEL
i : s A ⊙ ( i : A ) \frac{i :_{\mathsf{s}} A \mathbin{\odot} (i:A)}{} i : s A ⊙ ( i : A ) SP-RECORD
c : s ρ 0 [ τ j a j ] ⊙ ρ 1 { c } : s ∀ a j ‾ . { ρ 0 } ⊙ ρ 1 \frac{c :_{\mathsf{s}} \rho_0 \left[\frac{\tau_j}{a_j}\right] \mathbin{\odot} \rho_1}{\{c\} :_{\mathsf{s}} \forall\overline{a_j}.\{\rho_0\} \mathbin{\odot} \rho_1} { c } : s ∀ a j . { ρ 0 } ⊙ ρ 1 c : s ρ 0 [ a j τ j ] ⊙ ρ 1 SP-RECORDANY
c : s ϱ ⊙ ρ { c } : s ∀ a j ‾ . a k ⊙ ρ \frac{c :_{\mathsf{s}} \varrho\mathbin{\odot} \rho}{\{c\} :_{\mathsf{s}} \forall\overline{a_j}.a_k \mathbin{\odot} \rho} { c } : s ∀ a j . a k ⊙ ρ c : s ϱ ⊙ ρ (Syntax-Directed Pattern Separation)
ρ 0 ∙ s ρ 1 ⇝ ρ 2 \rho_0 \mathbin{\bullet_{\mathsf{s}}} \rho_1 \mathrel{\rightsquigarrow} \rho_2 ρ 0 ∙ s ρ 1 ⇝ ρ 2
SA-EMPTY
ε ∙ s ε ⇝ ε \frac{\varepsilon\mathbin{\bullet_{\mathsf{s}}} \varepsilon\mathrel{\rightsquigarrow} \varepsilon}{} ε ∙ s ε ⇝ ε SA-WEAKSTRONG
ρ 0 ∙ s ρ 10 , ρ 11 ⇝ ρ 2 i ∉ ρ 10 B ≤ A i : A , ρ 0 ∙ s ρ 10 , i ▶ B , ρ 11 ⇝ ρ 2 \frac{\rho_0 \mathbin{\bullet_{\mathsf{s}}} \rho_{10},\rho_{11} \mathrel{\rightsquigarrow} \rho_2 \qquad i \notin\rho_{10} \qquad B \leq A}{i:A,\rho_0 \mathbin{\bullet_{\mathsf{s}}} \rho_{10},i \mathbin{\blacktriangleright} B,\rho_{11} \mathrel{\rightsquigarrow} \rho_2} i : A , ρ 0 ∙ s ρ 10 , i ▶ B , ρ 11 ⇝ ρ 2 ρ 0 ∙ s ρ 10 , ρ 11 ⇝ ρ 2 i ∈ / ρ 10 B ≤ A SA-OPTIONALSTRONG
ρ 0 ∙ s ρ 10 , ρ 11 ⇝ ρ 2 i ∉ ρ 10 B ≤ A i ? A , ρ 0 ∙ s ρ 10 , i ▶ B , ρ 11 ⇝ ρ 2 \frac{\rho_0 \mathbin{\bullet_{\mathsf{s}}} \rho_{10},\rho_{11} \mathrel{\rightsquigarrow} \rho_2 \qquad i \notin\rho_{10} \qquad B \leq A}{i\,?A,\rho_0 \mathbin{\bullet_{\mathsf{s}}} \rho_{10},i \mathbin{\blacktriangleright} B,\rho_{11} \mathrel{\rightsquigarrow} \rho_2} i ? A , ρ 0 ∙ s ρ 10 , i ▶ B , ρ 11 ⇝ ρ 2 ρ 0 ∙ s ρ 10 , ρ 11 ⇝ ρ 2 i ∈ / ρ 10 B ≤ A SA-EXT
ρ 0 ∙ s ρ 10 , ρ 11 ⇝ ρ 2 i ∉ ρ 10 ⋆ 0 ∙ s ⋆ 1 ⇝ ⋆ 2 B ≤ A i ⋆ 0 A , ρ 0 ∙ s ρ 10 , i ⋆ 1 B , ρ 11 ⇝ i ⋆ 2 A , ρ 2 \frac{\rho_0 \mathbin{\bullet_{\mathsf{s}}} \rho_{10},\rho_{11} \mathrel{\rightsquigarrow} \rho_2 \qquad i \notin\rho_{10} \qquad\star_0 \mathbin{\bullet_{\mathsf{s}}} \star_1 \mathrel{\rightsquigarrow} \star_2 \qquad B \leq A}{i\,\star_0 A,\rho_0 \mathbin{\bullet_{\mathsf{s}}} \rho_{10},i\,\star_1 B,\rho_{11} \mathrel{\rightsquigarrow} i\,\star_2 A,\rho_2} i ⋆ 0 A , ρ 0 ∙ s ρ 10 , i ⋆ 1 B , ρ 11 ⇝ i ⋆ 2 A , ρ 2 ρ 0 ∙ s ρ 10 , ρ 11 ⇝ ρ 2 i ∈ / ρ 10 ⋆ 0 ∙ s ⋆ 1 ⇝ ⋆ 2 B ≤ A SA-WEAKEXT?
ρ 0 ∙ s ρ 1 ⇝ ρ 2 i ∉ ρ 1 i : A , ρ 0 ∙ s ρ 1 ⇝ i : A , ρ 2 \frac{\rho_0 \mathbin{\bullet_{\mathsf{s}}} \rho_1 \mathrel{\rightsquigarrow} \rho_2 \qquad i \notin\rho_1}{i:A,\rho_0 \mathbin{\bullet_{\mathsf{s}}} \rho_1 \mathrel{\rightsquigarrow} i:A,\rho_2} i : A , ρ 0 ∙ s ρ 1 ⇝ i : A , ρ 2 ρ 0 ∙ s ρ 1 ⇝ ρ 2 i ∈ / ρ 1 SA-OPTIONALEXT?
ρ 0 ∙ s ρ 1 ⇝ ρ 2 i ∉ ρ 1 i ? A , ρ 0 ∙ s ρ 1 ⇝ i ? A , ρ 2 \frac{\rho_0 \mathbin{\bullet_{\mathsf{s}}} \rho_1 \mathrel{\rightsquigarrow} \rho_2 \qquad i \notin\rho_1}{i\,?A,\rho_0 \mathbin{\bullet_{\mathsf{s}}} \rho_1 \mathrel{\rightsquigarrow} i\,?A,\rho_2} i ? A , ρ 0 ∙ s ρ 1 ⇝ i ? A , ρ 2 ρ 0 ∙ s ρ 1 ⇝ ρ 2 i ∈ / ρ 1 (Syntax-Directed Record Type App)
⋆ 0 ∙ s ⋆ 1 ⇝ ⋆ 2 \star_0 \mathbin{\bullet_{\mathsf{s}}} \star_1 \mathrel{\rightsquigarrow} \star_2 ⋆ 0 ∙ s ⋆ 1 ⇝ ⋆ 2
SA-LATER
: ∙ s ? ⇝ : :\mathbin{\bullet_{\mathsf{s}}}? \mathrel{\rightsquigarrow}: : ∙ s ? ⇝ : SA-IGNORE
: ∙ s : ⇝ : :\mathbin{\bullet_{\mathsf{s}}}: \mathrel{\rightsquigarrow}: : ∙ s : ⇝ : SA-SET
: ∙ s : ⇝ ? :\mathbin{\bullet_{\mathsf{s}}}: \mathrel{\rightsquigarrow}? : ∙ s : ⇝ ? SA-REPLACE
? ∙ s : ⇝ ? ?\mathbin{\bullet_{\mathsf{s}}}: \mathrel{\rightsquigarrow}? ? ∙ s : ⇝ ? SA-LEAVE
? ∙ s ? ⇝ ? ?\mathbin{\bullet_{\mathsf{s}}}? \mathrel{\rightsquigarrow}? ? ∙ s ? ⇝ ? (Syntax-Directed Strength App)
ρ 0 ⊕ s ρ 1 ↪ ρ 2 \rho_0 \mathbin{\oplus_{\mathsf{s}}} \rho_1 \mathrel{\hookrightarrow} \rho_2 ρ 0 ⊕ s ρ 1 ↪ ρ 2
SC-EMPTY
ε ⊕ s ε ↪ ε \frac{\varepsilon\mathbin{\oplus_{\mathsf{s}}} \varepsilon\mathrel{\hookrightarrow} \varepsilon}{} ε ⊕ s ε ↪ ε SC-STRONGL
ρ 0 ⊕ s ρ 1 ↪ ρ 2 i ▶ A , ρ 0 ⊕ s ρ 1 ↪ i ▶ A , ρ 2 \frac{\rho_0 \mathbin{\oplus_{\mathsf{s}}} \rho_1 \mathrel{\hookrightarrow} \rho_2}{i\mathbin{\blacktriangleright} A,\rho_0 \mathbin{\oplus_{\mathsf{s}}} \rho_1 \mathrel{\hookrightarrow} i\mathbin{\blacktriangleright} A,\rho_2} i ▶ A , ρ 0 ⊕ s ρ 1 ↪ i ▶ A , ρ 2 ρ 0 ⊕ s ρ 1 ↪ ρ 2 SC-EXT
ρ 0 ⊕ s ρ 10 , ρ 11 ↪ ρ 2 i ∉ ρ 10 ⋆ 0 ⊕ s ⋆ 1 ↪ ⋆ 2 A ≤ C B ≤ C i ⋆ 0 A , ρ 0 ⊕ s ρ 10 , i ⋆ 1 B , ρ 11 ↪ i ⋆ 2 C , ρ 2 \frac{\rho_0 \mathbin{\oplus_{\mathsf{s}}} \rho_{10},\rho_{11} \mathrel{\hookrightarrow} \rho_2 \qquad i \notin\rho_{10} \qquad\star_0 \mathbin{\oplus_{\mathsf{s}}} \star_1 \mathrel{\hookrightarrow} \star_2 \qquad A \leq C \qquad B \leq C}{i\,\star_0 A,\rho_0 \mathbin{\oplus_{\mathsf{s}}} \rho_{10},i\,\star_1 B,\rho_{11} \mathrel{\hookrightarrow} i\,\star_2 C,\rho_2} i ⋆ 0 A , ρ 0 ⊕ s ρ 10 , i ⋆ 1 B , ρ 11 ↪ i ⋆ 2 C , ρ 2 ρ 0 ⊕ s ρ 10 , ρ 11 ↪ ρ 2 i ∈ / ρ 10 ⋆ 0 ⊕ s ⋆ 1 ↪ ⋆ 2 A ≤ C B ≤ C SC-WEAKE XT?
ρ 0 ⊕ s ρ 1 ↪ ρ 2 i ∉ ρ 1 i : A , ρ 0 ⊕ s ρ 1 ↪ i : A , ρ 2 \frac{\rho_0 \mathbin{\oplus_{\mathsf{s}}} \rho_1 \mathrel{\hookrightarrow} \rho_2 \qquad i \notin\rho_1}{i:A,\rho_0 \mathbin{\oplus_{\mathsf{s}}} \rho_1 \mathrel{\hookrightarrow} i:A,\rho_2} i : A , ρ 0 ⊕ s ρ 1 ↪ i : A , ρ 2 ρ 0 ⊕ s ρ 1 ↪ ρ 2 i ∈ / ρ 1 SC-OPTIONALEXTL?
ρ 0 ⊕ s ρ 1 ↪ ρ 2 i ∉ ρ 1 A ≤ ? i ? A , ρ 0 ⊕ s ρ 1 ↪ i ? A , ρ 2 \frac{\rho_0 \mathbin{\oplus_{\mathsf{s}}} \rho_1 \mathrel{\hookrightarrow} \rho_2 \qquad i \notin\rho_1 \qquad A \leq?}{i\,?A,\rho_0 \mathbin{\oplus_{\mathsf{s}}} \rho_1 \mathrel{\hookrightarrow} i\,?A,\rho_2} i ? A , ρ 0 ⊕ s ρ 1 ↪ i ? A , ρ 2 ρ 0 ⊕ s ρ 1 ↪ ρ 2 i ∈ / ρ 1 A ≤ ? SC-WEAKE XTR?
ε ⊕ s ρ 1 ↪ ρ 2 ε ⊕ s i ▶ A , ρ 1 ↪ i ▶ A , ρ 2 \frac{\varepsilon\mathbin{\oplus_{\mathsf{s}}} \rho_1 \mathrel{\hookrightarrow} \rho_2}{\varepsilon\mathbin{\oplus_{\mathsf{s}}} i\mathbin{\blacktriangleright} A,\rho_1 \mathrel{\hookrightarrow} i\mathbin{\blacktriangleright} A,\rho_2} ε ⊕ s i ▶ A , ρ 1 ↪ i ▶ A , ρ 2 ε ⊕ s ρ 1 ↪ ρ 2 SC-WEAKEXTR?
ε ⊕ s ρ 1 ↪ ρ 2 ε ⊕ s i : A , ρ 1 ↪ i : A , ρ 2 \frac{\varepsilon\mathbin{\oplus_{\mathsf{s}}} \rho_1 \mathrel{\hookrightarrow} \rho_2}{\varepsilon\mathbin{\oplus_{\mathsf{s}}} i:A,\rho_1 \mathrel{\hookrightarrow} i:A,\rho_2} ε ⊕ s i : A , ρ 1 ↪ i : A , ρ 2 ε ⊕ s ρ 1 ↪ ρ 2 SC-OPTIONALEXTR?
ε ⊕ s ρ 1 ↪ ρ 2 A ≤ ? ε ⊕ s i ? A , ρ 1 ↪ i ? A , ρ 2 \frac{\varepsilon\mathbin{\oplus_{\mathsf{s}}} \rho_1 \mathrel{\hookrightarrow} \rho_2 \qquad A \leq?}{\varepsilon\mathbin{\oplus_{\mathsf{s}}} i\,?A,\rho_1 \mathrel{\hookrightarrow} i\,?A,\rho_2} ε ⊕ s i ? A , ρ 1 ↪ i ? A , ρ 2 ε ⊕ s ρ 1 ↪ ρ 2 A ≤ ? (Syntax-Directed Record Type Concat)
⋆ 0 ⊕ s ⋆ 1 ↪ ⋆ 2 \star_0 \mathbin{\oplus_{\mathsf{s}}} \star_1 \mathrel{\hookrightarrow} \star_2 ⋆ 0 ⊕ s ⋆ 1 ↪ ⋆ 2
SC-STRONGR
: ⊕ s ▶ ↪ ▶ :\mathbin{\oplus_{\mathsf{s}}} \mathbin{\blacktriangleright} \mathrel{\hookrightarrow} \mathbin{\blacktriangleright} : ⊕ s ▶ ↪ ▶ SC-LATER
? ⊕ s ⋆ ↪ ⋆ ?\mathbin{\oplus_{\mathsf{s}}} \star\mathrel{\hookrightarrow} \star ? ⊕ s ⋆ ↪ ⋆ SC-LEAVE
: ⊕ s ? ↪ : :\mathbin{\oplus_{\mathsf{s}}}? \mathrel{\hookrightarrow}: : ⊕ s ? ↪ : SC-REPLACE
: ⊕ s : ↪ : :\mathbin{\oplus_{\mathsf{s}}}: \mathrel{\hookrightarrow}: : ⊕ s : ↪ : SC-FORGET
: ⊕ s ? ↪ ? :\mathbin{\oplus_{\mathsf{s}}}? \mathrel{\hookrightarrow}? : ⊕ s ? ↪ ? (Syntax-Directed Strength Concat)
Lambda Calculus Syntax and Semantics
τ : : = τ 0 → τ 1 ∣ N type e : : = x ∣ λ x . e ∣ e 0 e 1 ∣ n term Γ : : = ε ∣ Γ , x : τ environment ι : : = ε ∣ ι , x ∼ i translation environment \begin{aligned}
\tau&::= \tau_0 \to\tau_1 \mid N && \text{type}\\
e &::= x \mid\lambda x.e \mid e_0\,e_1 \mid n && \text{term}\\
\Gamma&::= \varepsilon\mid\Gamma,x:\tau&& \text{environment}\\
\iota&::= \varepsilon\mid\iota,x\sim i && \text{translation environment}
\end{aligned} τ e Γ ι ::= τ 0 → τ 1 ∣ N ::= x ∣ λ x . e ∣ e 0 e 1 ∣ n ::= ε ∣ Γ , x : τ ::= ε ∣ ι , x ∼ i type term environment translation environment Γ ⊢ e : τ \Gamma\vdash e:\tau Γ ⊢ e : τ LT-var
x : τ ∈ Γ Γ ⊢ x : τ \frac{x:\tau\in\Gamma}{\Gamma\vdash x:\tau} Γ ⊢ x : τ x : τ ∈ Γ LT-lam
Γ , x : τ 0 ⊢ e : τ 1 Γ ⊢ λ x . e : τ 0 → τ 1 \frac{\Gamma,x:\tau_0\vdash e:\tau_1}{\Gamma\vdash\lambda x.e:\tau_0\to\tau_1} Γ ⊢ λ x . e : τ 0 → τ 1 Γ , x : τ 0 ⊢ e : τ 1 LT-app
Γ ⊢ e 0 : τ 0 → τ 1 Γ ⊢ e 1 : τ 0 Γ ⊢ e 0 e 1 : τ 1 \frac{\Gamma\vdash e_0:\tau_0\to\tau_1\qquad\Gamma\vdash e_1:\tau_0}{\Gamma\vdash e_0\,e_1:\tau_1} Γ ⊢ e 0 e 1 : τ 1 Γ ⊢ e 0 : τ 0 → τ 1 Γ ⊢ e 1 : τ 0 LT-nat
Γ ⊢ n : N \frac{}{\Gamma\vdash n:N} Γ ⊢ n : N e ⟶ e ′ e\longrightarrow e' e ⟶ e ′ LE-appl
e 0 ⟶ e 0 ′ e 0 e 1 ⟶ e 0 ′ e 1 \frac{e_0\longrightarrow e_0'}{e_0\,e_1\longrightarrow e_0'\,e_1} e 0 e 1 ⟶ e 0 ′ e 1 e 0 ⟶ e 0 ′ LE-appr
e ⟶ e ′ v e ⟶ v e ′ \frac{e\longrightarrow e'}{v\,e\longrightarrow v\,e'} v e ⟶ v e ′ e ⟶ e ′ LE-lamApp
( λ x . e ) v ⟶ e [ v / x ] (\lambda x.e)\,v\longrightarrow e[v/x] ( λ x . e ) v ⟶ e [ v / x ] Lambda Calculus Term Approximation
δ : : = ε ∣ δ , x ≈ i ∣ δ , i : v \delta::= \varepsilon\mid\delta,x\approx i \mid\delta,i:v δ ::= ε ∣ δ , x ≈ i ∣ δ , i : v δ ⊢ e s ≈ e \delta\vdash e_s\approx e δ ⊢ e s ≈ e A-varBound
\frac{i:v\in\delta\qquad\varepsilon\vdash v_s\approx v}{\delta\vdash v_s\approx@.i}
A-varFree
\frac{x\approx i\in\delta}{\delta\vdash x\approx@.i}
A-lam
δ , x ≈ i ⊢ e s ≈ e δ ⊢ λ x . e s ≈ λ { _ ⋄ i } . e \frac{\delta,x\approx i\vdash e_s\approx e}{\delta\vdash\lambda x.e_s\approx\lambda\{\,\_ \diamond i\,\}.e} δ ⊢ λ x . e s ≈ λ { _ ⋄ i } . e δ , x ≈ i ⊢ e s ≈ e A-closure
∥ o ∥ , x ≈ i ⊢ e s ≈ e δ ⊢ λ x . e s ≈ ⟨ o ; ε ∣ λ { _ ⋄ i } . e ⟩ \frac{\lVert o\rVert,x\approx i\vdash e_s\approx e}{\delta\vdash\lambda x.e_s\approx\langle o;\varepsilon\mid\lambda\{\,\_\diamond i\,\}.e\rangle} δ ⊢ λ x . e s ≈ ⟨ o ; ε ∣ λ { _ ⋄ i } . e ⟩ ∥ o ∥ , x ≈ i ⊢ e s ≈ e A-closureApp
∥ o ∥ , x ≈ i ⊢ e s ≈ e ε ⊢ v s ≈ v δ ⊢ ( λ x . e s ) v s ≈ force ⟨ o ; _ : v ∣ λ { _ ⋄ i } . e ⟩ \frac{\lVert o\rVert,x\approx i\vdash e_s\approx e\qquad\varepsilon\vdash v_s\approx v}{\delta\vdash(\lambda x.e_s)v_s\approx\operatorname{force}\langle o;\_ :v\mid\lambda\{\,\_\diamond i\,\}.e\rangle} δ ⊢ ( λ x . e s ) v s ≈ force ⟨ o ; _ : v ∣ λ { _ ⋄ i } . e ⟩ ∥ o ∥ , x ≈ i ⊢ e s ≈ e ε ⊢ v s ≈ v A-app
δ ⊢ e s 0 ≈ e 0 δ ⊢ e s 1 ≈ e 1 δ ⊢ e s 0 e s 1 ≈ force e 0 { _ : e 1 } \frac{\delta\vdash e_{s0}\approx e_0\qquad\delta\vdash e_{s1}\approx e_1}{\delta\vdash e_{s0}\,e_{s1}\approx\operatorname{force}\ e_0\{\,\_ :e_1\,\}} δ ⊢ e s 0 e s 1 ≈ force e 0 { _ : e 1 } δ ⊢ e s 0 ≈ e 0 δ ⊢ e s 1 ≈ e 1 A-box
∥ o ∥ ⊢ e s ≈ e δ ⊢ e s ≈ { o } ▹ e \frac{\lVert o\rVert\vdash e_s\approx e}{\delta\vdash e_s\approx\{\,o\,\}\mathbin{\triangleright}e} δ ⊢ e s ≈ { o } ▹ e ∥ o ∥ ⊢ e s ≈ e A-nat
δ ⊢ n ≈ n \frac{}{\delta\vdash n\approx n} δ ⊢ n ≈ n ∥ o ∥ ∥ ε ∥ = ε ∥ o , i : v ∥ = ∥ o ∥ , i : v \begin{aligned}
\lVert o\rVert\,\lVert\varepsilon\rVert&=\varepsilon\\
\lVert o,i:v\rVert&=\lVert o\rVert,i:v
\end{aligned} ∥ o ∥ ∥ ε ∥ ∥ o , i : v ∥ = ε = ∥ o ∥ , i : v ∥ ι ∥ ∥ ε ∥ = ε ∥ ι , x ∼ i ∥ = ∥ ι ∥ , x ≈ i \begin{aligned}
\lVert\iota\rVert\,\lVert\varepsilon\rVert&=\varepsilon\\
\lVert\iota,x\sim i\rVert&=\lVert\iota\rVert,x\approx i
\end{aligned} ∥ ι ∥ ∥ ε ∥ ∥ ι , x ∼ i ∥ = ε = ∥ ι ∥ , x ≈ i 
