DataFrame as a Row-Parameterized Type Constructor (+ bool)

Status: Implemented (2026-07-09)

Goal: make df::* functions polymorphic over the row (record) type of the
data they process, and add a bool type so quoted predicates have a proper
result type:

fn df::fromcsv(path: string) -> DataFrame<'a>
fn df::filter(frame: DataFrame<'a>, predicate: Quote<'a -> bool>) -> DataFrame<'a>
fn df::show(frame: DataFrame<'a>) -> i64

The row type is learned from the quoted predicate: :( fn (r) => r.a > r.b )
has inner type fn {a: i64, b: i64} -> bool, which unifies with the frame's
row, so df::filter(df::fromcsv(p), :( fn (r) => r.a > r.b )) produces
DataFrame<{a: i64, b: i64}>.

Companions: knowledge/design/list-types.md (node lists cross the boundary),
knowledge/design/sum-types.md (row machinery used by the quote's record
selects).

Decisions (confirmed with user, 2026-07-09)

1. Naming: Frame is the boundary resource, DataFrame<'a> is the type
   constructor. The WIT resource data-frame is named Frame in blr
   source. DataFrame is always written with a type argument — there is no
   bare DataFrame. This avoids a bare/parameterized duality in Type and a
   LALR conflict in the type grammar.
2. WASM boundaries cannot carry the row parameter, so typed wrappers call
   underscored externs that take/return Frame. Two compile-time cast
   builtins bridge the two types (mantle-rewritten to identity, like
   to_nodes):
   • to_frame_resource : fn DataFrame<'a> -> Frame (erases the row)
   • to_dataframe : fn Frame -> DataFrame<'a> (asserts a row; the row is a
     promise about the data, verified by nothing — confined to std::df)
     User code cannot cast; only the std::df wrappers do.
3. Quote literals are lowered eagerly. :( expr ) becomes a node-list
   value at its definition site (the quote's only physical form is already
   the node list; today it is just built lazely under to_nodes).
   to_nodes becomes an identity rewrite that works on any Quote-typed
   argument (literal or parameter). This is what makes to_nodes(predicate)
   valid inside std::df's filter body, where the quote arrives as a
   parameter and its source payload is not visible.
   In emitted (mantle→core) types a Quote<T> parameter is physically
   list<node> (one i32 region pointer, same facts as List), because every
   quote value is a node list.
4. The quote reports its real solved inner type (not the sealed
   QUOTE_INNER_VAR). The isolated inner context defaults its leftover
   unbound unifiers before the type escapes: type unifier → i64, row
   unifier → empty closed row. This is what ties DataFrame<'a> to the
   predicate's record type.
   Superseded (2026-07-10, knowledge/plans/quote-row-superset.md):
   quote bodies are inferred in the enclosing context; a quoted
   predicate's parameter row is the fields it references plus an
   unknown remainder (row superset), body-local rows close to the
   observed fields at item end, and chained df::filter calls accumulate
   (DataFrame<{a,b,c,d}> for predicates over {a,b} then {c,d}).
5. fromcsv may be left unconstrained today (e.g.
   df::show(df::fromcsv(p))). No defaulting/source-function syntax in
   this plan — that syntax is a later item. Guardrail so the pipeline doesn't
   silently break: the row parameter is phantom for codegen and
   monomorphization — is_mono_type(DataFrame(_)) => true,
   emit_val_typ(DataFrame(_)) => I32 — a leftover Var inside the
   DataFrame parameter does not poison main.
6. bool scope: bool type, true/false literals, and comparison
   operators >/</= get scheme T -> T -> bool (currently T -> T -> 'b
   with unconstrained result). Deferred: &&/||/not, and a
   boolean(bool) node case in df.wit (a quoted predicate that is a bare
   boolean literal gets a clean "not encodable in the v1 node set" diagnostic).
7. show takes a frame (show(path: string) in the request was a typo
   for fromcsv).
8. Monomorph mangling of instantiated wrappers uses the existing
   field[(row-sexpr)] scheme (verbose now, terse later).

Type model

Type::Frame                  // boundary resource: WIT `own <data-frame>`, monomorphic
Type::DataFrame(Box<Type>)   // typed frame; parameter = row type (a record type in practice)
Type::Bool                   // new primitive

• Unification: DataFrame<A> ~ DataFrame<B> iff A ~ B (strict).
  Frame never unifies with DataFrame<_> — only the cast builtins bridge.
• The row parameter is phantom in codegen: a frame value is an i32 resource
  handle regardless of the parameter.
