Inconsistent evaluation of unification?

[cueckoo]

Originally opened by @kumorid in cuelang/cue#964

What version of CUE are you using (cue version)?

$ cue version
cue version 0.4.0-beta.1 darwin/amd64

Does this issue reproduce with the latest release?

Yes

What did you do?

Given the files below

-- test1.cue --
#T: {
  a?: int

  isA: a != _|_ 
}

d: #T & {a: 56}
e: #T 

-- test2.cue --
#T: {
  a?: int

  isA: a != _|_ 
  valid:  isA & true
}

d: #T & {a: 56}

-- test3.cue --
#T: {
  isa: bool

  valid: isa & true
}
d: #T & {a: 56}

I ran cue export test1.cue, cue export test2.cue and cue export test3.cue, consecutively.

What did you expect to see?

The output of the first export:

{
    "d": {
        "a": 56,
        "isa": true
    },
    "e": {
        "isa": false
    }
}

The output of the second export

{
    "d": {
        "a": 56,
        "isa": true
        "valid": true
    }
}

The output of the third export:

{
    "d": {
        "isa": true
       "valid": true
    }
}

What did you see instead?

The output of the first export:

{
    "d": {
        "a": 56,
        "isa": true
    },
    "e": {
        "isa": false
    }
}

The output of the second export

#T.valid: conflicting values true and false
...

The output of the third export:

{
    "d": {
        "isa": true
        "valid": true
    }
}

Which in my opinion is inconsistent, as I will explain in what follows.

Export of test1.cue

Here, on the one hand, as d provides a value for a, a is not bottom in d, and isa==true, as expected.
On the other hand, as e does not provide a value for a, a is bottom in e, and we get isa==false.

All very intuitive and expected!

Export of test2.cue,

Here, all we introduce is field valid which should be valued as the result of unifying
field isa and value true.
We also remove top-level field e to avoid producing an error.

Thus, the intuitive result is that the unification for field valid will depend
on the value of field isa, which, for top-level field d is true as seen in the export of test1.cue

However we get the error reported above!

It looks like the unification for valid does not wait to evaluate isa!!

This is puzzling,... and, in the light of the next export, inconsistent.

Export of test3.cue

In here, field isa is not computed, which seems to make a huge difference, as now, unification
seems to wait until the value of field isa is available before passing judgment.

[cueckoo]

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

Same issue as before: definitions are evaluated. So also when running export.

So the #T.valid field evaluates to false, as the error message says.

In 3, it doesn't really wait, but rather just unify bool with true, which is fine.

But I see your point. There is little one can do here without introducing a substantial language change. The problem is comparing against bottom, which is generally not a great idea. It is okay to have "incomplete" errors in definitions, that is, expressions for which not all values are available. But the result of comparing against bottom is always defined. Then once it obtains its concrete value, it will complete the other evaluations and generate an error.

It looks like the unification for valid does not wait to evaluate isa!!

It evaluates it when it can. A definition is evaluated by itself, and separately at any point it is used. So one cannot speak of evaluating too early here. As you can see, the usage of #T in d in test2 does not generate an error. It only generates the error in the definition (which is correct).

What exactly is it what you try to do here? One could just write:

#T:  a: int

if the value is required to be there, no?

[cueckoo]

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

Note that Proposal #822 introduces a concept of required fields, allowing to state explicitly that a field must have a concrete value. Is this perhaps what you are trying to do here?

[cueckoo]

Original reply by @kumorid in cuelang/cue#964 (comment)

First things first.

What exactly is it what you try to do here? One could just write:

What I presented is a simplification of what I exposed in #955. And what I presented in #955 was itself an attempt to simplify a workaround for #951. Unfortunately, our application ends up relying in a set of complex cue files, which from time to time give us trouble.

The areas that give us trouble gravitate around struct disjunctions (your suggestion to achieve our goal as posed in #955 , that is, force to give at least one among a set of fields), and repeated specification fo field restrictions (that lead to VERY LONG processing times) that we use to enforce constraints that fields should abide by.

But along the way i bumped into the issue reported here.
I won't argue that this works as it is intended to work, but if that is the case, I posit that the way it works is not consistent.

The reasoning is as follows

given

-- test2.cue --
#T: {
  a?: int
  isa: bool
  isa: a != _|_ 

  valid:  isa & true
}

d: #T & {a: 56}

-- test3.cue --
#T: {
  isa: bool

  valid: isa & true
}
d: #T & {a: true}

( I fixed some incorrect values in the original post, sorry. Also I explicitly constrained field isa to bool in test2)

from the previous examples, in both cases field isa is bool: IN BOTH CASES.
However, in one case it gives an error, and in the other case it does not.

In my opinion, the error for test2 should NOT appear, as the value of isa is just bool, which should unify happily with
true as in test3.

