# J-core: common witty expressions

Design proposal · 2026-10-14

J-core is a proposed standalone Rust crate defining an expression-based HIR for data transformations and first-class functions. Its authoring model supports structural constraints and polymorphism; its resolved instances use nominal type identities. **Specialization is the boundary between a structural requirement and an exact nominal contract.** Its first consumers would be nix-wit and the functionally composable parts of Perry-WIT. A small optional syntax implementation makes the HIR usable independently of either compiler.

The shared core ends at **evaluation-strategy elaboration**. It describes expressions, lexical scope, structural requirements, nominal instances, possible effects, numerical contracts, and explicit continuations. Its consumers decide how expressions become eager computations or shared lazy computations. Allocation, closure conversion, stack representation, scheduling, canonical ABI marshalling, and Wasm emission follow that boundary. Type specialization can establish a precise contract before that handoff; specialization based on demand or physical representation belongs after it.

This document specifies a proposed design, not existing functionality. `j-core` is a working package name; registry availability remains to be checked.

## Purpose

Share the semantics and analysis of transformations such as:

```text
input document
  → select nested records
  → map a supplied function over their fields
  → construct a structurally typed result
  → pass it to a supplied continuation
```

The useful commonality is richer than JSON itself. JSON supplies recursive scalar, array, and object data; the core also needs functions, variants, absence, recursive schemas, numerical domains, and failure information. Functions are ordinary typed values inside the HIR. JSON encoding is a separate boundary with an explicit policy for values JSON cannot represent.

The primary proof of usefulness is one transformation expressed through both consumers, analyzed by the same implementation, with duplicated structural inference or rewriting removed from those consumers. Matching type names or wrapping two existing solvers is insufficient.

## Semantic boundary

An expression graph does not determine an evaluation strategy by itself. Consider:

```text
bind unused = fail("unused") in 42
project(record(answer = 42, other = loop()), answer)
```

An eager interpretation can fail or diverge where a demand-driven interpretation returns `42`. Failure and divergence matter even without mutable state or I/O.

Consequently, J-core describes a family of interpretations with common typing and structural laws. It preserves enough information for each consumer to select its interpretation. It does not claim that every accepted term has the same observable behavior in JavaScript and Nix.

The cross-language portable subset has stronger obligations: terminating, effect-free computations; compatible scalar operations; no observable identity; and compatible data-boundary behavior. Terms outside that subset can still share the HIR while retaining distinct host semantics.

| Inside J-core | Resolved by the consumer after J-core |
| --- | --- |
| Binding identity, lexical scope, expression occurrences | When a binding is evaluated |
| Argument, field, and element expressions in source order | Which expressions are demanded, in which order |
| Function bodies, recursive definitions, captures | Closure environments, application convention |
| Typed continuations and explicit transfers | Stack frames, resumption storage, scheduling |
| Potential effects, divergence, dependency relationships | Observable effect traces and effect execution |
| Structural requirements, nominal instances, numerical policies | Runtime tags, carriers, layout, memory management |
| Checked external operation signatures | JSON codecs, host calls, WIT marshalling |

A source frontend retains its evaluation contract beside the HIR. Syntax selection is not an implicit runtime policy. Changing a module from eager to lazy is a semantic change, not an optimization flag.

## Crate shape

Publish one library with a small public surface:

| Module | Responsibility |
| --- | --- |
| `hir` | The pliron dialect, typed construction, borrowed inspection, verification |
| `types` | Nominal definitions, structural requirements, type schemes, effect rows |
| `infer` | Scope checking, compatibility proofs, generalization, instance resolution |
| `rewrite` | Transformations valid before evaluation strategy is chosen |
| `syntax` | Optional parser, printers, source spans, diagnostics |

The crate accepts source bytes or programmatic builders and returns owned compiler data and structured diagnostics. Consumers supply named imports and their contracts. Filesystem acquisition, module discovery, environment access, logging, and process execution belong to callers.

