Please document the term "ground value"

[Nuru]

The documentation (also https://www.openpolicyagent.org/docs/latest/policy-performance/#early-exit-in-rule-evaluation) refers to "ground value": https://github.com/open-policy-agent/opa/blob/82433595385140b4d93d1d03873de57962563e9f/docs/content/policy-performance.md?plain=1#L141-L142

https://github.com/open-policy-agent/opa/blob/82433595385140b4d93d1d03873de57962563e9f/docs/content/policy-language.md?plain=1#L388-L390

Nowhere can I find a definition of "ground value", so I am not sure what the above mean. A search on "ground value" turns up those usages, but no definition.

I find the phrase "rules that only have one, ground value" awkward. Is that trying to say "rules that have only one value, and that value must be a ground value"? If so, I don't have a better suggestion right now, but if that is not what it means, then a clearer explanation is needed.

I really do not understand "variables inside sets must be unified with a ground value outside of the set". How is a variable "unified" with anything? A search on "unified" brings up things like:

• Distributing policy, retrieving status, and storing logs in the same way across all OPAs provides a unified management plane for policy across many different software systems.
• OPA also gives you a unified toolset to decouple policy from any software service you like....

but nothing relevant to variables being unified.

---

I am not asking to have these things explained to me here in this issue. What I am asking for is to have the documentation enhanced to have a definition of "ground value", and for the documentation on sets to have a reference (link or footnote) to the explanation of what it means for a variable to be unified. It would also be nice to have the example about sets requiring a unified variable expanded to show a success case; right now it only shows the error case when a variable has no value assigned.

[srenatus]

"Unification" and "ground values" are "logic language" that isn't really approachable, and shouldn't hinder understanding the docs... So, sorry about that! I suppose one way forward would be to add a glossary, or link to the wikipedia pages for the relevant terms... In this case, it's https://en.wikipedia.org/wiki/Unification_(computer_science) and https://en.wikipedia.org/wiki/Ground_expression#ground_term

[anderseknert]

Adding a short explanation where those terms are used, along with wikipedia links, seems like a good way forward. Adding good-first-issue label.

[Nuru]

Thank you for considering my request.

Unfortunately, neither of the Wiki articles are particularly helpful.

The unification article is far too long and dense for me to want to slog through, and even after the slog, I don't know what constitutes a variable that is "unified with a ground value outside of the set" in Rego.

The Ground expression article defines ground term, ground atom (a.k.a. ground predicate or ground literal), and ground formula, but not ground value. You may say that "ground value" is the same as "ground term", but I would not assume that given the careful distinctions being made between ground term and ground atom, for just one example. Furthermore, even after reading that and assuming that "ground value" means something like ground term, I do not understand what is meant by "A set of (complete document|function) rules that only have one, ground value". What does it mean for a rule to "have a value" or for a set of rules to have "one" value? In my mind, if something only has one value, then it is a constant, which is surely not what the author meant. Most of the documentation is, thankfully, written in a way understandable to anyone familiar with common computer programming terminology, so please do not expect readers to have a Master of Computer Science degree.

(In the example in the documentation, allowed can be either true or undefined. I guess the argument is that "undefined" is not a value, so allowed can only have one "value", true, but does that mean if I add default allowed := false to the example, it no longer qualifies for early exit? I do not see why it should.)

I think the documentation tried to answer my question about ground value, but failed by changing the terminology: https://github.com/open-policy-agent/opa/blob/82433595385140b4d93d1d03873de57962563e9f/docs/content/policy-performance.md?plain=1#L162

If you change this to something like:

Informally, by "ground value" we mean anything that does not have or depend on a variable. For a formal definition, see ground term

that would at least take care of the "ground value" reference in this section of the documentation.

[anderseknert]

All good input @Nuru 👍

Whether it's right or not, I've always thought of "ground" as known, and replaced it internally with that. So, this rule...

allow := true {
   ...
}

...would have a ground value, while this rule wouldn't...

allow := var {
    ...
    var := ...
}

Unification OTOH, kinda is different from what people are mostly familiar with from other languages, and not just a word that can be replaced by something more familiar. Since Rego also provides a unification operator (=), the concepts is explained to some degree elsewhere in the docs: https://www.openpolicyagent.org/docs/latest/policy-language/#unification-

Basically, when saying something like:

x = 5

x can either be an "input" (for comparison to five) or an "output" (assigned the value 5) depending on if it's previously defined. Rego uses unification extensively, even when not using the unification operator explicitly.

[srenatus]

To add just a tiny bit here -- unification is a very powerful feature, but you might not need it every day, or ever, for simple policies. There are always ways to write the same policy without explicitly using the unification operator. But also, it allows for succinctly expressing complex matches, like

test := x {
    a := "A"
    {"a": a, "b": {"d": x}, "c": [c, c, c]} = input
}

👉 playground

[Nuru]

@anderseknert @srenatus Thank you for the extra explanation. However, please remember that the only reason I care about unification is because, with regard to set equality, the documentation says:

Because sets are unordered, variables inside sets must be unified with a ground value outside of the set. If the variable is not unified with a ground value outside the set, OPA will complain.

and I want to know what that means. I do not so much want to know the details of unification as I want to know what do I need to do to make variables inside sets work. Apparently, this means that I cannot get OPA to fill in the value when it is inside a set:

Works:

cc := x {
  3 = x 
}

Does not work:

cc := x {
  {1, 2, 3} = {1, 2, x}
}

If the documentation would explain this without reference to "unification", that would address my concern here.

[srenatus]

Unifying sets is tricky:

{1, 2, 3} = {x, y, z}

This would have 6 valid assignments of 1, 2, 3 to x, y, and z. Your example makes it look simple! 😅 But it really isn't simple for many cases, so OPA doesn't attempt to do it.

To paraphrase your quote, variables cannot become set by unifying two sets.

This is supported:

x := 3
{1, 2, 3} = {1, 2, x}

This is not:

some x
{1, 2, 3} = {1, 2, x}

But in real life, this restriction really never bit me -- does it block something you're trying to do? Happy to discuss other ways the approach the problems you might be having.

[stale[bot]]

This issue has been automatically marked as inactive because it has not had any activity in the last 30 days. Although currently inactive, the issue could still be considered and actively worked on in the future. More details about the use-case this issue attempts to address, the value provided by completing it or possible solutions to resolve it would help to prioritize the issue.