Source-linked AI summary
You may implement this later: Cofunctors as partial implementations
Vincent Wang-Maścianica
TL;DR
The paper asks how to assemble implementations while deferring backend choices that may depend on specification state. It reads cofunctors as partial implementations, characterizes their compositional behavior, and illustrates executable migration plans with deferred choices.
Problem
Implementations may need to defer backend choices because available choices can depend on where composition reaches in the specification.
Method
The paper models partial implementations with state-dependent choices whose implementation map updates state and composes through staged implementation.
Results
Cofunctors recover parameterized implementations and ordinary functors as special cases, while a companion program constructs executable migration plans before execution.
Takeaways & Limitations
The paper presents “cofunctors are partial implementations” as a practical reading in which deferred choices are managed externally and resolved by later semantics.
Takeaways & Limitations
The paper acknowledges an objection that specifying Choice might require enumerating every implementation state that could arise.
Abstract
from arXiv · showhide
A functor is a familiar model of an implementation, where every operation in a specification is assigned a concrete instantiation at the outset. But some tasks are less eager: we often want to assemble systems while leaving backend choices such as data representations and algorithms for later. We observe that cofunctors admit a direct reading as such partial implementations, which are implementations whose extra argument is a state-dependent family of deferred choices. While cofunctors (also called retrofunctors) are not novel, their conceptual and purposive reading in this manner appears to be
1 Implement now, or later?
The paper contrasts eager implementations, which fix every operation immediately, with partial implementations that defer backend and representation choices. When choices depend on the specification state and evolve through composition, a single global parameter is insufficient.
- Staged configuration allows persistence, serialization, and replication decisions to be made at different stages.
- A categorical functor models an eager implementation by assigning concrete implementations to every specification object and operation.
- Parameterised modules defer implementation choices through a global parameter supplied later.
- Specification-dependent choices can be introduced or constrained by composition, making a single global parameter the wrong shape.For the store example, persistence may introduce serialization, while replication may add transaction requirements that expose backend conflicts.
2 A signature for partial implementations
The proposed signature represents partial implementations with specification-dependent choice states, transports those states along specification changes, and composes implementation changes sequentially. It generalizes ordinary parameterized implementations and reduces to functors when no choices remain.
- Partial implementations pair each specification object with a dependent choice state that may contain fixed fields, open fields, and accumulated obligations.
- Choice is required to preserve identities and compose transports, so it forms a functor from specifications to Set.
- Each specification change transports a current choice state forward and maps it to a corresponding partial-implementation change.
- The composition rule implements the first change, updates the implementation state, and then implements the second change using that updated state.
- The construction is a state-dependent generalization of ML-functors and recovers the constant-parameter case when all choice sets are the same and transports are identities.
- When every choice set is a singleton, the object and morphism maps reduce to an ordinary categorical functor.
3 That was a cofunctor
The paper identifies the resulting structure as a cofunctor, using an object bijection together with equations that encode identity and composition laws. Its categorical span presentation separates the dependent menu of choices from the interpretation of lifted implementation requests.
- The object mapping from specification-and-choice pairs to partial implementations is bijective onto the objects of P.
- Equations (1)–(4), together with the object bijection, define a cofunctor from S to P.
- In the span presentation, the discrete opfibration has fibre Choice(A), and its unique lifts are the transports f* between choice states.
- The other span leg interprets lifted requests as implementation artefacts, while object bijectivity ensures each partial implementation corresponds to exactly one obligation state.
Peanut gallery
The paper distinguishes cofunctors from static assembly and eager semantics by treating them as environments for composing partial implementations whose choices remain externally supplied. This supports live transformations of deployed systems, while later semantics can identify implementations with the same behaviour.
- Static assembly and cofunctors: A cofunctor stops before choosing a codomain semantics, so implementation changes compose before any concrete program category is declared.A later functor supplies semantics and may identify states with the same behaviour.
- Static assembly and cofunctors: The cofunctor models an environment for making and managing composite partial implementations, with choices supplied from outside.The semantics functor is treated as the last externally supplied choice.
- State-space objection: Partial implementation states need not enumerate every possible state: n optional fields yield 2^n obligation states in n lines.Each specification has its own choice fibre, while the range of values within a fibre is fixed up front.
- Static assembly and cofunctors: The approach differs from Backpack-style static assembly because it supplies state-indexed implementation arrows for live migration.Backpack can merge or fill hole interfaces, but the paper says it does not provide the corresponding running-store transformation and composition law.
- Static assembly and cofunctors: Cofunctors support transformations of running stores and composition laws that static assembly does not provide.They can handle a store after deployment and while it is holding data.
4 Procrastinating with cofunctors
The demonstration constructs typed migration plans for a deployed store, composes staged changes, and refines unresolved obligations before execution. The resulting plan completes a SQLite store with CBOR serialization, an open log, one replica, and Raft.
- Executable migration plans: Transport through persistence records durability while preserving existing decisions; replication adds transaction-log and replica-seeding effects plus an open protocol obligation.Replication also checks whether the backend supports transactions.
- Executable migration plans: Non-transactional flat-file replication becomes an explicit Conflict rather than an invalid or incomplete transport.The choice-level implementation carries the conflict forward when the backend cannot satisfy replication.
- Executable migration plans: The companion program builds typed migration plans in a category P, where plans compose before execution and record deployed-store effects.No semantic codomain C appears in the program.
- Composition and refinement: The staged composition law checks case by case that direct and sequential plans compute to the same record of effects.The cases hold by Refl because both sides reduce to identical records; a one-pass plan violating staged effects is rejected.
- Composition and refinement: Refinement is an arrow in P rather than a transport, because it has no underlying specification change.It fills unresolved fields such as serialiser and protocol after the specification remains ReplicatedStore.
- Execution result: The executed plan records an open serialiser, creates durable storage, opens a transaction log, seeds one replica, and commits CBOR and Raft.The completed store is SQLite/CBOR/LRU/Raft with durability, an open log, and 1 replica.
5 Deferred notes
The note presents cofunctors as a new practical conceptual reading of established categorical machinery: partial implementations with deferred, state-dependent choices. It situates this slogan among staged configuration, parameterised modules, dependent types, deferred interpreters, and prior cofunctor research.
- Staged configuration, parameterised modules, and dependent types already support deferred choices through other functional-programming techniques.These approaches are established, but the note connects that usage to cofunctors specifically.
- Tagless-final encodings, free constructions, and effect handlers defer interpretation, but select one interpreter or handler for the whole program.They therefore resemble a global-parameter shape rather than supporting per-state obligations that composition can rewrite.
- The absence of this functional-programming connection may partly reflect confusion with contravariant functors, also colloquially called cofunctors.The note identifies this terminology as a possible reason the connection remained underused or overlooked.
- Cofunctors have prior names and applications, including retrofunctors, delta lenses, update-update lenses, layered monoidal theories, and cofunctor boxes.The related work traces the construction across categorical and lens literature.
- The note’s central contribution is the practical slogan that cofunctors are partial implementations.The author explicitly presents this conceptual reading as new while noting that cofunctors and their ingredients are not novel.