Use pliron as the sole persistent HIR representation. A short-lived syntax tree is reasonable; a second permanent graph mirroring every pliron operation is not. Nominal definitions and their instances use compilation-local interned identities, keyed by definition identity and resolved arguments. Structural requirements refer to the same type graph. Expression occurrences retain their identity even when their shapes match.

Public construction validates operations and makes unresolved versus resolved modules distinct states. Resolved modules may contain explicitly bound type variables in polymorphic schemes; they contain no unsolved inference metavariables. Consumers receive read-only views and deliberate mutation APIs rather than public internal collections.

The published crate must have registry-resolvable normal dependencies. A development Git revision of pliron is not by itself a publishable dependency contract. Qualify the required APIs against a released pliron version before publishing; keep the compiler integrations outside J-core's dependency graph. Cargo documents the relevant publication constraints.[9]

## HIR representation

### Expression regions

Use a high-level pliron dialect with **graph regions**, lexical scopes, and explicit region results. Operation results at this level denote typed expressions, not evidence that a runtime computation has executed. A conceptual `Expr<T, E>` means “an expression producing `T`, with potential effects `E`.”

Preserve the following expression forms:

| Form | Meaning |
| --- | --- |
| Literal, reference | Scalar literal or hygienic reference to a binding |
| Record, list, variant | Logical construction from member expressions |
| Projection, selection | Static member access or checked dynamic selection |
| Functional update | A new record expression with specified fields replaced |
| Lambda, application | First-class code and application to expression arguments |
| Binding group | Lexical names, definitions, body, explicit recursive visibility |
| Conditional, match | Alternative expression regions selected by a condition |
| Primitive | Resolved operation identity, semantic contract, operands |
| Continuation, transfer | Explicit code destination and tail-position transfer |

Binding references identify one source binding. Two occurrences of `f(x)` remain two occurrences until an equivalence proof permits merging them. HIR node interning must not silently become runtime memoization. Intern immutable types and constants freely; share computations only through explicit binding identity or justified rewriting.

Store argument and construction order independently of compatibility checks. Structurally compatible record definitions can have different source field orders and distinct nominal identities. A field lookup used to prove compatibility cannot erase information needed by downstream evaluation or enumeration.

Recursive groups use finite identities and verified back-edges. Lexical visibility is explicit: Nix's recursive bindings and a JavaScript binding's initialization rules cannot be conflated merely because both are called `let`.

### ANF placement

Ordinary administrative normal form makes sequencing explicit. Rewriting a nested expression into eager `let` operations would cross the proposed boundary too early.

J-core may give expressions stable names for analysis, but those names carry no evaluate-now meaning. Actual ANF, CPS, or executable SSA is produced **after** the consumer selects evaluation semantics. This refines the initial idea of an ANF-based shared HIR: lexical naming is useful at the shared level; operational sequencing belongs below it.

Pliron supplies graph and SSACFG region kinds. Graph regions still require J-core's lexical, recursive-binding, and expression-use verifier. Generic SSA dominance is not a substitute for those rules.[3]

## Type model

The common type vocabulary contains:

- Null, Boolean, text, numerical domains, and explicit absence where admitted.
- Nominal definitions for immutable records and variants; homogeneous lists; tuples; structural requirements with closed or open rows.
- Functions with parameter types, result types, and latent effect rows.
- Finite recursive definition identities and quantified type, row, and effect variables.
- Opaque host identities where a boundary needs resources or references.

An open record transformation can have this type:

```text
mapValue : ∀A B R E.
  (A → B ! E) → { value: A | R } → { value: B | R } ! E
```

`R` preserves fields unrelated to `value`; `E` tracks effects potentially introduced by the callback. The row must exclude a second `value` field. Record rows and effect rows have different laws and must not be unified merely because both are called rows.

The signature above is a generic requirement. Applying it resolves the actual input definition, its fields, and a nominal result instance. Structural compatibility permits composition without making every matching record definition the same type.

