design: principled type-level restriction for object-level constant bodies

[iljakuklic]

Background

code def x: T = body currently accepts an arbitrary object-level body. For Wasm codegen, it would be desirable to guarantee that the body is a closed literal value (a Wasm ConstExpr), so constants can be emitted as Wasm globals rather than zero-argument functions.

The natural candidate [[T]] (object-level code of type T) is too broad — it admits arbitrarily complex programs, not just values.

Idea

Find a principled type-level mechanism to restrict constant bodies to closed normal forms. Possible directions include:

• A dedicated value/ground type former (e.g. Val(T))
• Kinds or universe levels that distinguish value types from computation types
• A constraint or predicate on [[T]] that rules out non-value inhabitants

The right formulation should fit naturally into the existing 2LTT structure and ideally have grounding in the staged compilation literature.

Open questions

• What mechanism fits best with the existing kind/universe structure?
• How do cross-references between code defs interact (globals are currently stuck during NbE)?
• Is there a clean formulation in terms of existing 2LTT literature?

Current workaround

Object-level constants are emitted as zero-argument Wasm functions (see #73). This issue tracks the research needed for a principled language-level solution.