• Quote(Box<Type>) is unchanged structurally; its inner type is now real
  (solved, closed) instead of Var(QUOTE_INNER_VAR). QUOTE_INNER_VAR is
  deleted.

Syntax

Parser (lang/src/compiler/air/parser.lalrpop), TypeExpr region (~:279):

• "Frame" => TypeExpr::Frame (replaces the bare "DataFrame" production).
• "DataFrame" < TypeExpr > => TypeExpr::DataFrame(Box::new(<>)).
• "bool" => TypeExpr::Bool.
• Arrow types — no function-type syntax exists in type position today
  (TypeExpr::Fun is only produced by fn-decl signatures). Needed for
  Quote<'a -> bool>. Add a dedicated right-recursive nonterminal to avoid
  the LALR shift/reduce on a -> b -> c:

  TypeExpr: TypeExpr = { ..., ArrowType, ... }
  ArrowType: TypeExpr = {
      <param:TypeExpr> "->" <ret:ArrowType> =>
          TypeExpr::Fun(FunctionType { parameter_names: vec!["_"],
                                       parameter_typs: vec![param],
                                       ret: Box::new(ret) }),
      <t:TypeExpr> => t,
  }
  

  TypeExpr::Fun already lowers to nested Abs (_lower_typ), so no crust
  change beyond the new TypeExpr variants.
• Expression literals: "true" => Expr::Bool(true),
  "false" => Expr::Bool(false) in the Term rule.

Quote value model (the core change)

Today: a quote literal lowers to a Unit hole; to_nodes(quote-lit) is
rewritten in the mantle to a node-list literal built from the air payload;
the quote's reported type is sealed (Quote(Var(QUOTE_INNER_VAR))).

New:

1. infer arm for crust::Expr::Quote (infer.rs:268): the isolated inner
   check runs as today (check_quote_inner, fresh inner TypeInference), but
   after inner.unification the inner context defaults unbound unifiers
   (type → Int, row → empty ClosedRow) and the solved inner type is
   substituted out and reported: Type::Quote(solved_inner).
2. check arm for Quote (infer.rs:460): the inner check runs against the
   translated expected inner type; on success the arm re-emits
   Constraint::TypeEqual(id, solved_inner, *expected_inner) to the outer
   context. Without this, outer variables (the shared frame-row 'a
   instantiated at the filter call) would never learn the row, because the
   inner table's solutions don't cross the isolation boundary. (The primary
   call flow — quote literal as an inferred application argument — already
   works via (1), since the literal's solved type is closed; this arm covers
   quote literals in check position, e.g. under an annotated binding.)
3. Mantle lower_expr (crust::Expr::Quote arm, mantle/mod.rs:~1303):
   :( air ) → Expr::list(node_ty, quote::encode(&node_ty, air)) — always,
   not only under to_nodes. node_ty is extracted once from the registered
   to_nodes item type (same peel pattern as the existing rewrite,
   mantle/mod.rs:~1235). The v1-node-set panic in quote::encode becomes a
   proper diagnostic carrying the quote's node id (covers the deferred
   boolean-literal case).
4. Mantle to_nodes rewrite: to_nodes(x) → x for any argument
   (previously required a quote literal).
5. Mantle lower_ty: crust::Type::Quote(_) => Type::list(node_ty) — the
   physical type of any quote is the node list. Consequences:
   mantle::Type::Quote becomes unconstructible and is removed (adjust,
   subst_ty, sexpr arms go away); to_nodes's stored type lowers to
   list<node> -> list<node> (physically an identity); the monomorphized
   filter[row] wrapper's predicate parameter is emitted as one i32 (list
   region pointer) and the node-list value crosses the local/remote call
   exactly like a List value (single i32 on the blr stack; the
   pointer-pair canonical ABI only matters at AppExternal, where the extern
   signature is list<node> and already codegen-complete per
   list-types.md).
6. core: the mantle→core arm (core/mod.rs:341) becomes
   mantle::Type::List(..) => ... as usual — no Quote case needed since
   the mantle no longer produces it. Update the stale comment.

Why this is sound enough: a Quote<T> value is always a node list
(built from the quoted source); nothing else can produce one. Typing the
physical value as list<node> erases only the (uninhabited-at-runtime)
T tag. The row-typing benefit lives entirely at the type level, where
Quote<fn R -> bool> still unifies against the frame row.

Cast builtins

Registered in an ItemSource (new lang/src/runtime/df.rs, called from
run() in lib.rs alongside register_quote_functions), module std::df:

