codecs: Encode.auto and Decode.auto, derived from the type

DESIGN.md

@@ -800,6 +800,40 @@ the new general `PyStmt::Raise` node and the `is` comparison for `null`). The ge
 (user-registered combinators, a `Value` type for already-parsed data) is deferred; the shipped set already
 covers records, lists, options, and unions.
 
+**Derived codecs — `Decode.auto` and `Encode.auto`.** A program that speaks to itself over a wire
+(or a save file) has the same Pyfun type on both ends, and writing the two halves by hand is where
+they drift. `Encode.auto : a -> string` and `Decode.auto : Decoder a` are derived from the type, so
+both ends are one line and the property the tests state once is `Decode.decodeString Decode.auto
+(Encode.auto v) == Ok v` for every type the derivation accepts: the primitives, records, sum types,
+tuples, `List`, `Set`, `Map`, `Option`, `Result`, newtypes (erased, so the wire carries the
+underlying value), and any recursion through them. **The shape** is the convention serde
+(`#[serde(tag = "type")]`), Pydantic discriminated unions and System.Text.Json share: a record is an
+object keyed by its Pyfun field names; a sum-type case is `{"type": "Move", "fields": [...]}` with
+positional payloads (`{"type": "Resign"}` for a nullary case; F#'s `{"Case", "Fields"}` is the outlier
+and was not copied); `Option` is `null` or the value; tuples and `List`/`Set` are arrays; a `Map` with
+string keys is an object and any other key type is a list of `[key, value]` pairs; `unit` is `null`.
+**Two mechanisms.** `Encode.auto` is a run-time helper: the emitted classes already carry a record's
+field names and a case's class name (the same knowledge `__repr__` uses), so `_pf_enc_value` reads
+the value's shape (`dataclasses.fields`, a keyword-mangled `class_` travelling as `class`) and
+`json.dumps` the result. `Decode.auto` is **type-directed lowering after inference**: the checker
+records every `Decode.auto` site with its instantiated `Decoder a`, resolves `a` once inference is
+complete, and derives a [`Codec`] from the declarations (records' fields, constructors' payloads at
+the instantiated type, newtypes read through); lowering turns it into a descriptor the emitted
+`_pf_dec_auto` interprets (`("record", Point, [("x", ("int",)), …])`, `("adt", {"Move": (Move,
+[("str",)])})`), user-declared types living in a per-module `_pf_codecs` table under their displayed
+type so a recursive `Tree` is a `("ref", "Tree")` back into it. The derived decoder is a `Decoder`
+like any other (a callable that raises on a mismatch, strict like the primitives, `unknown case Nope`
+/ `expected an object, got list` as the message), so it composes with `Decode.field`/`map2`/`andThen`
+and runs under `decodeString`'s `try`. An `a` still open at the site is an error there, with the ways
+to pin it named; a function, an extern type, a lazy `Seq` or an `Async` have no JSON form and say so.
+Because the codec is derived from the *resolved* type, a `Decode.auto` site's type variable stays
+**weak** at `let`-generalization (OCaml's `'_a`, the same discipline a deferred field access already
+follows), so `let back = Decode.decodeString Decode.auto wire` at the top level is pinned by the
+`match` that follows rather than each use getting a copy that pins nothing. Cross-module types work
+when the declaring module is imported directly (the descriptor names `rules.View`); a transitively
+carried record says to import its module. Type classes stay rejected: this is one derivation for one
+built-in decoder, not a mechanism for user-defined derivations.
+
 **String interpolation — `f"..."`.** Python-style interpolated strings: an `f` prefix
 (adjacent to the quote — `f "x"` with a space stays ordinary application, as in Python) with `{expr}`
 holes holding **full Pyfun expressions**, and `{{`/`}}` for literal braces. The whole string is a

INTERNALS.md

@@ -418,6 +418,10 @@ stdio. All features reuse the existing front end:
   `string ->{io} unit`) plus a **dedicated `Effect:` line** summarizing the concrete effect performed
   on full application (the union of the type's *result-spine* arrows — `io`/`async`; argument arrows
   are a callback's effect, not the value's, and pure values omit the line — `types::effect_summary`).
+  (The same pass hands lowering the derived codecs: `types::check_collecting` returns a
+  `types::Codecs`, one `Codec` per `Decode.auto` site keyed by span plus the named table, and
+  `lowering::lower_collecting` / `lower_in_project` take it beside the float-literal spans —
+  `DESIGN.md` §6, "Derived codecs".)
   It works because the checker, in a `record`-enabled pass (`types::check_collecting`, surfaced via
   `analyze`), accumulates a `(span, ty)` table for every expression node, binding name, function
   parameter, and pattern variable, then resolves each entry against the final substitution and renders

ROADMAP.md

@@ -352,21 +352,25 @@ play comes first; the browser target is last because it depends on the async dec
     dies with the session. It is promoted to the prelude once its signature stops moving; the game
     is its first consumer.
 
-19. **`Encode` to mirror `Decode`, with derived codecs** (#110, M–L, shape decided). A program that
-    speaks to itself over a wire writes values out with f-strings and reads them back with
-    `Decode.field` by hand, and the two drift; `Decode.map2` scales to two fields and a hand-written
-    decoder for a record holding a `Map (int, int) Placed` is forty lines. Two mechanisms: `Encode.auto
-    : a -> Json` is a runtime helper (the emitted classes carry their fields and case names, the same
-    knowledge `__repr__` uses); `Decode.auto : Decoder a` needs `a` known statically at the use site,
-    so it is type-directed lowering after inference (precedent: Decode specialization, `DESIGN.md`
-    §5.3) with a rejection when `a` is still a variable. Both ship together so both ends are one line,
-    and the property the tests state once is `Decode.auto (Encode.auto v) == Ok v`. **Decided shape:**
+19. ~~**`Encode` to mirror `Decode`, with derived codecs**~~ **CLOSED 2026-08-30** (#110, in the PR
+    carrying this entry). A program that speaks to itself over a wire wrote its values out with
+    f-strings and read them back with `Decode.field` by hand, and the two drifted. Now `Encode.auto :
+    a -> string` and `Decode.auto : Decoder a` are derived from the type (`DESIGN.md` §6, "Derived
+    codecs"): `Encode.auto` is a run-time helper reading the value's shape from the emitted classes;
+    `Decode.auto` is type-directed lowering after inference, the checker resolving each site's
+    `Decoder a` into a `Codec` (records, sum types, tuples, `List`/`Set`/`Map`/`Option`/`Result`,
+    newtypes read through, recursion via a per-module table) that lowering turns into a descriptor
+    the emitted `_pf_dec_auto` interprets. A site whose type is still open is an error naming the ways
+    to pin it, and its variable stays weak at `let`-generalization so a later use pins it. The
+    round-trip property holds on a record holding a `Map (int, int) Placed`, a recursive `Tree`, a
+    `Set`, a tuple and nested cases, in one file and across a project import. **Decided shape:**
     internally tagged objects, the convention serde (`tag = "type"`), Pydantic discriminated unions
-    and System.Text.Json share: a case with a record payload is `{"type": "Move", "square": "K11"}`,
-    positional payloads are `{"type": "Move", "fields": [...]}`, `Option` is `null` or the value,
-    tuples are arrays, a `Map` with string keys is an object and any other key type is a list of
-    `[k, v]` pairs. F#'s `{"Case", "Fields"}` is the outlier and was not copied. The game's `.replay`
-    files are free to adopt the same encoding.
+    and System.Text.Json share: `{"type": "Move", "fields": ["K11 a QUIZ"]}`, `{"type": "Resign"}`,
+    `Option` as `null` or the value, tuples as arrays, a `Map` with string keys as an object and any
+    other key type as a list of `[k, v]` pairs. F#'s `{"Case", "Fields"}` is the outlier and was not
+    copied. The game's `.replay` files are free to adopt the same encoding. **Not done:** a
+    composable `Encode` (`Encode.object`, `Encode.list`, a `Json` value type) for shapes that are not
+    a Pyfun type's own; a hand-written decoder remains the tool at a boundary you do not control.
 
 20. **A browser target** (#111, L, last). Three pieces once the async items are in: `pyfun bundle`
     (a static page: the compiled Python, the program's data files, and the Pyodide loader the

docs/src/learn/12-python-interop.md

@@ -88,6 +88,40 @@ missingField |> Decode.decodeString bookDecoder |> describe |> print
 
 The well-formed object decodes to a typed `Book`. The object missing `pages` short-circuits to an `Error` carrying the Python exception, which `match` forces you to handle. The output is `Dune, 412 pages` then `failed (KeyError)`.
 
+## Derived codecs
+
+Hand-written decoders are the right tool at a boundary you do not control. When both ends of the
+wire are your own Pyfun types, the compiler already knows every field and every case, so it can
+derive the codec. `Encode.auto` turns any value into JSON text, and `Decode.auto` is a decoder
+derived from the type it is used at:
+
+```pyfun
+type Player = Ann | Bob
+type Msg = Hello Player | Move string | Resign
+type Turn = { player: Player, msg: Msg, score: Option int }
+
+let turn = Turn { player = Bob, msg = Move "K11 a QUIZ", score = Some 42 }
+let wire = Encode.auto turn
+print wire
+
+let describe t = f"{t.player} played {t.msg}"
+
+match Decode.decodeString Decode.auto wire:
+  case Ok back: print (describe back)
+  case Error e: print f"failed: {e.errorMessage}"
+```
+
+```console
+{"player": {"type": "Bob"}, "msg": {"type": "Move", "fields": ["K11 a QUIZ"]}, "score": 42}
+Bob played Move('K11 a QUIZ')
+```
+
+A record is an object keyed by its field names, a case is `{"type": …, "fields": […]}`, an `Option`
+is `null` or the value, and a `Map` with string keys is an object. The decoder is strict like the
+primitives, so `{"type": "Nope"}` is an `Error` naming the unknown case rather than a crash later.
+`Decode.auto` reads the type from where it is used: here `describe back` fixes `back` to a `Turn`. If
+nothing fixes it, the compiler says so at the site instead of guessing.
+
 ## Handing Python a function
 
 A callback crosses the boundary the other way, and two rules keep it honest. Write a callback of

src/lib.rs

@@ -167,7 +167,7 @@ pub fn compile_collecting(
     // One inference pass gives both the gate (errors) and the resolved types, from
     // which we mark the integer literals that resolved to `float` so lowering emits
     // them as `7.0` (matching their inferred type — see `float_literal_spans`).
-    let (mut errors, types, holes, ordered) = types::check_collecting(&module);
+    let (mut errors, types, holes, ordered, codecs) = types::check_collecting(&module);
     if !errors.is_empty() {
         return Err(CompileError::Type(errors.remove(0)));
     }
@@ -182,9 +182,13 @@ pub fn compile_collecting(
     let floats = float_literal_spans(&types);
     // Single file: the whole program is visible, so emit ordering methods only for the
     // types actually compared (`DESIGN.md` §7.1).
-    let (py, notes) =
-        lowering::lower_collecting(&module, &floats, lowering::OrderPolicy::OnDemand(ordered))
-            .map_err(CompileError::Lower)?;
+    let (py, notes) = lowering::lower_collecting(
+        &module,
+        &floats,
+        lowering::OrderPolicy::OnDemand(ordered),
+        &codecs,
+    )
+    .map_err(CompileError::Lower)?;
     Ok((python_emitter::emit_for(&py, target), notes))
 }