Types specify admissible values. Inferred domains can retain narrower numerical or field facts. Neither fixes memory layout. An immutable record also differs from a mutable object with the same fields: Perry must prove a value view is valid, take an explicit snapshot, or retain an opaque reference with effectful access.

### Nominal identities

Give each record, variant, and recursive definition a stable identity within the compilation. Anonymous records receive compiler-generated definition identities; they need no source-level names. Transparent source aliases resolve to their target identity. Explicit brands and opaque declarations retain their own identity.

An instance is identified by its definition and resolved type arguments. Reserve recursive identities before resolving their members, and reuse them on recursive references. Equality of resolved types is identity equality. Structural compatibility is a separate, memoized proof over required and supplied members, including recursive pairs when needed.

The core does not require global minimization of equivalent recursive type graphs. Canonicalize instance keys and substitutions so repeated requests reuse an instance; independently defined recursive structures may remain distinct even when a compatibility proof succeeds. Display names are diagnostic labels, not interning keys.

Three relationships stay separate:

| Relationship | Rule |
| --- | --- |
| Resolved type equality | Same nominal definition and resolved arguments |
| Generic applicability | Actual type satisfies the structural and effect requirements |
| Runtime object identity | Preserved according to the consumer's aliasing and mutation semantics |

### Specialization boundary

Resolve a generic operation against the caller's actual nominal types. The resulting instance uses exact parameter, field, result, and continuation contracts. Ordinary operations inside that instance can use direct identities and resolved member references rather than repeatedly searching for structural matches.

For example, in HIR notation:

```text
nominal A = { value: s32 }
nominal B = { value: s32 }

getValue<T where T has { value: s32 }>(input: T) -> s32
  = input.value

getValue<A> : A -> s32
getValue<B> : B -> s32
```

Both calls are valid while `A` and `B` remain distinct. Specialization resolves the projection against each definition; it requires no record copy, runtime type test, or conversion from `B` into `A`. A frontend can translate a structural source parameter into this kind of requirement while preserving the source language's acceptance rules.

Structural equality and width compatibility are separate obligations. A read-only function requiring `value` may accept an instance with additional fields, subject to its effect contract. Mutable views must validate permitted writes and preserve aliases. An explicitly nominal parameter or opaque resource cannot be bypassed merely by matching its fields; a fixed ABI requiring another representation needs a checked boundary adaptation.

Use one instance cache keyed by the generic definition, actual nominal arguments, required result contract, and relevant semantic policies. Keys exclude individual runtime values and analysis traversal order. Recursive calls reuse matching instances. Unbounded polymorphic growth must receive a diagnostic or a sound generic representation, never silent type erasure.

An instance identity does not require immediate code duplication. Retain a shared body with substitutions until materialization is useful. Later code sharing requires equivalent semantics and calling representations; structural similarity alone is insufficient. This keeps nominal specialization useful without making one machine function per nominal record a requirement.

The same boundary applies to callbacks and continuations: instantiate their parameter, answer, and effect contracts consistently. Type specialization preserves expression occurrences, source binding identities, and unresolved evaluation behavior. Decisions that require eager sequencing, forcing, layout, or allocation remain in consumer lowering.

### Let-polymorphism

Generalization permits a binding such as identity to carry `∀A. A → A`. Each use instantiates fresh type variables, so one binding can accept both an integer and a record while preserving the input/output relationship. Constraint solving then resolves applicable nominal instances. Instantiating a type scheme and materializing specialized code are separate decisions.

Koka's formal treatment uses effects to control generalization; its displayed rule requires an effect-free bound expression. A shared mutable cell cannot safely become independently polymorphic at each use. Constructing a lambda is distinct from running its potentially effectful body.[1]

J-core starts with rank-1 schemes. Generalize only variables absent from the environment, after checking the binding's generalization eligibility. Recursive groups are checked monomorphically during inference, then eligible bindings are generalized. Higher-rank schemes and inferred polymorphic recursion are separate extensions.

