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

[simontreanor]

Closes #110.

Derived codecs

Encode.auto : a -> string and Decode.auto : Decoder a are derived from the type, so a program that speaks to itself over a wire (or a save file) writes both ends in one line each, and the property the tests state once holds: Decode.decodeString Decode.auto (Encode.auto v) == Ok v for records, sum types, tuples, List, Set, Map, Option, Result, newtypes (read through to the underlying value) and any recursion through them.

let wire = Encode.auto view              // a record holding a Map (int, int) Placed, nested cases, a Tree, a Set
match Decode.decodeString Decode.auto wire:
  case Ok v: print (v == view)           // True
  case Error e: print e.errorMessage

Wire shape (decided in ROADMAP item 19): internally tagged objects, the serde / Pydantic / System.Text.Json convention. A record is an object keyed by its Pyfun field names; a case is {"type": "Move", "fields": ["K11 a QUIZ"]} ({"type": "Resign"} when nullary); 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 a list of [key, value] pairs.

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, so _pf_enc_value reads the value's shape via dataclasses.fields (a keyword-mangled class_ travels 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 (record fields, constructor payloads at the instantiated type, newtypes read through). Lowering turns it into a descriptor the emitted _pf_dec_auto interprets; user-declared types live in a per-module _pf_codecs table under their displayed type, so a recursive Tree is ("ref", "Tree"):

_pf_codecs = {"Msg": ("adt", {"Hello": (Hello, [("ref", "Player")]), "Move": (Move, [("str",)]), "Resign": (_Resign, [])}),
              "Tree": ("adt", {"Leaf": (_Leaf, []), "Node": (Node, [("ref", "Tree"), ("int",), ("ref", "Tree")])}), …}

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), so it composes with Decode.field/map2/andThen and runs under decodeString's try.

Open sites. An a still open at the site is an error naming the ways to pin it. Because the codec comes from the resolved type, a site's variable stays weak at let-generalization (OCaml's '_a, the 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. A function, an extern type, a lazy Seq or an Async have no JSON form and say so. Cross-module types work when the declaring module is imported directly (the descriptor names rules.View).

Elsewhere

types::Codecs rides from check_collecting / check_module_collecting into lower_collecting / lower_in_project beside the float-literal spans. The Python IR gains a Dict display, and one-element tuples now emit with their trailing comma (("str",); the old ("str") was a parenthesised string). DESIGN.md §6 gets the "Derived codecs" paragraph, INTERNALS the plumbing note, lesson 12 a derived-codecs section (verified), ROADMAP item 19 is closed. Not done, and recorded: a composable Encode (Encode.object, 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.

Tests

Typecheck: the weak-variable pinning (top-level let then match; inside a function), the open-site error and the function/extern-type errors, Encode.auto pure and polymorphic. E2E: the rich round trip above with the descriptor table asserted and five error messages, a newtype plus keyword-named field, and a cross-module project round trip (tests/project.rs). cargo test, cargo clippy --all-targets, cargo fmt --check and docs/verify_lessons.py are clean.