ff-generics is an Agda library for describing finite families of algebraic datatypes as first-order generic codes.
It is built on Cubical Agda, typechecks in safe mode, and integrates with ff-json so generic specifications and values can be serialized when the atom universe has JSON codecs.
Core Idea
A type is generic when it can be represented as:
- an atom, deliberately treated as primitive; or
- one datatype from a finite family, where constructor fields are either recursive references to the family or atoms.
That covers ordinary datatypes, recursive datatypes, and mutually recursive families. The core formalization does not try to infer everything automatically. It is explicit and proof-carrying, while the macro layer handles a smaller practical fragment.
What The Generic Record Carries
A Generic U A is more than a schema. It contains:
- the finite type count;
- a description for every datatype in the family;
- the root being represented;
- type names and constructor names for tooling;
- an encoder from
A to indexed generic code;
- a decoder back to
A;
- proofs that encode/decode form an isomorphism.
This makes the generic layer suitable for tooling that must remain explainable: editor UIs, JSON interchange, generated code, and inspection panels can all refer back to the same checked description.
Practical Surfaces
The library includes:
Generic.Core for descriptions, indexed codes, atoms, and notation;Generic.Json and Generic.NativeJson for serialization;Generic.PrimAtom for string, natural number, integer, and boolean leaves;Generic.Macro for deriving simple instances;- examples for enums, records, non-nullary constructors, recursive lists, mutual recursion, built-in atoms, and custom atoms;
- a hand-written generic instance for Agda reflection terms;
- an unsafe companion library with a browser value-editor macro.
Where It Connects
MLTTDB uses ff-generics as a structured editor direction. A table can expose a generic row specification, load a current value as JSON, let the browser edit the value, and save generated Agda source back through the normal record endpoint.
That makes ff-generics a bridge between formal schemas and usable interfaces: the proof-carrying datatype description is not only a theorem object, but also an editor contract.
Why It Matters
In a proof assistant, a datatype is not automatically a form, a JSON schema, or a browser editor. It is checked source. Product workflows need enough structure for tooling while preserving the relationship to the original type.
ff-generics supplies that structure for selected finite datatype families. A tool can inspect constructor names, see which fields are recursive, distinguish primitive leaves from nested values, serialize generic values through ff-json, and render a usable editor around the checked description.
The library is a precise core and experimentation ground, not a universal generic-programming system for all Agda code. That boundary is useful. It keeps the claim credible: Formal Foundry can turn selected checked datatype families into usable tooling contracts, with representation and roundtrip evidence kept explicit.