Host references, unresolved effects, or uncertain eligibility conservatively prevent generalization. A lazy binding is not automatically eligible just because its computation has not run yet. A continuation capturing a monomorphic cell cannot generalize that cell through its own parameter scheme.

### Numerical contracts

Retain literal spelling until its numerical meaning is resolved. Record signedness, semantic width, exceptional alternatives, and the arithmetic policy independently of a future machine carrier.

An operation's identity includes its policy: fixed-width wrapping addition, IEEE addition, and a host's dynamic addition are different operations. The syntax `+` is resolved using the supplied language contract; matching punctuation does not establish matching arithmetic.

Preserve integer versus floating distinctions, negative zero, NaN, infinity, and overflow behavior where admitted. Wider-result constraints and explicit narrowing points are semantic facts supplied or resolved before arithmetic rewrites rely on them. J-core's initial structural inference need not reproduce Perry's entire representation solver.

### JSON boundary

Model dynamic JSON as a recursive data schema and typed JSON as a checked conversion into a schema. Preserve numeric tokens long enough for the selected integer or floating contract; do not make a floating number the universal intermediate representation.

Parsing, serialization, duplicate-key handling, field ordering, absence, Unicode, and exact integer behavior belong to explicit codec contracts. J-core can type calls to these operations without shipping either consumer's parser or runtime. A function, opaque reference, or exceptional number is not automatically JSON-serializable.

## Continuations

A continuation is an explicit typed destination for the rest of a computation. It can be represented before deciding how the producer is evaluated.

Use a logical signature:

```text
Cont<A, R, E>
```

It accepts a supplied `A`, ultimately produces the enclosing answer `R`, and has latent effects `E`. It has an explicit lexical environment and answer scope. Its code uses the same region representation as a function; a second function-body IR is unnecessary.

The minimal operations are continuation construction and **tail transfer**. Ordinary functions return to their callers. Transferring to a continuation does not introduce an additional return point at the transfer site. Branches can transfer into a shared typed join, and an explicitly passed continuation can compose another transformation.

For example, in HIR notation rather than either surface language:

```text
transform(document, finish: Cont<Output, R, E>) =
  continuation forward(value: Output) answers R ! E:
    transfer finish(value)
  ... produce an Output expression for forward ...
```

The ellipsis deliberately leaves producer evaluation unresolved. This describes a destination and its type, not a rule for when `document` or its fields are forced.

Continuation verification covers parameter/result compatibility, lexical capture, answer-scope escape, and invocation permission. Explicitly constructed continuations with duplicable captures may be reusable; imported one-shot destinations are affine. The permitted use follows the contract and captures, rather than silently treating every continuation as reusable. Affine destinations require linear-use checking through aliases and branches.

A scoped continuation cannot escape its answer scope. An escaping continuation must have an independently valid environment and answer contract. Whether that requires a heap allocation is a later decision.

This is enough to describe higher-order pipelines, joins, success/error destinations, and the destination of a future suspension. It does not capture the current dynamic stack. Delimited capture, effect handlers, promise execution, cancellation, stack cloning, and memoized resumption require further semantics in the consumer. An ordinary reusable explicit continuation is not a license to replay a captured mutable stack.

Keep continuation support available through the HIR builder initially. Surface functions can express explicit continuation-passing programs without introducing dedicated keywords. Full effect-handler syntax is outside the minimal parser.

Call-by-push-value provides a useful account of the distinction between values and computations, including translations of eager and call-by-name languages and treatment of control effects. It does not by itself supply Nix's call-by-need memoization.[2]

## Minimal syntax

### Shared fragment

A useful expression fragment already parses in both languages:

```text
compose(double)(readCount)(document)
```

With corresponding bindings, this exact expression was evaluated with JavaScript and Nix during preparation of this note and returned `42` in both. In JavaScript the parentheses express curried single-argument calls; in Nix each parenthesized expression is an application argument.

