Functional record extension and row capture
From Successor ML
Contents |
Introduction
We propose adding a form of functional record extension as well as its inverse: a form of functional row capture.
Functional record update can be expressed as a combination of the two.
Motivation
When using records, it is sometimes necessary to construct new records from existing ones, by adding only a small number of fields. Similarly, it can be convenient to be able to construct a new record by removing a small number of fields.
Currently, SML provides no convenient way of expressing this.
TODO: nice example
Row capture
We propose supporting row capture by raising the status of the ellipsis ... in record patterns to make it analogous to a normal field name. The ellipsis refers to all the other fields that have not been named explicitly.
Example:
val { d = x, p = y, ... = r } = e
This val binding takes the result of expression e, which must be some record that has at least fields d and p, and takes it apart. As usual, it binds the values of the d and p fields to x and y, respectively. But in addition it also binds r to a freshly constructed record value that consists of all the fields of e except d and p.
Example:
val { d = x, p = y, ... = r } = { a = 1, c = 3.0, d = nil, f = [1], p = "hello", z = NONE }
binds x to nil, y to "hello", and r to { a = 1, c = 3.0, f = [1], z = NONE }.
Record extension
We propose to support functional record extension by allowing ellipses in record expressions. This restores a sense of "perfect symmetry" between record patterns and record expressions.
Example:
{ d = e1, p = e2, ... = e3 }
Here e3 is required to be of record type without fields d and p. The result of the above expression is a record which consists of all the fields that were present in the result of e3 as well as a field d whose type and value are determined by e1 and a field p whose type and value are determined by e2.
Example:
let val r = { a = 1, c = 3.0, f = [1], z = NONE }
in { d = nil, p = "hello", ... = r }
end
yields { a = 1, c = 3.0, d = nil, f = [1], p = "hello", z = NONE }.
Record type extension
Like record values, record types can be constructed by extension.
Example:
type 'a t = { a : 'a, b : bool }
type 'a u = { c : char, d : 'a list, ... : 'a t }
Again, ellipses denote the type that is to be extended. It must be a record type. The result is a record type which consists of the combined fields. The example yields
type 'a u = {a : 'a, b : bool, c : char, d : 'a list}
Expressing functional record update
Functional record update can be expressed by a combination of row capture and record extension, as can be observed in the following example:
let val r = { a = 1, c = 3.0, d = "not a list", f = [1], p = ["not a string"], z = NONE }
in { r where d = nil, p = "hello" }
end
can be rewritten as:
let val r = { a = 1, c = 3.0, d = "not a list", f = [1], p = ["not a string"], z = NONE }
val { d = _, p = _, ... = tmp } = r
in { ... = tmp, d = nil, p = "hello" }
end
where tmp is an otherwise unused (fresh) variable.
Assumptions
None.
Syntax
Defined by the following changes to the Definition:
- In Section 2.8, Figure 3, change the production for pattern row wildcards to:
[patrow ::=] ... = pat ellipses
- Add the following production for type-expression rows:
[tyrow ::=] ... : ty ellipses
- In Section 2.8, Figure 4, add the following production for expression rows:
[exprow ::=] ... = exp ellipses
- In Section 2.9, remove the first bullet ruling out repeated labels.
- In Appendix A, Figure 15, add a box for expression rows:
Expression Rows
+-------------------+----------------------------------------------------+
| ... = exp, exprow | ... = let val vid = exp in {exprow, ... = vid} end |
+-------------------+----------------------------------------------------+
(see note in text concerning exprow; vid new)
- In Appendix A, Figure 16, extend the box for pattern rows as follows:
+---------------------+---------------------+
| ... | ... = _ |
+---------------------+---------------------+
| ... <= pat>, patrow | patrow, ... <= pat> |
+---------------------+---------------------+
(see note in text concerning patrow)
- Add a box for type-expression rows:
Type-expression Rows
+-----------------+-----------------+
| ... : ty, tyrow | tyrow, ... : ty |
+-----------------+-----------------+
(see note in text concerning tyrow)
- In Appendix A, add the following paragraph:
Note that the derived forms for ellipses in the middle of expression rows, pattern rows or type-expression rows are only valid if they can be transformed to bare syntax. This implies that the remaining rows may not again contain ellipses.
- In Appendix B, Figure 20, add the following production for expression rows:
[exprow ::=] ... = exp <, exprow> ellipses
- In Appendix B, Figure 22, change the production for pattern row wildcards to:
[patrow ::=] ... <= pat> <, patrow> ellipses
- In Appendix B, Figure 23, add the following production for type-expression rows:
[tyrow ::=] ... : ty <, tyrow> ellipses
Note that we define ellipses in arbitrary position as a derived form, since pattern matching for mid-row ellipses is more complicated to describe in a direct style within the current rules (we had to thread back the information about what further fields to remove from the row).
Static Semantics
Defined by the following changes to the Definition:
- In Section 4.7, add the following production for non-expansive expression rows:
[nexprow ::=] ... = nexp
- In Section 4.10, Expression Rows, change Rule 6 to:
C |- exp => tau <C |- exprow => rho lab notin Dom rho>
------------------------------------------------------------ (6)
C |- lab = exp <, exprow> => {lab |-> tau} <+ rho>
- Add the following rule:
C |- exp => rho in Type ----------------------- (6a) C |- ... = exp => rho
- In Section 4.10, Pattern Rows, change Rules 38 and 39 as follows:
C |- pat => (VE, rho in Type) ----------------------------- (38) C |- ... = pat => (VE,rho)
C |- pat => (VE,tau)
<C |- patrow => (VE',rho) Dom VE cap Dom VE' = 0 lab notin Dom rho>
------------------------------------------------------------------------- (39)
C |- lab = pat <, patrow> => (VE <+ VE'>, {lab |-> tau} <+ rho>)
- Remove the comment regarding Rule 39.
- In Section 4.10, Type-expression Rows, change Rule 49 to:
C |- ty => tau <C |- tyrow => rho lab notin Dom rho>
---------------------------------------------------------- (49)
C |- lab : ty <, tyrow> => {lab |-> tau} <+ rho>
- Remove the respective comment.
- Add the following rule:
C |- ty => rho in Type ---------------------- (49a) C |- ... : ty => rho
- In Section 4.11, change the first item to:
For each occurence of a record expression containing ellipses, i.e. of the
form {lab_1=exp_1,...,lab_m=exp_m, ...=exp_0} the program context must determine uniquely
the domain {lab_1,...,lab_n} of its row type, where m<=n; thus, the context must
determine the labels {lab_m+1,...,lab_n} of the fields of exp_0.
Likewise for record patterns containing ellipses. For these purposes, explicit type
constraints may be needed.
Dynamic Semantics
Defined by the following changes to the Definition:
- In Section 4.2, add the following definition after the paragraph defining modification of maps:
The restriction of a map f by a set S, written f\S, is defined as
f\S = { x |-> f(x) ; x in Dom f \ S }
- In Section 6.7, Expression Rows, add the following rule:
E |- exp => r in Val -------------------- (95a) E |- ... = exp => r
- In Section 6.7, Pattern Rows, change Rule 140 to:
E,r in Val |- pat => VE/FAIL ---------------------------- (140) E,r |- ... = pat => VE/FAIL
- Change Rule 142 to:
E,r(lab) |- pat => VE <E,r\{lab} |- patrow => VE'/FAIL>
---------------------------------------------------------- (142)
E,r |- lab = pat <, patrow> => VE<+VE'/FAIL>
Interactions
Given extensible rows, functional record update can be defined as a simple derived form as follows:
+----------------------+-----------------------------------+
| {atexp where exprow} | let val {patrow, ...=vid} = atexp |
| | in {exprow, ...=vid} end |
+----------------------+-----------------------------------+
where vid is fresh and patrow is obtained from exprow by replacing all right-hand sides by wildcards. Note that exprow may not contain ellipses.
Compatibility
This is a conservative extension. An experimental implementation has been done in the MLPolyR compiler. MLPolyR generalizes this feature to also allow SML#-style record polymorphism and shows that an efficient implementation of this combination is possible.
Implementation
Type inference is not entirely straightforward in the given form, but the issues are only slightly harder than those already caused by the existing ellipsis mechanism (unresolved row variables become shared between different record types and hence require additional propagation). Type inference actually becomes simpler in the presence of SML#-style record polymorphism, but an efficient implementation of the dynamic semantics becomes somewhat trickier.
