Gitiles

commit | 6e5d9939f2c543e339d16a5cf0a97ca8ac43eea2 | [log] [tgz] |
---|---|---|

author | Marcel van Lohuizen <mpvl@golang.org> | Thu Mar 14 15:52:48 2019 +0100 |

committer | Marcel van Lohuizen <mpvl@google.com> | Sun Mar 31 11:33:39 2019 +0000 |

tree | 2b1db3bb32ac8c7e3bdfb2b540f84d0647f966c2 | |

parent | 8dfef670f5c227b3a4324de5d0ca4c449bbedb00 [diff] |

doc/ref: alternative alternative spec for default values See jba’s https://cue-review.googlesource.com/c/cue/+/1341. Change-Id: I405624fa2d41c8dbeb4fb5f2788f3da84c51623d Reviewed-on: https://cue-review.googlesource.com/c/cue/+/1660 Reviewed-by: Marcel van Lohuizen <mpvl@google.com>

diff --git a/doc/ref/spec.md b/doc/ref/spec.md index 94228ec..be367c3 100644 --- a/doc/ref/spec.md +++ b/doc/ref/spec.md

@@ -625,7 +625,7 @@ - The disjunction of two bottom values is bottom. Disjunction in CUE is a [binary expression](#Operands), written `a | b`. -It is commutative and associative. +It is commutative, associative, and idempotent. The unification of a disjunction with another value is equal to the disjunction composed of the unification of this value with all of the original elements @@ -643,93 +643,156 @@ ("a" | "b") & "c" _|_ ``` +A disjunction is _normalized_ if there is no element +`a` for which there is an element `b` such that `a ⊑ b`. + +<!-- +Normalization is important, as we need to account for spurious elements +For instance "tcp" | "tcp" should resolve to "tcp". + +Also consider + + ({a:1} | {b:1}) & ({a:1} | {b:2}) -> {a:1} | {a:1,b:1} | {a:1,b:2}, + +in this case, elements {a:1,b:1} and {a:1,b:2} are subsumed by {a:1} and thus +this expression is logically equivalent to {a:1} and should therefore be +considered to be unambiguous and resolve to {a:1} if a concrete value is needed. + +For instance, in + + x: ({a:1} | {b:1}) & ({a:1} | {b:2}) // -> {a:1} | {a:1,b:1} | {a:1,b:2} + y: x.a // 1 + +y should resolve to 1, and not an error. + +For comparison, in + + x: ({a:1, b:1} | {b:2}) & {a:1} // -> {a:1,b:1} | {a:1,b:2} + y: x.a // _|_ + +y should be an error as x is still ambiguous before the selector is applied, +even though `a` resolves to 1 in all cases. +--> + #### Default values -One or more values in a disjunction can be _marked_ -by prefixing it with a `*` ([a unary expression](#Operators)). -A bottom value cannot be marked. -When a marked value is unified, the result is also marked. -(When unification results in a single value, -the mark is dropped, as single values cannot be marked.) +Any element of a disjunction can be marked as a default +by prefixing it with an asterisk '*'. +Intuitively, when an expression needs to be resolved for an operation other +than unification or disjunctions, +non-starred elements are dropped in favor of starred ones if the starred ones +do not resolve to bottom. -A disjunction is _normalized_ if there is no unmarked element -`a` for which there is an element `b` such that `a ⊑ b` -and no marked element `c` for which there is a marked element -`d` such that `c ⊑ d`. -A disjunction literal must be normalized. +More precisely, any value `v` may be associated with a default value `d`, +denoted `(v, d)` (not CUE syntax), +where `d` must be in instance of `v` (`d ⊑ v`). +The rules for unifying and disjoining such values are as follows: + +``` +U1: (v1, d1) & v2 => (v1&v2, d1&v2) +U2: (v1, d1) & (v2, d2) => (v1&v2, d1&d2) + +D1: (v1, d1) | v2 => (v1|v2, d1) +D2: (v1, d1) | (v2, d2) => (v1|v2, d1|d2) +``` + +For any other operation, such as arithmetic expressions, indices, slices, and +selectors, the value `(v, d)` yields `d` if it is not bottom, or `v` otherwise. + +Default values may be introduced within disjunctions +by _marking_ terms of a disjunction with an asterisk `*` +([a unary expression](#Operators)). +The default value of a disjunction with marked terms is the disjunction +of those marked terms, applying the following rules for marks: + +``` +M1: *v => (v, v) +M2: *(v1, d1) => (v1, d1) +``` + +``` +Expression Value-default pair Rules applied +*"tcp" | "udp" ("tcp"|"udp", "tcp") M1, D1 +string | *"foo" (string, "foo") M1, D1 + +*1 | 2 | 3 (1|2|3, 1) M1, D1 + +(*1|2|3) | (1|*2|3) (1|2|3, 1|2) M1, D1, D2 +(*1|2|3) | *(1|*2|3) (1|2|3, 1|2) M1, D1, M2, D2 +(*1|2|3) | (1|*2|3)&2 (1|2|3, 1|2) M1, D1, U1, D2 + +(*1|2) & (1|*2) (1|2, _|_) M1, D1, U2 +``` + +The rules of subsumption for defaults can be derived from the above definitions +and are as follows. + +``` +(v2, d2) ⊑ (v1, d1) if v2 ⊑ v1 and d2 ⊑ d1 +(v1, d1) ⊑ v if v1 ⊑ v +v ⊑ (v1, d1) if v ⊑ d1 +``` + +<!-- +For the second rule, note that by definition d1 ⊑ v1, so d1 ⊑ v1 ⊑ v. + +The last one is so restrictive as v could still be made more specific by +associating it with a default that is not subsumed by d1. + +Proof: + by definition for any d ⊑ v, it holds that (v, d) ⊑ v, + where the most general value is (v, v). + Given the subsumption rule for (v2, d2) ⊑ (v1, d1), + from (v, v) ⊑ v ⊑ (v1, d1) it follows that v ⊑ d1 + exactly defines the boundary of this subsumption. +--> <!-- (non-normalized entries could also be implicitly marked, allowing writing int | 1, instead of int | *1, but that can be done in a backwards -compatible way later if really desirable). - -Normalization is important, as we need to account for spurious elements -For instance -"tcp" | "tcp", or -({a:1} | {b:1}) & ({a:1} | {b:2}) -> {a:1} | {a:1,b:1} | {a:1,b:2}, - -In the latter case, elements {a:1,b:1} and {a:1,b:2} are subsumed by {a:1}. -Note that without defaults, {a:1} | {a:1,b:1} | {a:1,b:2} is logically -identical to {a:1}. -More to the point, without normalization unifying {a:1} | {b:1} with {a:1,b:2} -results in a single value and thus resolves, -whereas unifying {a:1} | {a:1,b:1} | {a:1,b:2} with {a:1,b:2} -results in two values, and thus does not resolve. -With normalization: -({a:1} | {a:1,b:1} | {a:1,b:2}) & {a:1} {a:1}, instead of _|_, -({a:1} | {b:1}) & {a:1} {a:1} (instead of _|_), as {a:1,b:1} ⊑ {a:1} +compatible way later if really desirable, as long as we require that +disjunction literals be normalized). --> -If a disjunction appears where a concrete value is required -(that is, as an operand or in a location where it will be emitted), -the result is, after normalization and after dropping non-marked elements -if some elements are marked, -the resulting value itself if only a single value remains or bottom otherwise. - -<!-- -We treat remaining marked and unmarked elements the same to have less surprises: - -Unifying {a:1}|{b:1} with *{}|string produces *{a:1}|*{b:1}. It would be -surprising to have a different default for {a:1}|{b:1} and *{a:1}|*{b:1} in -this case. - -Similarly, we do not unify the remaining elements to minimize the difference -between using a disjunction in cases where concrete values are required -versus otherwise. ---> - -<!-- TODO: is the above definition precise enough, or perhaps too abstract? -Previously: - -A default value is chosen if the disjunction is not used -in a unification or disjunction operation. -This means that, in practice, a default is chosen for almost any expression -that does not involve `&` and `|`, including slices, indices, selectors, -and all but a few explicitly marked builtin functions. --> ``` -Expression Default -"tcp" | "udp" _|_ // more than one element remaining +Expression Resolves to +"tcp" | "udp" "tcp" | "udp" *"tcp" | "udp" "tcp" float | *1 1 *string | 1.0 string +(*1|2|3) | (1|*2|3) 1|2 +(*1|2|3) & (1|*2|3) 1|2|3 // default is _|_ + +(* >=5 | int) & (* <=5 | int) 5 + (*"tcp"|"udp") & ("udp"|*"tcp") "tcp" (*"tcp"|"udp") & ("udp"|"tcp") "tcp" (*"tcp"|"udp") & "tcp" "tcp" -(*"tcp"|"udp") & (*"udp"|"tcp") _|_ // "tcp" & "udp" +(*"tcp"|"udp") & (*"udp"|"tcp") "tcp" | "udp" // default is _|_ (*true | false) & bool true (*true | false) & (true | false) true -{a: 1} | {b: 1} _|_ // more than one element remaining +{a: 1} | {b: 1} {a: 1} | {b: 1} {a: 1} | *{b: 1} {b:1} -*{a: 1} | *{b: 1} _|_ // more than one marked element remaining -({a: 1} | {b: 1}) & {a:1} {a:1} // after eliminating {a:1,b:1} -({a:1}|*{b:1}) & ({a:1}|*{b:1}) {b:1} // after eliminating *{a:1,b:1} +*{a: 1} | *{b: 1} {a: 1} | {b: 1} +({a: 1} | {b: 1}) & {a:1} {a:1} // after eliminating {a:1,b:1} by normalization +({a:1}|*{b:1}) & ({a:1}|*{b:1}) {b:1} // after eliminating {a:1,b:1} by normalization ``` +<!-- +TODO: to be consistent, we should probably drop this requirement and define +for such operation which which types a value is unified. + +For instance, right now [1, 2][0.0] is not allowed, +whereas [1, 2][0] is (implicitly unified with int). +It would be consistent to allow [1, 2]["foo" | 0] to work as well. +The alternative is to disallow [1, 2][0], which would be quite annoying. +--> + A disjunction always evaluates to the same default value, regardless of the context in which the value is used. For instance, `[1, 3][*"a" | 1]` will result in an error, as `"a"` will be