Use the common fragment for names, restricted scalar literals, parentheses, field selection, single-argument application, and compatible operators. Restrict identifiers, string escapes, and literals to a documented intersection. Reject interpolation and implicit coercion in the portable profile.

A substantial language with literal lambdas and records cannot be a literal subset of both. Nix writes `x: body` and `{ field = value; }`; JavaScript writes `x => body` and `{ field: value }`. Conditions and multi-element lists differ too. Avoid hiding these differences behind preprocessor tricks.[6][7]

### Syntax profiles

Ship one small parser with two explicit profiles sharing its binding, type, and HIR implementation. The profiles adapt notation, not evaluation strategy.

The JavaScript profile accepts expression-bodied arrows and object expressions:

```javascript
row => ({
  title: row.title,
  doubled: row.count * 2
})
```

The Nix profile accepts the corresponding lambda and attribute set:

```nix
row: {
  title = row.title;
  doubled = row.count * 2;
}
```

Both examples were evaluated against `{ title = "Demo"; count = 21; }` or its JavaScript counterpart and produced the same field values. Their printed object order differed, illustrating why serialization equivalence needs its own contract.

Keep the initial syntax inventory small:

| Construct | JavaScript profile | Nix profile |
| --- | --- | --- |
| Lambda | `x => expression` | `x: expression` |
| Record | `({ a: x, b: y })` | `{ a = x; b = y; }` |
| List | `[x, y]` | `[ x y ]` |
| Conditional | `p ? x : y` | `if p then x else y` |
| Application | `f(x)(y)` | `f(x)(y)` |
| Projection | `record.field` | `record.field` |

For Nix lists, preserve the language's element/application grammar rather than parsing every whitespace sequence as an application. The JavaScript profile excludes `this`, prototypes, getters, mutation, and coercive operators unless the consumer provides a separate contract.

The initial text format can be a single expression with imports supplied through the API. Explicit local binding groups, recursive groups, and advanced row operations remain expressible through the HIR builder; add surface notation when there is a concrete authoring need. Curry multiple arguments instead of inventing a third calling syntax.

The syntax parser returns spans and a source profile. Numerical contracts, import signatures, and the eventual eager/lazy interpretation are supplied explicitly. A parse/print round trip preserves the profile; printing the other profile is a checked source translation, not a promise of behavioral equivalence for arbitrary programs.

## Safe shared analysis

The common layer supports structural constraint solving, nominal instance resolution, recursive compatibility proofs, callable-target facts, projection typing, and potential-effect propagation. Cache applicability at the specialization boundary; resolved member references carry the result into the body. These are useful before layout and evaluation decisions.

Potential effects describe what a subexpression can do **if evaluated**. A record can contain a failing field without record construction necessarily triggering that failure under every interpretation. Keep latent member facts and dependency relationships; flattening them into one unconditional executed-effect set loses the information needed at the boundary.

An unknown external operation remains conservative. A function's declared purity is an obligation to validate or a trusted import contract, not evidence manufactured by the optimizer.

Rewrites must be valid under every supported interpretation of the unresolved graph. Examples include hygienic renaming, type substitution, literal operations with fixed semantics, and structural projection when discarded members are proved total and effect-free. Preserve identity-sensitive behavior and divergence.

| Tempting rewrite | Required proof before evaluation elaboration |
| --- | --- |
| Discard an unused binding | Its evaluation can have no observable effect or divergence |
| Project one field from a constructed record | Discarded fields are harmless under eager interpretation |
| Substitute an argument into a lambda body | Substitution preserves demand, multiplicity, effects, termination, and capture |
| Merge equal-looking calls | Evaluation identity and invocation count are unobservable |
| Reassociate arithmetic | The numerical contract permits it |

Partial evaluation and aggressive optimization can become more permissive after the host interpretation is fixed. Avoid making the shared stage carry duplicate strictness solvers just to emulate that later knowledge.

## Infrastructure reuse

