Better document which kind of cycles are solvable

[cueckoo]

Originally opened by @Ereski in https://github.com/cuelang/cue/issues/624

The documentation is inaccurate regarding which cycles are valid:

• https://cuelang.org/docs/concepts/logic/#cycles: does not imply any kind of limit on cycles as long as they are solvable, except for structural cycles for "Detection of structural cycles (an occurs check) is not yet implemented"
• https://cuelang.org/docs/references/spec/#cycles: states that "A field value of the form r & v, where r evaluates to a reference cycle and v is a value, evaluates to v." In light of #622, this is inaccurate. If I understand correctly, v should be a literal, not just any value?

[cueckoo]

Original reply by @mpvl in https://github.com/cuelang/cue/issues/624#issuecomment-752963799

If I understand correctly, v should be a literal, not just any value?

v can be any value, but a value, not an expression, which has distinct meaning in CUE (which is a consequence of CUE types and values being the same thing). So 2, string, >4, etc are all values. Without loss of generality, v can also be a reference to a value. But v cannot be s + w, where w is another value and s is an unresolvable reference, for instance if it resolves to a cycle. s+w is not a value.

In other words, there is no rewrite rule that will allow the cycle of #622 to be resolved.

I understand this can be confusing and this could indeed be explained better.

"Detection of structural cycles (an occurs check) is not yet implemented"

This is a documentation bug, actually: it now has been implemented.

[cueckoo]

Original reply by @Ereski in https://github.com/cuelang/cue/issues/624#issuecomment-752977701

@mpvl I'm sorry if I'm misunderstanding, but the issue with #622 is that all fields evaluate to a concrete value because X unifies to 5.0, so whether b0 or any other field is a cycle or a value is a matter of evaluation order (which, as I understand, should not influence the result). Even this errors out for example:

a0: X & 5.0
a1: a0 * 2
Y: a1

b0: Y
b1: b0 / 2
X: b1

My original comment here was incorrect. Basically, a0: X & 5.0 should evaluate to the concrete value 5.0 regardless of whether X is a cycle or not, correct? Which means a0 should be usable in a1: a0 * 2. a0 is not an unresolvable reference.

I think actually #622 should be reopened, because the following works as intended:

a0: X
a1: (a0 & 5.0) * 2
Y: a1

b0: Y
b1: b0 / 2
X: b1

So the following two snippets are not treated equally when they should:

a0: X & 5.0
a1: a0 * 2

and

a0: X
a1: (a0 & 5.0) * 2

[cueckoo]

Original reply by @mpvl in https://github.com/cuelang/cue/issues/624#issuecomment-752981980

a0: X & 5.0 is not the issue and could indeed evaluate if X ends up on a cycle. The problematic fields are a1: a0 * 2 and b1: b0 / 2, because a0 and b0 are cyclic.

Indeed evaluation order should not influence the result, so CUE should take care to always fail for such cases, even if the evaluation order makes it lucky and allows it to evaluate. With lazy binding, which CUE uses, one typically gets that for free.

But indeed, the second example succeeding is problematic. It should fail. I looked into a bit more and indeed the order can influence the result, which it should not. But both cases should always fail, instead of succeed.

CUE should not try to resolve these cases, btw, as it is potentially expensive (akin to backtracking). A nice property of graph unification is that it is nearly linear (similarly to how a hash lookup is near constant). Comprehensions and disjunctions break that property, but processing disjunctions can be made linear for pretty much all practical applications, and for comprehensions it is often syntactically obvious one is doing something expensive.

But indeed it should not succeed for some of these cases.

[cueckoo]

Original reply by @mpvl in https://github.com/cuelang/cue/issues/624#issuecomment-752982941

BTW, it is okay to break a cycle by providing a concrete value on the path of a cycle. In that case, as the expression cannot make the concrete value more concrete, it can be used as is. The expression is then postponed until after processing to verify that the end result is correct.

Ah, so indeed this should allow CUE to break the cycle in the example.

Either way, whatever it is there is something funky going on, so I'll reopen.

[cueckoo]

Original reply by @Ereski in https://github.com/cuelang/cue/issues/624#issuecomment-752985868

But both cases should always fail, instead of succeed

So that means that (a & b) + c where b and c are values is only valid in some cases, unlike a plain a & b?

CUE should not try to resolve these cases, btw, as it is potentially expensive (akin to backtracking)

As a pull-based solver it is indeed like backtracking. You mentioned lazy evaluation, so I assume that is the case. A push-based solver could do that linearly-ish though by noting which other fields/definitions become resolvable as others are solved.

Also I'm curious, why would graph unification be needed? Which graphs are being unified here?

[cueckoo]

Original reply by @Ereski in https://github.com/cuelang/cue/issues/624#issuecomment-752986525

BTW, it is okay to break a cycle by providing a concrete value on the path of a cycle

It's a bit of a pain to do that with my use case as my code has to go down an AST and do some rewriting. Just appending X: 5.0 would be much easier.

[cueckoo]

Original reply by @myitcv in https://github.com/cuelang/cue/issues/624#issuecomment-753778094

For anyone following this thread above, note that https://github.com/cuelang/cue/issues/622#issuecomment-752984071 followed @mpvl's comments above:

Ah, yes indeed. I stand corrected. There is an illegal cycle, but the 5.0 in

X: b1
X: 5.0 // this breaks the cycle and should allow CUE to resolve it.

should break it.

[myitcv]

The v0.5.x milestone is now closed because we have moved onto focus on v0.6.0. Hence moving this to v0.6.x. This particular issue is not critical to the release of v0.6.0, but completing it as a stretch goal would be good given the previous work on cycles.