Composable record and extension and its dual

To understand the underlying mechanism, it is instructive to first look at an example. In MLPolyR we write { a = 1, ... = r } to create a new record which extends record r with a new field a. Since records are first-class values, we can abstract over the record being extended and obtain a function add_a that extends any argument record (as long as it does not already contain a) with a field a. Such a function can be thought of as the “difference” between its result and its argument:

fun add a r = { a = 1, ... = r }

Here the difference consists of a field labeled a of type int and value 1. The type of function add_a is inferred as:

val add a: { `b } ! { a: int, `b }

We can write similar functions add_b and add_c of types { `b } -> { b:bool, `b } and { `b } -> { c:string, `b } which add fields b and c respectively:

fun add b r = { b = true, ... = r } 
fun add c r = { c = "hello", ... = r } 

We can then “add up” record differences represented by add_a, add_b, add_c by composing these functions:

fun add ab r = add a (add b r)
fun add bc r = add b (add c r)

The inferred types are:

val add_ab: { `b } -> { a: int, b: bool, `b } 
val add_bc: { `b } -> { b: bool, c: string, `b }

Finally, we can create actual records by “adding” differences to the empty record:

val a = add_a {} 
val ab = add_ab {} 
val bc = add_bc {}

When translated to the dual, extensibility of records becomes extensibility of code. Here is a function representing the difference between two code fragments, one of which can handle case ‘A while the other, represented by the argument c, cannot:

fun add A c = cases ‘A () => print "A"
              default: c

Note that function add_A corresponds to add_a of the dual. The type inferred for add A is:

val add A: (<`b> => ()) ! (<‘A of (), `b> => ())

Here a type <`r> => t denotes the type of first-class cases where <`r> is the sum type that is being handled and t is the result. One can think of => as an alternative function arrow whose elimination form will be discussed below. Examples for functions add_B and add_C (corresponding to add_b and add_c in the dual) are:

fun add B c = cases ‘B () => print "B"
              default: c
fun add C c = cases ‘C () => print "C"
              default: c

As in the dual, we can now compose difference functions to obtain larger differences:

fun add AB c = add A (add B c)
fun add BC c = add B (add C c)

By applying a difference to the empty case nocases we obtain case values:

val case A = add A nocases
val case AB = add AB nocases
val case BC = add BC nocases

These values can be used in a match form. The match construct is the elimination form for the case arrow =>. The following expression will cause "B" to be printed:

match ‘B () with case BC

The previous examples demonstrate how functional record extension in the primal corresponds to code extension in the dual. This forms the basis for our proposed solution to the expression problem. In the non-recursive case, code extension is as straightforward as shown above.