ch:datatype-descriptions: ch:datatype-descriptions

Problem and result. Represent the six description constructors, elaborate the binary-tree layer, and run generic programs on the sample $$\mathsf{fork}(\mathsf{leaf}(1),\mathsf{leaf}(2)).$$ The accepted run maps both children, computes constructor size three, returns leaf list $[1,2]$, selects two different payload codes from dependent Sigma tags, and rejects a recursive occurrence in an arrow domain.

Representation. Use Desc for the six codes and one Value syntax for interpretation layers, Roll, recursive positions, and fold results. There is no separate concrete Tree. A result-returning elaborator maps the surface declaration to a code or reports a negative recursive occurrence. The executable Sigma specializes the printed tag type to Bool, encoded by natural tags zero and one:

data Desc : Type = One | Constant | Recursive
  | Sum Desc Desc | Product Desc Desc | Sigma Desc Desc

sigmaBranch : Nat -> Desc -> Desc -> Option Desc
let sigmaBranch tag falseCode trueCode =
  if tag == 0 then Some falseCode
  else if tag == 1 then Some trueCode else None

The two stored descriptions are the executable family $F(\mathsf{false})$ and $F(\mathsf{true})$. Every Sigma interpreter first runs sigmaBranch; the tag therefore determines the payload code rather than merely accompanying a payload checked against one fixed description.

Representation tradeoff. A concrete Tree plus separate layer and fold ASTs would make each individual function shorter, but its map, fold, and traversal could silently drift apart. The single Value representation is more explicit and requires runtime shape checks in Kappa; in return, the accepted treeCode drives construction and every generic program through the same interpreter.

First complete version. Implement elaborateLayer and elaborate. The good leaf/fork declaration returns a sum of a constant leaf and a product of two recursive positions. Construct the sample only in that accepted branch, with the returned code stored in each roll. The first end-to-end version needs only these cases:

treeDeclaration : SurfaceDecl
let treeDeclaration = Declaration Atom (PairTy RecTy RecTy)

leaf : Nat -> Value
let leaf n = Roll treeCode (LeftValue (ConstantValue n))

fork : Value -> Value -> Value
let fork l r =
  let fields = ProductValue
    (RecursiveValue l) (RecursiveValue r) in
  Roll treeCode (RightValue fields)

Validate the layer stored by each Roll against the code returned by elaboration before running a generic operation.

Remaining cases. Interpret the returned code to validate layers. Use the same interpreter for generic layer map, fold transformation and its size/leaf algebras, and effectful traversal. Send the bad arrow declaration through the same elaborator and require NegativeRecursiveOccurrence. Keep the fold generic by passing its algebra rather than selecting from a closed enumeration:

foldInterpretation : Desc -> (Value -> Option Value)
  -> Desc -> Value -> Option Value
fold : Desc -> (Value -> Option Value)
  -> Value -> Option Value

At a recursive position, recurse at the root code and wrap the result in RecursiveValue; at a Roll, transform its layer and pass that layer to the algebra. Define sizeAlgebra and leavesAlgebra as two functions of type Value -> Option Value. The Option traversal processes the left product field before the right and returns None when either effect rejects.

A failing version. If the arrow-domain clause keeps the incoming polarity rather than negating it, the named type Arrow RecTy Atom is accepted. The line negative recursive occurrence rejected changes to FAIL.

Acceptance test. Require all six PASS lines, the exact leaf order [1,2], the final recorded summary, and audit result []. For the Sigma code shown in the representation block, require tag zero with unit and tag one with two recursive values to pass. Require the crossed shapes and tag two to fail.

Mathematical boundary. The run illustrates elaboration to a finite regular Tree code and three generic programs over one representation. It is not an implementation of the whole MAG ISPT/SPF universe and does not prove description induction, the equality theorem, elaboration soundness, fold fusion, or the generic binding laws.