1. In CUE, types and values are equivalent and both live within the same lattice. You have a spectrum from the abstract to the concrete. See https://cuelang.org/docs/concepts/logic/ for a good overview. There are also definitions and structs, which have different semantics for closedness (ability to add fields). See https://cuetorials.com/deep-dives/closedness/ for an overview. One really interesting aspect of CUE is subsumption which can tell you if your types or API are backwards compatible.

2. Generally CUE is a turing-incomplete language, which means you cannot program. No user functions or lambdas by design. There are a number of utilities provided in the stdlib which are idempotent. It is not possible to maintain the guarantees of the language with user define functions. There are list and field comprehensions which are like a map. You can fold be simulated with comprehension. A proper fold could be added at some point.

1. The subsumption rule is elegant, but doesn't answer the pragmatic question: for what use-cases is a naive structural type system (familiar to a large population of developers) insufficient? Logic theory has type towers, but for 99% of the use-cases values and types are interesting, rarely kinds. Not even sure if 'type of kinds' has a name by itself. Possibly constraints are an answer, but the constraint system feels ad-hoc.

To rephrase, how would one describe Cue type system as a generalization of a naive structural type system?

2. Not sure what you mean by 'idempotent', perhaps 'pure' or 'no side-effects'? There is plenty of non-turing complete computations that can be done with pure functions.

I don't fully have my head around it either, but in my understanding you can have two mutually independent files that define `john: <constraint>` where <constraint> differs in each file, and in Cue these will be unified: the `john` value must satisfy both constraints.

For example, one file might have the constraint "john is an int" and the other "john is between 1 and 7". If the constraints clash (e.g., john is an int and john is a string), then it's an error.

That said, I think my disconnect is "when is this useful?" or "what can I do with this property?".

"When is this useful?" I can't comment on specific CUE design decisions, and speaking generally about data languages and not specifically about typing thereof.

A canonical use-case for data languages is a cloud deployment consisting of many almost identical items, e.g. k8 pods, described as a series of data templates with the the property that the cost of overriding any (shared) configuration parameter over the entire deployment is O(1).

In a standard function-based language this can be done by rewriting function arguments at runtime, i.e. some form of monkey patching. I haven't seen a good theoretical explanation on how data languages (GCL, jsonnet, CUE, etc.) avoid the monkey patching trap as opposed to embracing it with good terse monkey patching syntax & semantics.

Perhaps there is a there there, but until the basic evaluation semantics is clarified, I have little hope of grokking higher level concerns like typing.

I guess I don't have a good sense of the value of overriding a configuration parameter. If I were generating config in Starlark or Python, I would just provide the configuration as parameters to functions. If there's some function `def foo(): bar(x=4)` and I want to allow someone to change the value that is passed to bar.x, I would simply factor it out: `def foo(x=4): bar(x=x)`.

> In a standard function-based language this can be done by rewriting function arguments at runtime, i.e. some form of monkey patching. I haven't seen a good theoretical explanation on how data languages (GCL, jsonnet, CUE, etc.) avoid the monkey patching trap as opposed to embracing it with good terse monkey patching syntax & semantics.

I'm not entirely sure. I know you can arbitrarily layer on more constraints (e.g., you can impose your own naming conventions onto a Kubernetes Deployment "name" field by adding a `Deployment{name: <regex>}` constraint to your own files). But it's not clear to me how you would do other kinds of patches.

I think you are right. I see it as a form of multiple inheritance, a new one which no other language has.

It's called unification and exists in many languages, Prolog is a well known one. CUE is in the logical language family. It uses Typed Feature Structures which originated in NLP before deep neural networks became capable.

It is specifically not inheritance where overrides are allowed.

Sort of. Inheritance extends (hence the keyword of the same name) while constraints restrict (or constrain).

Inheritance also allows overrides, which is something CUE errors on. CUE has Go like embedding so you can reuse common schema or config.

CUE's constraints are in the "middle" of the spectrum (lattice, partially ordered graph) from abstract types to concrete data.

I'd draw the line at having two-way relations instead of functions. But I don't think this is the way CUE went, which is troubling.