The proposed HIR is a pliron dialect, not an e-graph. Pliron provides interned type infrastructure, operation use-def relationships, regions, verification hooks, traversal, and rewriting. J-core supplies structural compatibility, nominal instance resolution, lexical rules, effect meaning, and continuation contracts.[3][4]

Algorithm reuse depends on representation. Pliron's pinned SCCP implementation explicitly lacks region-branch interface handling. Its CFG algorithms therefore cannot simply be applied to arbitrary functional graph regions. SCCP, CFG simplification, executable liveness, and Mem2Reg become applicable after suitable lowering; using their pass manager earlier is framework reuse, not reuse of those algorithms.[3]

An e-graph can be an optional optimization tool for eligible expression fragments. Equality classes are not lexical binding identities or shared lazy cells. The default package need not depend on `egg`.[8]

The inspected nix-wit implementation demonstrates this separation: its primary `ProgramGraph` is an indexed typed graph whose identity participates in sharing; a temporary `egg::EGraph` optimizes closed, total expressions and returns literal rewrites. It does not hold the entire lazy program.[5]

Perry already matches ordinary record shapes during lowering and assigns nominal MIR handles; recursive definitions receive reserved identities. Its lowering layer documents narrower-record compatibility as unsupported. This is a useful starting point for separating applicability from identity. J-core makes specialization that explicit boundary, replacing generated-name matching with definition and instance identities rather than requiring all compatible shapes to become one type. Nix-wit's runtime-oriented scalar graph provides a separate integration reference. Import logical information before physical carriers or language-specific demand machinery erase it.[5][10]

## Lowering handoff

The final artifact owned by J-core is a verified typed module with generic schemes, resolved nominal instances, expression structure, captures, continuations, primitive contracts, and conservative analysis results.

```text
minimal syntax ─────┐
Nix frontend ───────┼─→ J-core generic expressions
Perry frontend ────┘              │
                        structural constraints
                                 │
                    nominal instance specialization
                                 │
                         shared safe rewrites
                                 │
                    ───── end of J-core ─────
                                 │
                  consumer evaluation elaboration
                       /                   \
              eager sequencing        shared demand
                       \                   /
                 consumer representation lowering
                                 │
                        executable IR / Wasm
```

For an eager consumer, elaboration determines argument and construction order and preserves exceptions from unused eager expressions. For a lazy consumer, it creates demand relationships, shared evaluation cells, and forcing behavior, including recursive-demand failures. These are substantial separate implementations with shared input types.

Mutation, identity-sensitive objects, native resources, and ambient operations enter only through explicit boundaries unless the consumer has proved a functional interpretation valid. A typed call to an opaque operation is representable; pretending its implementation is part of the portable functional subset is not.

No common runtime, evaluator, thunk allocator, JavaScript object model, Nix module loader, or WIT component emitter is required to publish J-core. Consumers own executable semantics below the documented handoff.

## Acceptance criteria

1. **Independent package:** build and test from a registry-compatible package without either consumer checkout. The optional syntax feature has no runtime or compiler dependency on them.
2. **Nominal composition:** infer a row-preserving higher-order transformation and specialize it for distinct nominal records, including nested and recursive structures. Verify repeated instance reuse, let-polymorphic applicability, and explicit rejection of incompatible or opaque types. Rejected terms produce source-located diagnostics.
3. **Continuation composition:** verify joins, answer types, captures, scoped escape, reusable destinations, and affine imported destinations using the same code-region representation as functions.
4. **Syntax parity:** parse both profiles into equivalent logical structures for paired fixtures. Run only the declared portable subset through both native languages as an equivalence check.
5. **Boundary preservation:** retain unused failure, unused divergence, effectful arguments, and unselected record fields until consumer elaboration. Verify the expected eager/lazy differences after that handoff.
6. **Identity discipline:** repeated nominal instances reuse identities; structurally compatible definitions can remain distinct. Specialization introduces no unnecessary record conversion, allocation, or mandatory body duplication. Effectful expression occurrences and source bindings cannot be merged accidentally. Mutable aliases cannot masquerade as immutable rows.
7. **Measured integration:** express the same nested-data pipeline in both consumers, including a retained higher-order helper and a continuation. Identify and remove the duplicated production responsibility actually superseded.

