Compound values (⊗ vs &)

[gatlin]

In (linear) Call-By-Push-Value, there are two products:

• ⊗ , the "tensor product." This is, fundamentally, the force which binds arguments together in an ArgK continuation frame (defined in ceskm.ts); and
• &, the "cartesian" or "projective product."

In a symmetric monoidal closed category, the following holds true:

(A & B) ! ≅ A! ⊗ B!
     ⊤!   ≅ _

What this means in practice is that a data structure providing indexed access to some set of values amounts to a lookup function closed over an argument frame (or some union of them in a nested scope, it ends up working out the same).

This comes to mind because I want the machine to have basic support for manipulating any values that could be expressed as JSON. That seems only natural given my goal of producing a tool for pedagogical use, and also it makes sense to take advantage of existing tools and semantics where possible. Etc.

However, I don't want to over-complicate the semantics of the language or hastily make a decision I'll come to regret, over-specializing the machine where I don't need to.

My thinking is thus:

in JSON, arrays and objects are simply alternate notations for indexing and constructing heterogeneous compound products of other values.

Semantically, neither commits to an underlying representation; both may be thought of as unary lookup function (each with different requirements on their arguments).
Thus I am considering the following:

type Value
  = /* ... existing definitions ... | */
     { tag: "ObjectV"; v: { [key: string]: Value } }
   | { tag: "ArrayV"; v: Value[]  }
   ;

This wrapping scheme extends the language of Values for use by primops and formally imports the notion of JSON objects and arrays from the host language; at the same time this solution does not commit to any particular surface syntax for constructing, destructing, indexing, or otherwise transforming these values.