Comparison to bottom, v0.2.2 vs 0.3.0

[cueckoo]

Originally opened by @pipex in cuelang/cue#601

Hi,

As part of the experimentation I'm doing with cue I wanted to write a simple cue specification to validate other cue specifications.

The problem is that I'm not getting the same results for cue v0.2.2 and v0.3.0-alpha5 for some more complex structures.

The way I perform the test is by unifying a test subject with the assertion and comparing to bottom.

subject: _
rejects: _
passes: (subject & rejects) == _|_

But on testing a structure with a simple comprehension

subject: {
	keys: [for k,s in states {k}]
	initial: or(keys) // intitial must be a valid state key
	states: [K=string]: {
		key: K
	}
}

rejects: {
	initial: "blue"
	states: "red": {}
	states: "green": {}
}

passes: (subject & rejects) == _|_

v0.2.2 returns true for passes (the expected behavior) and v0.3.0 returns false. I think the issue is with the latest version is not treating incomplete values to be the same as bottom. If I add a property

unification: (subject & rejects)

On cue eval, v0.3.0 returns

...
passes: true
unification: {
    keys: ["red", "green"]
    initial: or(keys) & "blue"
    states: {
        red: {
            key: "red"
        }
        green: {
            key: "green"
        }
    }
}

while v0.2.2 returns

unification.initial: empty disjunction: conflicting values "red" and "blue":
    ./example.cue:2:20
    ./example.cue:10:11

Is this a bug? Am I expecting the wrong result from a comparison with bottom?

Thanks for your help

[cueckoo]

Original reply by @pipex in cuelang/cue#601 (comment)

If anyone is curious, the idea for the testing schema to be able to write tests as follows

example: #TestSuite
example: describe: "Test suite": {
	subject: =~"^(foo|bar)+$"
	it: "should do some tests": {
		accepts: "combinations of foo and bar": [
			"foo",
			"foobar",
		]
		rejects: "incomplete combinations foo and bar": [
			"foob",
			"fo",
		]
	}
}

And through cue eval <test>.cue get

example: {
    describe: {
        "Test suite": {
            subject: =~"^(foo|bar)+$"
            it: {
                "should do some tests": {
                    accepts: {
                        "combinations of foo and bar": ["foo", "foobar"]
                    }
                    rejects: {
                        "incomplete combinations foo and bar": ["foob", "fo"]
                    }
                    passing: 2
                    failing: 0
                    failures: []
                }
            }
            passing: 1
            failing: 0
        }
    }
}

[cueckoo]

Original reply by @verdverm in cuelang/cue#601 (comment)

You might try the -c option to eval

$ cat or.cue 
keys: ["a", "b"]
testB: or(keys) & "b"
testC: or(keys) & "c"

$ cue eval or.cue 
keys: ["a", "b"]
testB: "b"
testC: or(keys) & "c"

$ cue eval -c or.cue 
testC: empty disjunction

v0.3.0 is a significant rewrite of the evaluator, and in theory should be more correct (pending any remaining bugs).

[cueckoo]

Original reply by @pipex in cuelang/cue#601 (comment)

Hi @verdverm, thanks for your reply. Here is the full example

// example.cue
subject: {
	keys: [for k,s in states {k}]
	initial: or(keys)
	states: [K=string]: {
		key: K
	}
}

rejects: {
	initial: "blue"
	states: "red": {}
	states: "green": {}
}

passes: (subject & rejects) == _|_

With cue 0.2.2

cue eval example.cue                                                                                                                                     main  ✭ ✱
subject: {
    keys: []
    states: {}
    initial: or(keys)
}
rejects: {
    states: {
        red: {}
        green: {}
    }
    initial: "blue"
}
passes: true

With cue 0.3.0-alpha5

./cue-0.3.0-alpha5 eval example.cue                                                                                                                      main  ✭ ✱
subject: {
    keys: []
    initial: or(keys)
    states: {}
}
rejects: {
    initial: "blue"
    states: {
        red: {}
        green: {}
    }
}
passes: false

Using the -c option, I get with both

subject.initial: empty list in call to or:

Which maybe means I'm misunderstanding how comprehensions should evaluate? I would expect the result of or(keys) to restrict the value of initial property to the keys in the states property

[cueckoo]

Original reply by @verdverm in cuelang/cue#601 (comment)

Probably need @mpvl to comment on this one. This is probably the result of a semantic change in the evaluator, or a bug.

[cueckoo]

Original reply by @verdverm in cuelang/cue#601 (comment)

keys: ["a", "b"]
testB: or(keys) & "b"
testC: or(keys) & "c"

p1: testB == _|_
p2: testC == _|_

A: {
        keys: ["a", "b"]
        test: or(keys)
}

B: {
        test: "b"
}

C: {
        test: "c"
}

u3: (A & B)
p3: (A & B) == _|_
u4: (A & C)
p4: (A & C) == _|_


$ cue eval or.cue
keys: ["a", "b"]
testB: "b"
testC: or(keys) & "c"
p1:    false
p2:    true
A: {
    keys: ["a", "b"]
    test: "a" | "b"
}
B: {
    test: "b"
}
C: {
    test: "c"
}
u3: {
    keys: ["a", "b"]
    test: "b"
}
p3: false
u4: {
    keys: ["a", "b"]
    test: or(keys) & "c"
}
p4: false

From this, I think the question might be "is a field with an invalid disjunction == _|_ while a struct with a nested invalid disjunction != _|_?"

[cueckoo]

Original reply by @pipex in cuelang/cue#601 (comment)

Adding the unification field yields in 0.2.2

unification.initial: empty disjunction: conflicting values "red" and "blue":
    ./example.cue:3:20
    ./example.cue:11:1

And in 0.3.0

subject: {
    keys: []
    initial: or(keys)
    states: {}
}
rejects: {
    initial: "blue"
    states: {
        red: {}
        green: {}
    }
}
unification: {
    keys: ["red", "green"]
    initial: or(keys) & "blue"
    states: {
        red: {
            key: "red"
        }
        green: {
            key: "green"
        }
    }
}
passes: false

The unification shows the values I would expect, except for the value of initial which it looks like is not resolving to anything (even though all the information is there)

[cueckoo]

Original reply by @verdverm in cuelang/cue#601 (comment)

This may be intentional: https://github.com/cuelang/cue/blob/master/cue/testdata/builtins/all.txtar#L13

[cueckoo]

Original reply by @pipex in cuelang/cue#601 (comment)

Any thoughts on this @mpvl?

[cueckoo]

Original reply by @mpvl in cuelang/cue#601 (comment)

This seems related to #475. See cuelang/cue#475 (comment).

Especially the coined terminology of "open disjunctions" seems relevant here.

Basically, the use of _|_ can give rise to non-monotonic behavior if not done properly. Comparing against _|_ is akin to a logical not, which is a questionable construct. So the mechanism in place here is preventing this. v0.2 was really poor at this, but v0.3 is probably too aggressive at doing so. This actually happens all over the place already (looking of a non-existing field in an open struct is incomplete, while for a closed struct it is fatal, for instance), but this case is particularly tricky.

We need to find the right balance here. Note that we also intend to add must() #575 and not() #571 , which are two other necessary evils with similar characteristics. It makes sense to address all of these in unison.

This is a nice example, though, and I've added it to #475. I think here that the evaluator should at some point recognize that growing the size of keys isn't gonna happen anymore and make the error fatal, after which your check will return true.

The good thing is that although this is a complicated matter and these bugs are hard to understand, the user generally won't have to think about the distinction and won't be confronted with it once the bugs are gone.