From b382b61bf66506a920e05f2ff44b584d2618b7d5 Mon Sep 17 00:00:00 2001 From: Tony Garnock-Jones Date: Mon, 27 Mar 2023 23:07:41 +0200 Subject: [PATCH] Merges --- preserves.md | 37 ++++++++++++++++++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/preserves.md b/preserves.md index 98f9e08..475a12e 100644 --- a/preserves.md +++ b/preserves.md @@ -174,7 +174,7 @@ URL, compared according to usually be represented as ordinary `Value`s, in which case the ordinary rules for comparing `Value`s will apply. -## Examples +## Appendix. Examples The definitions above are independent of any particular concrete syntax. The examples of `Value`s that follow are written using [the Preserves @@ -358,5 +358,40 @@ encodes to binary as follows: 84 84 +## Appendix. Merging Values + +The *merge* of two `Value`s is a combination of the two values that includes all information +from each that is missing from the other. If the values are incompatible, they have no merge. + + - the merge of two `Atom`s has no value if they are not [equal](#equivalence); otherwise, it + has value equal to (an arbitrary) one of the atoms. + + - the merge of two `Embedded`s depends on the interpretation of the embedded values, and so is + implementation-defined. + + - the merge of two `Compound`s is: + + - if both are `Sequence`s, let `n` be the minimum of the lengths of the two sequences. If + every merge of corresponding positions up to `n` in the sequences is defined, the result + is defined, with elements merged up to position `n` and simply copied from the longer + sequence from position `n` onward; otherwise, it is undefined. + + - if both are `Record`s, the `Record` with the merge of the two input records' labels as its + label and the merge of the inputs' field sequences as its fields; + + - if both are `Dictionary`s, if every merge of values associated with keys common to both + inputs is defined, the result is defined, with merged values at common keys and simply + copied from either side for keys unique to that side; otherwise, it is undefined. + + - Otherwise, the merge is undefined. + +**Examples.** + + - `merge [1, [2], 3] [1, [2, 99], 3, 4, 5] = merge [1, [2, 99], 3, 4, 5]` + - `merge [1, 2, 3] [1, 5, 3] = ⊥` + - `merge #{a, b, c} #{a, b, c} = ⊥` + - `merge {a: 1, b: [2]} {b: [2, 99] c: 3} = {a: 1, b: [2, 99], c: 3}` + - `merge {a: 1, b: [2]} {a: 5, b: [2]} = ⊥` + ## Notes