to_frame_resource : ∀'a. DataFrame<'a> -> Frame
to_dataframe      : ∀'a. Frame -> DataFrame<'a>

Mantle rewrite (next to to_nodes in lower_expr's Application arm, keyed
on symbol.field): the application lowers to its argument. Both directions
are the identity as values (an i32 handle).

New std::df surface

stdlib/wit/df.wit — rename the host functions (the typed wrappers need the
unmangled names for themselves); resource and node types unchanged:

fromcsv -> _fromcsv : func(path: string) -> data-frame
filter  -> _filter  : func(frame: data-frame, predicate: list<node>) -> data-frame
show    -> _show    : func(frame: data-frame) -> s64

stdlib/src/df.blr:

pub extern type binaryoperator = [ ... ]        // unchanged
pub extern type binary = { ... }                // unchanged
pub extern type function = { ... }              // unchanged
pub extern type node = [ ... ]                  // unchanged

pub extern fn _fromcsv(path: string) -> Frame;
pub extern fn _filter(frame: Frame, predicate: list<node>) -> Frame;
pub extern fn _show(frame: Frame) -> i64;

pub fn fromcsv(path: string) -> DataFrame<'a> { to_dataframe(_fromcsv(path)) }
pub fn filter(frame: DataFrame<'a>, predicate: Quote<'a -> bool>) -> DataFrame<'a> {
    to_dataframe(_filter(to_frame_resource(frame), to_nodes(predicate)))
}
pub fn show(frame: DataFrame<'a>) -> i64 { _show(to_frame_resource(frame)) }

stdlib/src/df.rs — bindgen!/Host impls renamed to _fromcsv/_filter/
_show; build_node_expr unchanged.

Flow for df::filter(df::fromcsv(p), :( fn (r) => r.a > r.b )):
quote literal infers Quote<fn {a: i64, b: i64} -> bool> (inner context:
r's row solves to {a: U1, b: U2} via the existing row-combination
machinery, > unifies U1 ~ U2, both default to i64); filter's shared
row unifier 'u := {a: i64, b: i64} from the predicate parameter and
flows from the frame parameter; main monomorphizes requesting
filter[{a:i64,b:i64}] and fromcsv[{a:i64,b:i64}] in std::df via the
existing cross-module instances machinery (same as +[(float)]). The
emitted call passes (i32 frame handle, i32 node-list region) to the
filter[row] function, which calls host _filter — the host code is
byte-identical to today's df::filter extern call.

bool

• Comparisons (runtime/binary.rs register_comparison_functions): scheme
  T -> T -> bool (drop the 'b var). No existing test uses comparisons
  outside quotes (runtime impls are todo!() stubs; binary_ops.blr uses
  only + - * /), so this is test-safe.
• Type::Bool plumbing is mechanical, patterned on Int at every
  Type::DataFrame/Type::List match site below, with these physical
  facts: core wasm i32 (ValType::I32), component bool
  (PrimitiveValType::Bool), size_align = (4, 4), flat [I32],
  literal emission i32.const 0/1.
• Expr::Bool(NodeId, bool) in air/crust; mantle/core get a matching
  literal variant (do not fold into Integer — different valtype).
• Not added in v1: ExternalType::Bool / boolean(bool) node case /
  && || not (see decision 6).

Touch-point map

air

• parser.lalrpop: Frame / DataFrame <TypeExpr> / bool / arrow
  ArrowType productions; true/false Term tokens; TypeExpr::Frame,
  TypeExpr::DataFrame(Box<TypeExpr>), TypeExpr::Bool; Expr::Bool.
  Run parser_tests.rs early (arrow rule is the main parser risk).
• air/mod.rs (143-169), air/sexpr.rs (To 270, From 881, test 1187):
  variants + (frame), (dataframe <inner>), (bool), (b <literal>)
  forms.

crust

• ty.rs: Type::Frame, Type::DataFrame(Box<Type>) (replaces
  Type::DataFrame), Type::Bool; occurs_check, mentions.
• unification.rs: normalize_ty (:148-171), unify_ty_ty arms
  (DataFrame(a)~DataFrame(b) recursive; Frame~Frame; Bool~Bool).
• inst.rs: Instantiate::ty (~:94-127).
• subst.rs: substitute_ty (121-150) + expr traversal.
• infer.rs: Expr::Bool infer + check arms; translate_ty arms; quote
  changes per "Quote value model" (1)-(2); delete QUOTE_INNER_VAR use.
• mod.rs: _lower_typ arms (DataFrame(Box) lowers its parameter;
  Frame; Bool); convert_to_ext_typ: Frame => ExternalType::Resource("data-frame"), DataFrame(_) => panic!("DataFrame row types cannot cross the component boundary; declare externs with Frame"); Expr::Bool in enum/id()/lowering.
• sexpr.rs: type To/From + allow-lists.

runtime registrations

• runtime/quote.rs: unchanged scheme; (doc updates).
• runtime/binary.rs: comparison scheme → T -> T -> bool.
• runtime/df.rs (new): to_frame_resource / to_dataframe schemes.
• lib.rs run(): register the new module.

mantle

• mod.rs: Type::Frame, Type::DataFrame(Box<Type>), Type::Bool
  (subst/shift/adjust/lower_ty/sexpr); lower_ty quote →
  list<node>; remove Type::Quote; Expr::Bool lowering; eager
  quote-literal arm; to_nodes/cast identity rewrites; node_ty() helper.
• monomorph.rs: is_mono_type — Frame | Bool => true,
  DataFrame(_) => true (phantom; decision 5).
• simplify.rs: subst_typ type arms; expr arms for Expr::Bool.
• quote.rs: encode panic → diagnostic; tests updated for eager
  lowering/identity.
• sexpr.rs: arms + allow-lists.

core

• mod.rs: Type::Frame, Type::DataFrame(Box<Type>), Type::Bool
  (295); lower_typ (341-357, incl. the quote comment);
  convert_external_type (701): Resource(_) => Type::Frame;
  Expr::Bool (+ free_vars_aux/rename/type_of); mantle→core expr arm.
• sexpr.rs: arms + allow-lists (42-81, 410-514, 842-881).

nucleus

• mod.rs: emit_val_typ (111: Frame | Bool | DataFrame(_) => I32);
  Expr::Bool literal emission (i32.const); size_align (Bool (4,4));
  flatten_type/core_flat_tys (Bool → [I32]); the list-element arm at
  392 and record/sum slot arms at 536/645/936 gain the new variants
  (DataFrame stays todo!()-parity in slots: no record/sum field may carry
  a frame in v1); emit_load/emit_store_expr Bool arms (i32).
• component.rs: convert_ext_ty_to_ctyp — Resource arm unchanged;
  EmitComponent::convert_ty_to_ctyp core-Type arms updated
  (Frame/DataFrame(_) stay todo!()-parity: frames never cross the
  root component boundary — main returns i64).

external_type.rs

• v1: no new variant (see decision 6). Resource("data-frame") unchanged.

stdlib

• wit/df.wit: function renames only.
• src/df.blr: per "New std::df surface".
• src/df.rs: Host impl renames; build_node_expr unchanged.

Test strategy

• Integration (lang/tests/integration/):
  • df.blr unchanged source; .out unchanged (0? — verify: currently
    returns the csv row count via show); WAT changes are expected.
  • df_filter.blr → df::filter(df::fromcsv("test.csv"), :( fn (r) => r.a > r.b )) (drop to_nodes); .out unchanged.
  • New df_chain.blr: df::show(df::filter(df::fromcsv("test.csv"), :( fn (r) => r.a > r.b ))) — row flows through two wrappers.
• Type check (lang/tests/type_check/):
  • New frame_row_mismatch.blr:
    df::filter(df::filter(df::fromcsv("test.csv"), :( fn (r) => r.a > r.b )), :( fn (r) => r.c < r.d )) → error (rows {a,b} vs {c,d} do not
    unify) — the first real negative test for row tracking.
  • New bool_type.blr style positive/negative checks (true : bool,
    1 > 2 : bool, bool vs i64 mismatch).
• Unit: parser tests (arrow type, DataFrame<'a>, Frame, literals);
  sexpr roundtrips per layer; quote::encode diagnostic test;
  is_mono_type DataFrame facts.
• Snapshot WAT audit (BLR_SNAPSHOT + print_wasm example):
  • main passes (i32 frame, i32 node-list region) to the mangled
    filter[(prd ...)] function in the std::df core module.
  • std::df module calls the lowered host _filter import with the
    pointer-pair list lift (existing machinery).
  • to_dataframe/to_frame_resource leave no trace (identity rewrites).
• Gates: full workspace green, cargo fmt,
  cargo clippy --workspace -- -D warnings; existing expect-test snapshots
  (crust/mantle sexpr, monomorph test in monomorph.rs:315+,
  quote.rs:149+) get bulk-updated — review diffs for sanity, not
  byte-for-byte.

Work items

D1-D4 are mechanical (the list-types.md arm census is the template); land
per layer as today. D5 is the only genuinely new mechanism. D7/D8 depend on
D5.

Risks

• Arrow-type grammar: new -> in TypeExpr position next to existing
  -> in fn-decl position and the >> forward token — the dedicated
  right-recursive ArrowType rule is the mitigation; land D1 and run
  parser + precedence tests first.
• Quote check-arm information flow: if the TypeEqual(solved, expected)
  re-emit is missed, rows silently fail to unify in check-position quotes —
  covered by the df_chain and frame_row_mismatch tests.
• DataFrame(Var) in main: the phantom guard (decision 5) keeps
  unconstrained fromcsv alive; without it main would be classified poly
  and dropped as dead code (monomorph.rs:76-80). The real fix (source
  function syntax) is deferred.
• Node list crossing local/remote item calls: single-i32 region values
  through LocalItem/RemoteItem calls are untested territory (lists
  today only cross AppExternal). The WAT audit in D8 is the gate; fallback
  if broken: emit filter[row] bodies with the list argument stack-allocated
  like other i32 params (expected, since emit_val_typ(List) = I32 already).
• Snapshot churn: every layer's expect-test snapshots touching
  DataFrame/Quote change; budget review time.

Progress log

• 2026-07-09: Plan written from repo survey (crust/mantle/core/nucleus
  touch points, quote isolation mechanics, monomorph instance machinery,
  list/quote physical facts). Decisions 1-8 confirmed with user.
• 2026-07-09: Implemented across five commits on the quote branch:
  1. bool type, true/false literals, comparisons T -> T -> bool
     (D1/D2/D3/D4/D6).
  2. Frame boundary resource + DataFrame<row> constructor, arrow type
     syntax (D1-D4).
  3. Quote value model: real solved inner types, eager node-list lowering,
     to_nodes/cast identity rewrites, runtime/df.rs cast registration
     (D5).
  4. Typed std::df wrappers (D7) plus the mechanisms that proved
     necessary (see deviations below).
  5. Tests: df_chain integration, frame_row_mismatch / bool_type /
     bool_mismatch type-check cases (D8), WAT audit.

Deviations from the written plan

• Boundary WIT names are readcsv / applyfilter / count, not
  _fromcsv / _filter / _show: WIT identifiers cannot start with
  _, and BLR identifiers cannot contain - (WIT is kebab-case), so the
  host functions must be single words. The blr externs match them
  verbatim (no name mapping at the boundary).
• mantle::Type::DataFrame was deleted rather than kept: with the
  identity cast rewrites, a DataFrame-typed value passed where Frame
  is expected tripped the mantle's application type-check. Lowering both
  crust::Type::Frame and crust::Type::DataFrame(_) to the single
  mantle Frame type is simpler and consistent with the row being
  phantom; the row still flows through monomorphization via the wrapper
  TypApp (mangled names carry the row sexpr).
• Quote row-closing needed a new mechanism: the row-combination solver
  does not merge complementary single-field projections (r.a and r.b
  produce two partial combinations on the same goal row that are not
  unifiable under the existing two-out-of-three rule), so a quote
  parameter's row stayed an open variable. TypeInference::close_unbound_rows
  (isolated quote contexts only) closes pending combinations whose goal is
  still unbound: goal := union of the closed left rows, each right :=
  goal minus its left.
  Superseded (2026-07-10): close_unbound_rows now runs in the main
  context at item end with a reachability filter — only body-local goals
  close; signature-reachable rows stay open (row-polymorphic items keep
  their row and carry the predicate's row equations as evidence).
  Quote-context isolation itself is gone (quote bodies infer in the
  enclosing context); liveness of monomorphic items is guaranteed by
  scheme hygiene (only interface-named variables quantify an item), not by
  closing.
• The phantom guard needed a second half: is_mono_type(DataFrame(_)) => true
  alone does not keep an unconstrained show(fromcsv(p)) alive — the free
  row variable leaks into the item scheme via the item wrappers, making
  main vacuously polymorphic (∀a. () -> i64) and dropped. Added
  TypeInference::default_body_local_ty_unifiers (main context): unbound
  type unifiers not reachable from the signature type (following solved
  unifiers) are defaulted to Int after unification. Reachable unifiers
  are preserved (the S combinator's inferred b is reachable through a
  solved parameter unifier).
• Monomorph instance dedup: the same poly item instantiated at the
  same type from several call sites (e.g. two filters at the same row)
  produced duplicate exports; instance recording now dedups by type.