Value.Subsume with constraints

[verdverm]

I have the following

package main

import (
	"fmt"

	"cuelang.org/go/cue"
	"cuelang.org/go/cue/cuecontext"
	"cuelang.org/go/cue/errors"
)

const schema = `
{
	i: int
	s: string
}
`

const constraint = `
{
	i: >10
	s: =~"^foo"
}
`

const val = `
{
	i: 100
	s: "foobar"
}
`

func main() {
	c := cuecontext.New()
	s := c.CompileString(schema, cue.Filename("schema.cue"))
	r := c.CompileString(constraint, cue.Filename("constrain.cue"))
	v := c.CompileString(val, cue.Filename("val.cue"))

	// check subsumptions
	printErr("s > r", s.Subsume(r))
	printErr("r > s", r.Subsume(s))

	printErr("s > v", s.Subsume(v))
	printErr("v > s", v.Subsume(s))
}

func printErr(prefix string, err error) {
	if err != nil {
		msg := errors.Details(err, nil)
		fmt.Printf("%s:\n%s\n", prefix, msg)
	}
}

And I get the following output:

$ go run subsume.go 
s > r:
field i not present in {i:>10,s:=~"^foo"}:
    constrain.cue:2:1
missing field "i"

r > s:
field i not present in {i:int,s:string}:
    schema.cue:2:1
missing field "i"

v > s:
field i not present in {i:int,s:string}:
    schema.cue:2:1
missing field "i"

1. It seems the error message is off
2. I would expect s > r to not have an error, as my understanding is that a more constrained value is an instance of a less constrained value. Is that correct?

[antong]

1. Yes, the error message is about as bogus as it gets :-)
2. Yes, but the r in your example is not more constrained than s. As an example, r.i allows a float like 12.34, while s.i must be an integer.

So I think that in this case the results are correct and precise. But I've understood that CUE really can't precisely always precisely calculate whether one value subsumes another. I think that if v.Subsume(w) returns nil, then then v definitely subsumes w. But there are cases where v.Subsume(w) returns an error even though v does subsume w. One example is comparing regexps. For instance building on your example, s : =~ "^f" in reality subsumes s : =~ "^foo", but Value.Subsume() returns an error.

[verdverm]

There seems to be inconsistency in how constraints like <10 are represented. Here it seems like number, i.e. if either schema.i: number or constraint.i: int & <10, then the subsumption passes. Regexp are not compared due to the difficulty and complexity of making such an ordering, I think this was called out somewhere...

Note that <1.0 was converted to an int as in here: #1310 and is the other case for inconsistency.

[antong]

In this case I don't think it is inconsistent. The reference does say floating point numbers can be compared with integers. This would mean that the bound >10 is the infinite disjunction of all ints greater than 10 and all floats greater than ten (11|12|13|...|10.1|10.2|...|10.9|10.01|10.02|...). So while 10 is an int and not a float, still the comparison 10.7 > 10 is defined and true, so with:

schema: i: int
constraint: i: >10

then {i:10.7} is an instance of constraint, but {i:10.7} is not an instance of schema. So then constraint can't be an instance of schema and schema doesn't subsume constraint.

[verdverm]

The inconsistency is that

• in floating point bounds not as expected #1310 both <1 and <1.0 are treated as ints.
• here, <10 remains the general number which can itself be subsumed by int, float, or a bare <10

So in that case <10 is a number which is more general than int and the subsume call correctly reports an error. You have to ensure the numeric type remains consistent throughout. That is, when you have bounds constraint, you need to possibly specify the numeric type if the values being using in the subsume check have not been unified prior, as in

a: i: int
b: i: <10

neither can subsume the other. Note this is not the same as

a: i: int
b: i: int & <10

or

a: i: number
b: i: <10

where a does subsume b

---

Circling around, should <10 be treated as a number or an int? The answer to this is unclear based on the other issue and the comment from the ADT link.

[verdverm]

This all might be simplified by #253

[antong]

If I understood correctly #1310 is not about numbers in bounds treated as ints vs floats. It is a simplification bug limited to when you have an upper and lower bound for a number and then it doesn't catch impossible bounds for floats as. So I wouldn't necessarily let that issue influence the interpretation of <10.

I understand it so that with the current specification and implementation 10 is an int, but <10 is a number and can be either an int or a float, because both ints and floats can be compared to an int. And 10.0 is a float, but <10.0 includes ints.