The first release should demonstrate these boundaries with a small operation set. Full JavaScript/Nix compatibility, generalized effect handlers, schema-directed JSON runtimes, and backend unification would be separate projects.

## Research sources

These references support the distinctions used here. The crate design and its scope are recommendations derived from them, not functionality supplied wholesale by any source.

1. **Koka:** Daan Leijen, [Programming with Row-polymorphic Effect Types](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/paper-20.pdf), especially the sections on heap safety and type inference; [current Koka book](https://koka-lang.github.io/koka/doc/book.html). The generalization discussion above refers to the paper's formal system, not a claim that every detail matches the current implementation.
2. **Call-by-push-value:** Paul Blane Levy, [Effects and Call-by-Push-Value](https://pblevy.github.io/mgs/effcbpv.html). Basis for distinguishing values, computations, and control while relating evaluation strategies.
3. **pliron, revision `6ff5b3c8a6d5553b8cbee19d58f3c039f10e5a97`:** [region interfaces](https://github.com/pliron-org/pliron/blob/6ff5b3c8a6d5553b8cbee19d58f3c039f10e5a97/src/builtin/op_interfaces.rs), [SCCP](https://github.com/pliron-org/pliron/blob/6ff5b3c8a6d5553b8cbee19d58f3c039f10e5a97/src/opts/constants/sccp.rs), [Mem2Reg](https://github.com/pliron-org/pliron/blob/6ff5b3c8a6d5553b8cbee19d58f3c039f10e5a97/src/opts/mem2reg.rs). These implementations were inspected locally; publication compatibility needs separate verification.
4. **MLIR:** [Language Reference](https://mlir.llvm.org/docs/LangRef/), particularly graph regions versus SSACFG regions. Architectural reference for dialects and regions; no MLIR runtime dependency is proposed.
5. **nix-wit, revision `65aaa12c83cc7ca43549689da68583009859fd21`:** locally inspected [typed expression graph](/Users/dafcok/Documents/Development/RUST/monty/playground/nix-wit/crates/core/src/ir.rs), [term representation](/Users/dafcok/Documents/Development/RUST/monty/playground/nix-wit/crates/core/src/ir/term.rs), [restricted e-graph optimizer](/Users/dafcok/Documents/Development/RUST/monty/playground/nix-wit/crates/core/src/ir/term/rewrite.rs), and [type refinement](/Users/dafcok/Documents/Development/RUST/monty/playground/nix-wit/crates/core/src/ir/ssa/types.rs). These local links are checkout references, not independently verified public publication URLs.
6. **Nix:** [Syntax and semantics, manual 2.34](https://nix.dev/manual/nix/2.34/language/syntax.html). Reference for the Nix syntax profile.
7. **ECMAScript:** [Language expressions](https://tc39.es/ecma262/multipage/ecmascript-language-expressions.html). Reference for arrow functions, object initializers, application, and expression grammar.
8. **egg:** [EGraph API](https://docs.rs/egg/latest/egg/struct.EGraph.html). Equality representation and analysis, distinct from source binding identity.
9. **Cargo:** [Specifying dependencies](https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html#multiple-locations). Registry dependency requirements for publication.
10. **Perry-WIT:** inspected [record types](/Users/dafcok/.codex/worktrees/96c5/perry-wit/crates/perry-mir/src/types.rs) and [shape lowering](/Users/dafcok/.codex/worktrees/96c5/perry-wit/crates/perry-lower/src/shapes.rs). Ordinary shapes are matched structurally before receiving nominal MIR handles; recursive definitions reserve identities. The proposed specialization boundary builds on this distinction while making compatibility and instance identity explicit.