I cannot understand the rationale for the observed behavior.

[cueckoo]

Original reply by @myitcv in cuelang/cue#964 (comment)

But the result of comparing against bottom is always defined

@kumorid I think this is the key statement in @mpvl's response.

One strange thing I have observed however:

a1: {
    a: int
    b: a != _|_
}

a2: {
    a: 5
    b: a != _|_
}

a3: a1 & a2

evaluates to:

a1: {
	a: int
	b: false
}
a2: {
	a: 5
	b: true
}
a3: {
	a: 5
	b: true
}

(playground)

[cueckoo]

Original reply by @kumorid in cuelang/cue#964 (comment)

Hi @myitcv,

I assume by defined you mean defined with a concrete boolean value.
Yes, comparing against bottom is always defined, no argument about it, the question is "when" a particular concrete value is committed to.

If it is committed to before even unification happened (which clearly it is not, as my testx.cue exemplify) it would seem to be of dubious use.

Going to your example: yes, it is strange.

Clearly, field b in a1 is defined, albeit only as an int, with no concrete int value, but definitely, not bottom.
So, that looks like a bug to me.

Maybe comparison to bottom is trying to do too many things: report when a field cannot get any value AND report when a field does not exist, and this gives some trouble (just a speculation).

In our application, I believe all cases of comparing against bottom are to check existence of a particular field.
And commitment to a particular boolean value takes into account unifications.

[cueckoo]

Original reply by @myitcv in cuelang/cue#964 (comment)

Maybe comparison to bottom is trying to do too many things: report when a field cannot get any value AND report when a field does not exist, and this gives some trouble (just a speculation).

That is indeed the case, which is one of the mains reasons for cuelang/cue#943

[cueckoo]

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

@kumorid: solving the processing time for disjunction problem is high on the agenda. It is a bit work, but it will consist of several solutions that each will have a big impact.

In my opinion, the error for test2 should NOT appear, as the value of isa is just bool,

The value of isa is not just bool in test2: it is bool & a != _|_, where a != _|_ evaluates rightfully to false. Note that the failure does not occur at d.valid, where a != _|_ evaluates to true, but at #T.valid, where it doesn't.

Note that comparison against bottom checks whether the field is present and whether it is concrete. Optional fields (those with ?) are NOT considered to be present, so it evaluates to false. It doesn't matter whether or not the value is concrete. This is perhaps one of the surprising things about optional fields, and one of the reason for the desire to get rid of them (see required field proposal). Note that foo?: bool is a shorthand for ["foo"]: bool, which maybe is more intuitive as to what it means.

Also, the semantics of comparators require that their operands be concrete.

So all in all, it is working as intended, that is not to say it is an ideal interpretation.

The core builtins proposal is supposed to clean up the semantics of comparing against bottom.

Another unfortunate thing: we ignore any errors in definitions that could be resolved by making a definition more specific ("incomplete" errors). So your test case 2 seems to satisfy this condition and thus it could arguably be expected that it does note result in an error. However, in this case, that mechanism does not apply as comparison against bottom is considered completed. Maybe we can find a way to carry the potential incompleteness forward and not fail in this case as well. That would be a language change, but arguably an improvement and not very impactful from a compatibility standpoint.

So leaving this open for now.

[cueckoo]

Original reply by @myitcv in cuelang/cue#964 (comment)

Thanks, @mpvl - I've now wrapped my head around where my thinking was wrong. Your explanation above makes sense, and emphasises even more strongly the importance of #943.

[cueckoo]

Original reply by @kumorid in cuelang/cue#964 (comment)

@mpvl , Thanks for your post, it explains the behavior observed...
A different question is whether that behavior is the best one could hope for.

The value of isa is not just bool in test2: it is bool & a != |, where a != | evaluates rightfully to false. Note that the failure >
does not occur at d.valid, where a != | evaluates to true, but at #T.valid, where it doesn't.

But, an export is not interested in #T by itself, so, it is not clear to me why cue is behaving as if I wanted #T to be exported.

I suppose this is a consequence of the decision that a bottom produces a fatal error as soon as it shows up as the value of a field.

In that case, I would be very much in favor of acting as I believe you suggest in your last paragraph, as the present behavior is confusing when compared with how everything else behaves, and gives the impression that CUE's main property (irreversible constraints) is not preserved: the behavior observed seems to indicate that field isa goes from false in #T to true in d, because CUE makes the decision to abort execution because of that!

I assume the proposed builtin, must, does not produce such short-circuit behavior, so that I could use something like

-- test2.cue --
#T: {
  a?: int
  isa: bool
  isa: exists(a) 
  must(isa)
}

d: #T & {a: 56}

And get the expected output after cue export test2.cue

{
    "d": {
        "a": 56,
        "isa": true
    }
}

instead of an error at #T.